harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_const_sub_uIcc : (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
dsimp [Function.comp_def] at this

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), (fun x => a + -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
simp [sub_eq_add_neg, this, add_comm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]

Tactic:
have := image_comp (fun x => a + x) fun x => -x

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c : α
this : ∀ (a_1 : Set α), ((fun x => a + x) ∘ fun x => -x) '' a_1 = (fun x => a + x) '' ((fun x => -x) '' a_1)
⊢ (fun x => a - x) '' [[b, c]] = [[a - b, a - c]]
-- Mathlib/Order/RelClasses.lean
lemma ssubset_of_ssubset_of_eq (hab : a ⊂ b) (hbc : b = c) : a ⊂ c

Proof state:
α : Type u
inst✝ : HasSSubset α
a b c : α
hab : a ⊂ b
hbc : b = c
⊢ a ⊂ c

Tactic:
rwa [← hbc]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem exists_real_pos_lt_infEdist_of_not_mem_closure {x : α} {E : Set α} (h : x ∉ closure E) :
    ∃ ε : ℝ, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : x ∉ closure E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Tactic:
rw [← infEdist_pos_iff_not_mem_closure, ENNReal.lt_iff_exists_real_btwn] at h

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : ∃ r, 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
h : ∃ r, 0 ≤ r ∧ 0 < ENNReal.ofReal r ∧ ENNReal.ofReal r < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Tactic:
rcases h with ⟨ε, ⟨_, ⟨ε_pos, ε_lt⟩⟩⟩

Result:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
ε : ℝ
left✝ : 0 ≤ ε
ε_pos : 0 < ENNReal.ofReal ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Proof state:
case intro.intro.intro
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
E : Set α
ε : ℝ
left✝ : 0 ≤ ε
ε_pos : 0 < ENNReal.ofReal ε
ε_lt : ENNReal.ofReal ε < infEdist x E
⊢ ∃ ε, 0 < ε ∧ ENNReal.ofReal ε < infEdist x E

Tactic:
exact ⟨ε, ⟨ENNReal.ofReal_pos.mp ε_pos, ε_lt⟩⟩

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma compAddMonoidHom_injective_left (f : A →+ B) (hf : Surjective f) :
    Injective fun ψ : AddChar B M ↦ ψ.compAddMonoidHom f

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
⊢ Injective fun ψ => ψ.compAddMonoidHom f

Tactic:
rintro ψ χ h

Result:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : (fun ψ => ψ.compAddMonoidHom f) ψ = (fun ψ => ψ.compAddMonoidHom f) χ
⊢ ψ = χ

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ => ψ.compAddMonoidHom f) ψ) = ⇑((fun ψ => ψ.compAddMonoidHom f) χ)
⊢ ⇑ψ = ⇑χ

Tactic:
exact hf.injective_comp_right h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : (fun ψ => ψ.compAddMonoidHom f) ψ = (fun ψ => ψ.compAddMonoidHom f) χ
⊢ ψ = χ

Tactic:
rw [DFunLike.ext'_iff] at h ⊢

Result:
A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
f : A →+ B
hf : Surjective ⇑f
ψ χ : AddChar B M
h : ⇑((fun ψ => ψ.compAddMonoidHom f) ψ) = ⇑((fun ψ => ψ.compAddMonoidHom f) χ)
⊢ ⇑ψ = ⇑χ
-- Mathlib/Data/Nat/PartENat.lean
theorem add_one_le_iff_lt {x y : PartENat} (hx : x ≠ ⊤) : x + 1 ≤ y ↔ x < y

Proof state:
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m + 1 ≤ y
⊢ ↑m < y

Tactic:
induction' y using PartENat.casesOn with n

Result:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m + 1 ≤ ⊤
⊢ ↑m < ⊤

case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ ↑m < ↑n

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m + 1 ≤ ⊤
⊢ ↑m < ⊤

Tactic:
apply natCast_lt_top

Result:
no goals

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ ↑m < ↑n

Tactic:
norm_cast

Result:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ m < n

Proof state:
case intro.a.h
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ m.succ ≤ n

Tactic:
norm_cast at h

Result:
no goals

Proof state:
case intro.a
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ m < n

Tactic:
apply Nat.lt_of_succ_le

Result:
case intro.a.h
m : ℕ
hx : ↑m ≠ ⊤
n : ℕ
h : ↑m + 1 ≤ ↑n
⊢ m.succ ≤ n

Proof state:
x y : PartENat
hx : x ≠ ⊤
h : x + 1 ≤ y
⊢ x < y

Tactic:
rcases ne_top_iff.mp hx with ⟨m, rfl⟩

Result:
case intro
y : PartENat
m : ℕ
hx : ↑m ≠ ⊤
h : ↑m + 1 ≤ y
⊢ ↑m < y

Proof state:
x y : PartENat
hx : x ≠ ⊤
⊢ x + 1 ≤ y ↔ x < y

Tactic:
refine ⟨fun h => ?_, add_one_le_of_lt⟩

Result:
x y : PartENat
hx : x ≠ ⊤
h : x + 1 ≤ y
⊢ x < y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/DecidableEq.lean
theorem rel_of_isEqv {r : α → α → Bool} {a b : Array α} :
    Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))

