Batteries.Logic

theorem congrFun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :

f a b = g a b

source

theorem congrFun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :

f a b c = g a b c

source

theorem funext₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : ∀ (a : α) (b : β a), f a b = g a b) :

f = g

source

theorem funext₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : ∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c) :

f = g

source

@[deprecated funext_iff]

theorem Function.funext_iff {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} :

f = g ↔ ∀ (x : α), f x = g x

Alias of funext_iff.

source

theorem Eq.congr :

∀ {α : Sort u_1} {x₁ y₁ x₂ y₂ : α}, x₁ = y₁ → x₂ = y₂ → (x₁ = x₂ ↔ y₁ = y₂)

source

theorem Eq.congr_left {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) :

x = z ↔ y = z

source

theorem Eq.congr_right {α : Sort u_1} {x : α} {y : α} {z : α} (h : x = y) :

z = x ↔ z = y

source

theorem congr_arg {α : Sort u} {β : Sort v} {a₁ : α} {a₂ : α} (f : α → β) (h : a₁ = a₂) :

f a₁ = f a₂

Alias of congrArg.

Congruence in the function argument: if a₁ = a₂ then f a₁ = f a₂ for any (nondependent) function f. This is more powerful than it might look at first, because you can also use a lambda expression for f to prove that <something containing a₁> = <something containing a₂>. This function is used internally by tactics like congr and simp to apply equalities inside subterms.

For more information: Equality

source

theorem congr_arg₂ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} (f : α → β → γ) {x : α} {x' : α} {y : β} {y' : β} (hx : x = x') (hy : y = y') :

f x y = f x' y'

Alias of congrArg₂.

source

theorem congr_fun {α : Sort u} {β : α → Sort v} {f : (x : α) → β x} {g : (x : α) → β x} (h : f = g) (a : α) :

f a = g a

Alias of congrFun.

Congruence in the function part of an application: If f = g then f a = g a.

source

theorem congr_fun₂ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {f : (a : α) → (b : β a) → γ a b} {g : (a : α) → (b : β a) → γ a b} (h : f = g) (a : α) (b : β a) :

f a b = g a b

Alias of congrFun₂.

source

theorem congr_fun₃ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4} {f : (a : α) → (b : β a) → (c : γ a b) → δ a b c} {g : (a : α) → (b : β a) → (c : γ a b) → δ a b c} (h : f = g) (a : α) (b : β a) (c : γ a b) :

f a b c = g a b c

Alias of congrFun₃.

source

theorem heq_of_cast_eq {α : Sort u_1} {β : Sort u_1} {a : α} {a' : β} (e : α = β) :

cast e a = a' → HEq a a'

source

theorem cast_eq_iff_heq :

∀ {a a_1 : Sort u_1} {e : a = a_1} {a_2 : a} {a' : a_1}, cast e a_2 = a' ↔ HEq a_2 a'

source

theorem eqRec_eq_cast {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :

e ▸ x = cast ⋯ x

source

theorem eqRec_heq_self {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} (x : motive a ⋯) {a' : α} (e : a = a') :

HEq (e ▸ x) x

source

@[simp]

theorem eqRec_heq_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :

HEq (e ▸ x) y ↔ HEq x y

source

@[simp]

theorem heq_eqRec_iff_heq {α : Sort u_1} {a : α} {motive : (a' : α) → a = a' → Sort u_2} {x : motive a ⋯} {a' : α} {e : a = a'} {β : Sort u_2} {y : β} :

HEq y (e ▸ x) ↔ HEq y x