Proof state:
case isFalse
α : Type u_1
r : α → α → Bool
a b : Array α
h : ¬a.size = b.size
⊢ false = true → ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Tactic:
intro

Result:
case isFalse
α : Type u_1
r : α → α → Bool
a b : Array α
h : ¬a.size = b.size
a✝ : false = true
⊢ ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
⊢ a.isEqv b r = true → ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Tactic:
simp only [isEqv]

Result:
α : Type u_1
r : α → α → Bool
a b : Array α
⊢ (if h : a.size = b.size then a.isEqvAux b h r a.size ⋯ else false) = true →
    ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Proof state:
case isTrue
α : Type u_1
r : α → α → Bool
a b : Array α
h : a.size = b.size
⊢ a.isEqvAux b h r a.size ⋯ = true → ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Tactic:
exact fun h' => ⟨h, fun i => rel_of_isEqvAux h (Nat.le_refl ..) h'⟩

Result:
no goals

Proof state:
case isFalse
α : Type u_1
r : α → α → Bool
a b : Array α
h : ¬a.size = b.size
a✝ : false = true
⊢ ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Bool
a b : Array α
⊢ (if h : a.size = b.size then a.isEqvAux b h r a.size ⋯ else false) = true →
    ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

Tactic:
split <;> rename_i h

Result:
case isTrue
α : Type u_1
r : α → α → Bool
a b : Array α
h : a.size = b.size
⊢ a.isEqvAux b h r a.size ⋯ = true → ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true

case isFalse
α : Type u_1
r : α → α → Bool
a b : Array α
h : ¬a.size = b.size
⊢ false = true → ∃ h, ∀ (i : Nat) (h' : i < a.size), r a[i] b[i] = true
-- Mathlib/CategoryTheory/Limits/Fubini.lean
theorem colimitIsoColimitCurryCompColim_ι_hom {j} {k} :
    colimit.ι _ (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom =
      (colimit.ι (_) k ≫ colimit.ι (curry.obj G ⋙ colim) j : _ ⟶ colimit (_ ⋙ colim))

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom) ≫ (colimitIsoColimitCurryCompColim G).inv =
    (colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j) ≫ (colimitIsoColimitCurryCompColim G).inv

Tactic:
simp

Result:
no goals

Proof state:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom =
    colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j

Tactic:
rw [← cancel_mono (colimitIsoColimitCurryCompColim G).inv]

Result:
J : Type u_1
K : Type u_2
inst✝⁴ : Category.{u_5, u_1} J
inst✝³ : Category.{u_6, u_2} K
C : Type u_3
inst✝² : Category.{u_4, u_3} C
G : J × K ⥤ C
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
j : J
k : K
⊢ (colimit.ι G (j, k) ≫ (colimitIsoColimitCurryCompColim G).hom) ≫ (colimitIsoColimitCurryCompColim G).inv =
    (colimit.ι ((curry.obj G).obj j) k ≫ colimit.ι (curry.obj G ⋙ colim) j) ≫ (colimitIsoColimitCurryCompColim G).inv
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_lt_pow_of_lt {a n m : Nat} (h : 1 < a) (w : n < m) : a ^ n < a ^ m

Proof state:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
⊢ a ^ n < a ^ (n + 1 + k)

Tactic:
rw [Nat.pow_add, ← Nat.mul_one (a^n)]

Result:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
⊢ a ^ n * 1 < a ^ (n + 1) * a ^ k

Proof state:
a n m : Nat
h : 1 < a
w : n < m
⊢ a ^ n < a ^ m

Tactic:
have := Nat.exists_eq_add_of_lt w

Result:
a n m : Nat
h : 1 < a
w : n < m
this : ∃ k, m = n + k + 1
⊢ a ^ n < a ^ m

Proof state:
a n m : Nat
h : 1 < a
w : n < m
k : Nat
p : m = n + 1 + k
⊢ a ^ n < a ^ m

Tactic:
subst p

Result:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
⊢ a ^ n < a ^ (n + 1 + k)

Proof state:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
⊢ a ^ n * 1 < a ^ (n + 1) * a ^ k

Tactic:
have t : 0 < a ^ k := Nat.pow_pos (Nat.lt_trans Nat.zero_lt_one h)

Result:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
t : 0 < a ^ k
⊢ a ^ n * 1 < a ^ (n + 1) * a ^ k

Proof state:
a n m : Nat
h : 1 < a
w : n < m
k : Nat
p : m = n + k + 1
⊢ a ^ n < a ^ m

Tactic:
rw [Nat.add_right_comm] at p

Result:
a n m : Nat
h : 1 < a
w : n < m
k : Nat
p : m = n + 1 + k
⊢ a ^ n < a ^ m

Proof state:
case intro
a n m : Nat
h : 1 < a
w : n < m
w✝ : Nat
h✝ : m = n + w✝ + 1
⊢ a ^ n < a ^ m

Tactic:
case intro k p =>
rw [Nat.add_right_comm] at p
subst p
rw [Nat.pow_add, ← Nat.mul_one (a^n)]
have t : 0 < a ^ k := Nat.pow_pos (Nat.lt_trans Nat.zero_lt_one h)
exact Nat.mul_lt_mul_of_lt_of_le (Nat.pow_lt_pow_succ h) t t

Result:
no goals

Proof state:
a n m : Nat
h : 1 < a
w : n < m
this : ∃ k, m = n + k + 1
⊢ a ^ n < a ^ m

Tactic:
cases this

Result:
case intro
a n m : Nat
h : 1 < a
w : n < m
w✝ : Nat
h✝ : m = n + w✝ + 1
⊢ a ^ n < a ^ m

Proof state:
a n : Nat
h : 1 < a
k : Nat
w : n < n + 1 + k
t : 0 < a ^ k
⊢ a ^ n * 1 < a ^ (n + 1) * a ^ k

Tactic:
exact Nat.mul_lt_mul_of_lt_of_le (Nat.pow_lt_pow_succ h) t t

Result:
no goals
-- Mathlib/RingTheory/MatrixAlgebra.lean
theorem left_inv (M : A ⊗[R] Matrix n n R) : invFun n R A (toFunAlgHom n R A M) = M

Proof state:
case add
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y) = x + y

Tactic:
conv_rhs => rw [← hx, ← hy, ← invFun_add]

Result:
no goals

Proof state:
case tmul
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
a : A
m : Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A) (a ⊗ₜ[R] m)) = a ⊗ₜ[R] m

Tactic:
simp

Result:
no goals

Proof state:
case add
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) (x + y)) = x + y

Tactic:
rw [map_add]

Result:
case add
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x y : A ⊗[R] Matrix n n R
hx : invFun n R A ((toFunAlgHom n R A) x) = x
hy : invFun n R A ((toFunAlgHom n R A) y) = y
⊢ invFun n R A ((toFunAlgHom n R A) x + (toFunAlgHom n R A) y) = x + y

Proof state:
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
M : A ⊗[R] Matrix n n R
⊢ invFun n R A ((toFunAlgHom n R A) M) = M

Tactic:
induction M with
| zero => simp
| tmul a m => simp
| add x y hx hy =>
  rw [map_add]
  conv_rhs => rw [← hx, ← hy, ← invFun_add]

Result:
no goals

Proof state:
case zero
n : Type u_1
R : Type u_2
A : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ invFun n R A ((toFunAlgHom n R A) 0) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
lemma mem_ball_dynEntourage {T : X → X} {U : Set (X × X)} {n : ℕ} {x y : X} :
    y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
x y : X
⊢ y ∈ ball x (dynEntourage T U n) ↔ ∀ k < n, T^[k] y ∈ ball (T^[k] x) U

Tactic:
simp only [ball, mem_preimage]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
x y : X
⊢ (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
x y : X
⊢ (x, y) ∈ dynEntourage T U n ↔ ∀ k < n, (T^[k] x, T^[k] y) ∈ U

Tactic:
exact mem_dynEntourage

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem sumCongr_trans {α₁ α₂ β₁ β₂ γ₁ γ₂} (e : α₁ ≃ β₁) (f : α₂ ≃ β₂) (g : β₁ ≃ γ₁) (h : β₂ ≃ γ₂) :
    (Equiv.sumCongr e f).trans (Equiv.sumCongr g h) = Equiv.sumCongr (e.trans g) (f.trans h)

Proof state:
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
⊢ (e.sumCongr f).trans (g.sumCongr h) = (e.trans g).sumCongr (f.trans h)

Tactic:
ext i

Result:
case H
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) i = ((e.trans g).sumCongr (f.trans h)) i

Proof state:
case H
α₁ : Type u_9
α₂ : Type u_10
β₁ : Type u_11
β₂ : Type u_12
γ₁ : Type u_13
γ₂ : Type u_14
e : α₁ ≃ β₁
f : α₂ ≃ β₂
g : β₁ ≃ γ₁
h : β₂ ≃ γ₂
i : α₁ ⊕ α₂
⊢ ((e.sumCongr f).trans (g.sumCongr h)) i = ((e.trans g).sumCongr (f.trans h)) i

Tactic:
cases i <;> rfl

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem sub_mulVec [Fintype n] (A B : Matrix m n α) (x : n → α) :
    (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
A B : Matrix m n α
x : n → α
⊢ (A - B) *ᵥ x = A *ᵥ x - B *ᵥ x

Tactic:
simp [sub_eq_add_neg, add_mulVec, neg_mulVec]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_swap_iff : Principal (Function.swap op) o ↔ Principal op o

Proof state:
o : Ordinal.{u}
op : Ordinal.{u} → Ordinal.{u} → Ordinal.{u}
⊢ Principal (Function.swap op) o ↔ Principal op o

Tactic:
constructor <;> exact fun h a b ha hb => h hb ha

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem coeff_rename_ne_zero (f : σ → τ) (φ : MvPolynomial σ R) (d : τ →₀ ℕ)
    (h : (rename f φ).coeff d ≠ 0) : ∃ u : σ →₀ ℕ, u.mapDomain f = d ∧ φ.coeff u ≠ 0

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : coeff d ((rename f) φ) ≠ 0
⊢ ∃ u, Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0

Tactic:
contrapose! h

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d ((rename f) φ) = 0

Tactic:
apply coeff_rename_eq_zero _ _ _ h

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_add (a b : Ordinal) : b ≠ 0 → cof (a + b) = cof b := fun h => by
  rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)
  · contradiction
  · rw [add_succ, cof_succ, cof_succ]
  · exact (isNormal_add_right a).cof_eq hb

Proof state:
case inl
a : Ordinal.{u_1}
h : 0 ≠ 0
⊢ (a + 0).cof = cof 0

Tactic:
contradiction

Result:
no goals

Proof state:
case inr.inr
a b : Ordinal.{u_1}
h : b ≠ 0
hb : b.IsLimit
⊢ (a + b).cof = b.cof

Tactic:
exact (isNormal_add_right a).cof_eq hb

Result:
no goals

Proof state:
case inr.inl.intro
a c : Ordinal.{u_1}
h : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

Tactic:
rw [add_succ, cof_succ, cof_succ]

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
h : b ≠ 0
⊢ (a + b).cof = b.cof

Tactic:
rcases zero_or_succ_or_limit b with (rfl | ⟨c, rfl⟩ | hb)

Result:
case inl
a : Ordinal.{u_1}
h : 0 ≠ 0
⊢ (a + 0).cof = cof 0

case inr.inl.intro
a c : Ordinal.{u_1}
h : succ c ≠ 0
⊢ (a + succ c).cof = (succ c).cof

case inr.inr
a b : Ordinal.{u_1}
h : b ≠ 0
hb : b.IsLimit
⊢ (a + b).cof = b.cof
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem ascFactorial_eq_factorial_mul_choose' (n k : ℕ) :
    n.ascFactorial k = k ! * (n + k - 1).choose k

Proof state:
n k : ℕ
⊢ n.ascFactorial k = k ! * (n + k - 1).choose k

Tactic:
cases n

Result:
case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

case succ
k n✝ : ℕ
⊢ (n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k

Proof state:
case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)

Tactic:
simp only [zero_ascFactorial, zero_eq, Nat.zero_add, succ_sub_succ_eq_sub,
  Nat.le_zero_eq, Nat.sub_zero, choose_succ_self, Nat.mul_zero]

Result:
no goals

Proof state:
case succ
k n✝ : ℕ
⊢ k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k

Tactic:
simp only [succ_add_sub_one]

Result:
no goals

Proof state:
case zero.zero

⊢ ascFactorial 0 0 = 0! * (0 + 0 - 1).choose 0

Tactic:
rw [ascFactorial_zero, choose_zero_right, factorial_zero, Nat.mul_one]

Result:
no goals

Proof state:
case zero
k : ℕ
⊢ ascFactorial 0 k = k ! * (0 + k - 1).choose k

Tactic:
cases k

Result:
case zero.zero

⊢ ascFactorial 0 0 = 0! * (0 + 0 - 1).choose 0

case zero.succ
n✝ : ℕ
⊢ ascFactorial 0 (n✝ + 1) = (n✝ + 1)! * (0 + (n✝ + 1) - 1).choose (n✝ + 1)

Proof state:
case succ
k n✝ : ℕ
⊢ (n✝ + 1).ascFactorial k = k ! * (n✝ + 1 + k - 1).choose k

Tactic:
rw [ascFactorial_eq_factorial_mul_choose]

Result:
case succ
k n✝ : ℕ
⊢ k ! * (n✝ + k).choose k = k ! * (n✝ + 1 + k - 1).choose k
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma coeSubmodule_differentIdeal [NoZeroSMulDivisors A B] :
    coeSubmodule L (differentIdeal A B) = 1 / Submodule.traceDual A K 1

Proof state:
case e_a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Submodule.map (↑(FractionRing.algEquiv B L)).toLinearMap (Submodule.traceDual A (FractionRing A) 1) =
    Submodule.traceDual A K 1

Tactic:
refine (map_equiv_traceDual A K _).trans ?_

Result:
case e_a
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁹ : CommRing A
inst✝¹⁸ : Field K
inst✝¹⁷ : CommRing B
inst✝¹⁶ : Field L
inst✝¹⁵ : Algebra A K
inst✝¹⁴ : Algebra B L
inst✝¹³ : Algebra A B
inst✝¹² : Algebra K L
inst✝¹¹ : Algebra A L
inst✝¹⁰ : IsScalarTower A K L
inst✝⁹ : IsScalarTower A B L
inst✝⁸ : IsDomain A
inst✝⁷ : IsFractionRing A K
inst✝⁶ : FiniteDimensional K L
inst✝⁵ : Algebra.IsSeparable K L
inst✝⁴ : IsIntegralClosure B A L
inst✝³ : IsIntegrallyClosed A
inst✝² : IsDedekindDomain B
inst✝¹ : IsFractionRing B L
inst✝ : NoZeroSMulDivisors A B
this✝² : ↑(FractionRing.algEquiv B L).toLinearEquiv ∘ₗ Algebra.linearMap B (FractionRing B) = Algebra.linearMap B L
H :
  (algebraMap (FractionRing A) (FractionRing B)).comp ↑(FractionRing.algEquiv A K).symm.toRingEquiv =
    (↑(FractionRing.algEquiv B L).symm.toRingEquiv).comp (algebraMap K L)
this✝¹ : Algebra.IsSeparable (FractionRing A) (FractionRing B)
this✝ : FiniteDimensional (FractionRing A) (FractionRing B)
this : Algebra.IsIntegral A B
⊢ Submodule.traceDual A K (Submodule.map (FractionRing.algEquiv B L) 1) = Submodule.traceDual A K 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_rotateRight {x : BitVec w} {r : Nat} :
    (x.rotateRight r).toNat = (x.toNat >>> (r % w)) ||| x.toNat <<< (w - r % w) % (2^w)

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ (x.rotateRight r).toNat = x.toNat >>> (r % w) ||| x.toNat <<< (w - r % w) % 2 ^ w

Tactic:
simp only [rotateRight_def, toNat_shiftLeft, toNat_ushiftRight, toNat_or]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
theorem closure_neg (s : Set M) : span R (-s) = -span R s

Proof state:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

Tactic:
rw [span_le, coe_set_neg, ← Set.neg_subset, neg_neg]

Result:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)

Proof state:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ s ⊆ ↑(span R s)

Tactic:
exact subset_span

Result:
no goals

Proof state:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(span R (-s))

Tactic:
exact subset_span

Result:
no goals

Proof state:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)

Tactic:
rw [neg_le, span_le, coe_set_neg, ← Set.neg_subset]

Result:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -s ⊆ ↑(span R (-s))

Proof state:
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) = -span R s

Tactic:
apply le_antisymm

Result:
case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ span R (-s) ≤ -span R s

case a
R : Type u_2
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set M
⊢ -span R s ≤ span R (-s)