harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem coeff_zero_eq_zero (hx : IsIntegral A x) : coeff (minpoly A x) 0 = 0 ↔ x = 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (minpoly A x).coeff 0 = 0 ↔ x = 0

Tactic:
constructor

Result:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (minpoly A x).coeff 0 = 0 → x = 0

case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ x = 0 → (minpoly A x).coeff 0 = 0

Proof state:
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ x = 0 → (minpoly A x).coeff 0 = 0

Tactic:
rintro rfl

Result:
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
hx : IsIntegral A 0
⊢ (minpoly A 0).coeff 0 = 0

Proof state:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
zero_root : (minpoly A x).IsRoot 0
⊢ (algebraMap A B) 0 = 0

Tactic:
exact RingHom.map_zero _

Result:
no goals

Proof state:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
zero_root : (minpoly A x).IsRoot 0
⊢ x = 0

Tactic:
rw [← root hx zero_root]

Result:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
zero_root : (minpoly A x).IsRoot 0
⊢ (algebraMap A B) 0 = 0

Proof state:
case mpr
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
hx : IsIntegral A 0
⊢ (minpoly A 0).coeff 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0

Tactic:
have zero_root := zero_isRoot_of_coeff_zero_eq_zero h

Result:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
zero_root : (minpoly A x).IsRoot 0
⊢ x = 0

Proof state:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
⊢ (minpoly A x).coeff 0 = 0 → x = 0

Tactic:
intro h

Result:
case mp
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0
-- Mathlib/Order/SupIndep.lean
theorem SupIndep.image [DecidableEq ι] {s : Finset ι'} {g : ι' → ι}
    (hs : s.SupIndep (f ∘ g)) : (s.image g).SupIndep f

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) ((image g t).sup f)

Tactic:
rw [sup_image]

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) (t.sup (f ∘ g))

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
hit : i ∉ t
⊢ Disjoint (f i) (t.sup f)

Tactic:
rcases subset_image_iff.mp ht with ⟨t, hts, rfl⟩

Result:
case intro.intro
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
i : ι
hi : i ∈ image g s
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
hit : i ∉ image g t
⊢ Disjoint (f i) ((image g t).sup f)

Proof state:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
⊢ (image g s).SupIndep f

Tactic:
intro t ht i hi hit

Result:
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι
ht : t ⊆ image g s
i : ι
hi : i ∈ image g s
hit : i ∉ t
⊢ Disjoint (f i) (t.sup f)

Proof state:
case intro.intro
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
i : ι
hi : i ∈ image g s
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
hit : i ∉ image g t
⊢ Disjoint (f i) ((image g t).sup f)

Tactic:
rcases mem_image.mp hi with ⟨i, his, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
s : Finset ι'
g : ι' → ι
hs : s.SupIndep (f ∘ g)
t : Finset ι'
hts : t ⊆ s
ht : image g t ⊆ image g s
i : ι'
his : i ∈ s
hi : g i ∈ image g s
hit : g i ∉ image g t
⊢ Disjoint (f (g i)) ((image g t).sup f)
-- Mathlib/Analysis/Analytic/Inverse.lean
theorem leftInv_coeff_one (p : FormalMultilinearSeries 𝕜 E F) (i : E ≃L[𝕜] F) (x : E) :
    p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm i.symm

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
i : E ≃L[𝕜] F
x : E
⊢ p.leftInv i x 1 = (continuousMultilinearCurryFin1 𝕜 F E).symm ↑i.symm

Tactic:
rw [leftInv]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem measureUnivNNReal_pos [IsFiniteMeasure μ] (hμ : μ ≠ 0) : 0 < measureUnivNNReal μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
⊢ 0 < measureUnivNNReal μ

Tactic:
contrapose! hμ

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
hμ : measureUnivNNReal μ ≤ 0
⊢ μ = 0

Tactic:
simpa [measureUnivNNReal_eq_zero, Nat.le_zero] using hμ

Result:
no goals
-- Mathlib/Algebra/Lie/Submodule.lean
theorem inclusion_injective {I₁ I₂ : LieIdeal R L} (h : I₁ ≤ I₂) :
    Function.Injective (inclusion h) :=
  fun x y ↦ by
  simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I₁ I₂ : LieIdeal R L
h : I₁ ≤ I₂
x y : ↥I₁
⊢ (inclusion h) x = (inclusion h) y → x = y

Tactic:
simp only [inclusion_apply, imp_self, Subtype.mk_eq_mk, SetLike.coe_eq_coe]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToSimpleFunc_neg (T : Set α → E →L[ℝ] F) (h_add : FinMeasAdditive μ T) {f : α →ₛ E}
    (hf : Integrable f μ) : setToSimpleFunc T (-f) = -setToSimpleFunc T f :=
  calc
    setToSimpleFunc T (-f) = setToSimpleFunc T (f.map Neg.neg) := rfl
    _ = -setToSimpleFunc T f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ setToSimpleFunc T (map Neg.neg f) = -setToSimpleFunc T f

Tactic:
rw [map_setToSimpleFunc T h_add hf neg_zero, setToSimpleFunc, ← sum_neg_distrib]

Result:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = ∑ x ∈ f.range, -(T (⇑f ⁻¹' {x})) x

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
T : Set α → E →L[ℝ] F
h_add : FinMeasAdditive μ T
f : α →ₛ E
hf : Integrable (⇑f) μ
⊢ ∑ x ∈ f.range, (T (⇑f ⁻¹' {x})) (-x) = ∑ x ∈ f.range, -(T (⇑f ⁻¹' {x})) x

Tactic:
exact Finset.sum_congr rfl fun x _ => ContinuousLinearMap.map_neg _ _

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem DvdNotUnit.not_associated [CancelCommMonoidWithZero M] {p q : M} (h : DvdNotUnit p q) :
    ¬Associated p q

Proof state:
case intro.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : p * ↑a = p * x
⊢ False

Tactic:
rcases (mul_right_inj' hp).mp hx' with rfl

Result:
case intro.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False

Proof state:
case intro.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
hp : p ≠ 0
hx : ¬IsUnit ↑a
hx' : p * ↑a = p * ↑a
⊢ False

Tactic:
exact hx a.isUnit

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p q : M
h : DvdNotUnit p q
⊢ ¬p ~ᵤ q

Tactic:
rintro ⟨a, rfl⟩

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
h : DvdNotUnit p (p * ↑a)
⊢ False

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
h : DvdNotUnit p (p * ↑a)
⊢ False

Tactic:
obtain ⟨hp, x, hx, hx'⟩ := h

Result:
case intro.intro.intro.intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p : M
a : Mˣ
hp : p ≠ 0
x : M
hx : ¬IsUnit x
hx' : p * ↑a = p * x
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean
theorem pi_mul_cot_pi_q_exp (z : ℍ) :
    π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n

Proof state:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * (2 * ∑' (i : ℕ), cexp (2 * ↑π * I * ↑z) ^ i - 1) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
ring

Result:
no goals

Proof state:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ ↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
rw [cot_pi_eq_exp_ratio, h1, one_div, (tsum_geometric_of_norm_lt_one
  (UpperHalfPlane.norm_exp_two_pi_I_lt_one z)).symm, add_comm, geom_series_mul_one_add
    (Complex.exp (2 * π * I * (z : ℂ))) (UpperHalfPlane.norm_exp_two_pi_I_lt_one _)]

Result:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ -↑π * I * (2 * ∑' (i : ℕ), cexp (2 * ↑π * I * ↑z) ^ i - 1) =
    ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Proof state:
z : ℍ
⊢ ↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Tactic:
have h1 : π * ((exp (2 * π * I * z) + 1) / (I * (1 - exp (2 * π * I * z)))) =
    -π * I * ((exp (2 * π * I * z) + 1) * (1 / (1 - exp (2 * π * I * z)))) := by
  simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]
  ring

Result:
z : ℍ
h1 :
  ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))
⊢ ↑π * (↑π * ↑z).cot = ↑π * I - 2 * ↑π * I * ∑' (n : ℕ), cexp (2 * ↑π * I * ↑z) ^ n

Proof state:
z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) * I * (1 - cexp (2 * ↑π * I * ↑z))⁻¹) =
    ↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 - cexp (2 * ↑π * I * ↑z))⁻¹)

Tactic:
ring

Result:
no goals

Proof state:
z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) / (I * (1 - cexp (2 * ↑π * I * ↑z)))) =
    -↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 / (1 - cexp (2 * ↑π * I * ↑z))))

Tactic:
simp only [div_mul_eq_div_mul_one_div, div_I, one_div, neg_mul, mul_neg, neg_inj]

Result:
z : ℍ
⊢ ↑π * ((cexp (2 * ↑π * I * ↑z) + 1) * I * (1 - cexp (2 * ↑π * I * ↑z))⁻¹) =
    ↑π * I * ((cexp (2 * ↑π * I * ↑z) + 1) * (1 - cexp (2 * ↑π * I * ↑z))⁻¹)
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_top [OrderTop α] [Fintype α] : Iic (⊤ : α) = univ

Proof state:
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
⊢ Iic ⊤ = univ

Tactic:
ext a

Result:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
a : α
⊢ a ∈ Iic ⊤ ↔ a ∈ univ

Proof state:
case h
α : Type u_2
inst✝³ : Preorder α
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : OrderTop α
inst✝ : Fintype α
a : α
⊢ a ∈ Iic ⊤ ↔ a ∈ univ

Tactic:
simp only [mem_Iic, le_top, mem_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/System/Platform.lean
theorem numBits_le : numBits ≤ 64

Proof state:
⊢ numBits ≤ 64

Tactic:
cases numBits_eq <;> next h => simp [h]

Result:
no goals

Proof state:
h : numBits = 64
⊢ numBits ≤ 64

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
lemma exists_iff_succAbove {P : Fin (n + 1) → Prop} (p : Fin (n + 1)) :
    (∃ i, P i) ↔ P p ∨ ∃ i, P (p.succAbove i) where
  mp

Proof state:
case intro.x
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
exact .inl hi

Result:
no goals

Proof state:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (∃ i, P i) → P p ∨ ∃ i, P (p.succAbove i)

Tactic:
rintro ⟨i, hi⟩

Result:
case intro
n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
⊢ P p ∨ ∃ i, P (p.succAbove i)

Proof state:
case intro.p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
exact .inr ⟨_, hi⟩

Result:
no goals

Proof state:
case intro
n : ℕ
P : Fin (n + 1) → Prop
p i : Fin (n + 1)
hi : P i
⊢ P p ∨ ∃ i, P (p.succAbove i)

Tactic:
induction' i using p.succAboveCases

Result:
case intro.x
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
hi : P p
⊢ P p ∨ ∃ i, P (p.succAbove i)

case intro.p
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
j✝ : Fin n
hi : P (p.succAbove j✝)
⊢ P p ∨ ∃ i, P (p.succAbove i)

Proof state:
n : ℕ
P : Fin (n + 1) → Prop
p : Fin (n + 1)
⊢ (P p ∨ ∃ i, P (p.succAbove i)) → ∃ i, P i

Tactic:
rintro (h | ⟨i, hi⟩) <;> exact ⟨_, ‹_›⟩

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem mul_smul' (x y : GL(2, ℝ)⁺) (z : ℍ) : smulAux (x * y) z = smulAux x (smulAux y z)

Proof state:
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ smulAux (x * y) z = smulAux x (smulAux y z)

Tactic:
ext1

Result:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ↑(smulAux (x * y) z) = ↑(smulAux x (smulAux y z))

Proof state:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z / denom (x * y) z = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)

Tactic:
rw [denom_cocycle]

Result:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z / (denom x (smulAux y z) * denom y z) =
    (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)

Proof state:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ↑(smulAux (x * y) z) = ↑(smulAux x (smulAux y z))

Tactic:
change _ / _ = (_ * (_ / _) + _) / _

Result:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z / denom (x * y) z = (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)

Proof state:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ((↑(↑↑x 0 0) * ↑(↑↑y 0 0) + ↑(↑↑x 0 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 0 0) * ↑(↑↑y 0 1) + ↑(↑↑x 0 1) * ↑(↑↑y 1 1))) *
      ((↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)) * (↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1))) =
    (↑(↑↑x 0 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 0 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))) *
      ((↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1)) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)))

Tactic:
ring

Result:
no goals

Proof state:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z / (denom x (smulAux y z) * denom y z) =
    (↑(↑↑x 0 0) * (num y z / denom y z) + ↑(↑↑x 0 1)) / denom x (smulAux y z)

Tactic:
field_simp [denom_ne_zero]

Result:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z * (denom y z * denom x (smulAux y z)) =
    (↑(↑↑x 0 0) * num y z + ↑(↑↑x 0 1) * denom y z) * (denom x (smulAux y z) * denom y z)

Proof state:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ num (x * y) z * (denom y z * denom x (smulAux y z)) =
    (↑(↑↑x 0 0) * num y z + ↑(↑↑x 0 1) * denom y z) * (denom x (smulAux y z) * denom y z)

Tactic:
simp only [num, Subgroup.coe_mul, Fin.isValue, Units.val_mul, mul_apply, Fin.sum_univ_succ,
  Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one,
  Complex.ofReal_add, Complex.ofReal_mul, denom]

Result:
case h
x y : ↥GL(2, ℝ)⁺
z : ℍ
⊢ ((↑(↑↑x 0 0) * ↑(↑↑y 0 0) + ↑(↑↑x 0 1) * ↑(↑↑y 1 0)) * ↑z + (↑(↑↑x 0 0) * ↑(↑↑y 0 1) + ↑(↑↑x 0 1) * ↑(↑↑y 1 1))) *
      ((↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)) * (↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1))) =
    (↑(↑↑x 0 0) * (↑(↑↑y 0 0) * ↑z + ↑(↑↑y 0 1)) + ↑(↑↑x 0 1) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1))) *
      ((↑(↑↑x 1 0) * ↑(smulAux y z) + ↑(↑↑x 1 1)) * (↑(↑↑y 1 0) * ↑z + ↑(↑↑y 1 1)))
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Perm.lean
theorem Perm.union_right {l₁ l₂ : List α} (t₁ : List α) (h : l₁ ~ l₂) : l₁ ∪ t₁ ~ l₂ ∪ t₁

Proof state:
case swap
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
x✝ y✝ : α
l✝ : List α
⊢ y✝ :: x✝ :: l✝ ∪ t₁ ~ x✝ :: y✝ :: l✝ ∪ t₁

Tactic:
apply perm_insert_swap

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
a : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : l₁✝ ∪ t₁ ~ l₂✝ ∪ t₁
⊢ a :: l₁✝ ∪ t₁ ~ a :: l₂✝ ∪ t₁

Tactic:
exact ih.insert a

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
h : l₁ ~ l₂
⊢ l₁ ∪ t₁ ~ l₂ ∪ t₁

Tactic:
induction h with
| nil => rfl
| cons a _ ih => exact ih.insert a
| swap => apply perm_insert_swap
| trans _ _ ih_1 ih_2 => exact ih_1.trans ih_2

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t₁ : List α
⊢ [] ∪ t₁ ~ [] ∪ t₁

Tactic:
rfl

Result:
no goals

Proof state:
case trans
α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih_1 : l₁✝ ∪ t₁ ~ l₂✝ ∪ t₁
ih_2 : l₂✝ ∪ t₁ ~ l₃✝ ∪ t₁
⊢ l₁✝ ∪ t₁ ~ l₃✝ ∪ t₁

Tactic:
exact ih_1.trans ih_2

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mulVec_stdBasisMatrix [NonUnitalNonAssocSemiring α] [Fintype m]
    (i : n) (j : m) (c : α) (x : m → α) :
    mulVec (stdBasisMatrix i j c) x = Function.update (0 : n → α) i (c * x j)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ stdBasisMatrix i j c *ᵥ x = Function.update 0 i (c * x j)

Tactic:
ext i'

Result:
case h
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (stdBasisMatrix i j c *ᵥ x) i' = Function.update 0 i (c * x j) i'

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (stdBasisMatrix i j c *ᵥ x) i' = Function.update 0 i (c * x j) i'

Tactic:
simp [stdBasisMatrix, mulVec, dotProduct]

Result:
case h
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
⊢ (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'

Tactic:
rcases eq_or_ne i i' with rfl|h

Result:
case h.inl
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i

case h.inr
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'

Proof state:
case h.inr
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
i' : n
h : i ≠ i'
⊢ (∑ x_1 : m, if i = i' ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i'

Tactic:
simp [h, h.symm]

Result:
no goals

Proof state:
case h.inl
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
i : n
j : m
c : α
x : m → α
⊢ (∑ x_1 : m, if i = i ∧ j = x_1 then c * x x_1 else 0) = Function.update 0 i (c * x j) i

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem succ_one : succ (1 : Ordinal) = 2

Proof state:
case e_a

⊢ 1 = Nat.unaryCast 1

Tactic:
simp only [Nat.unaryCast, zero_add]

Result:
no goals

Proof state:
⊢ succ 1 = 2

Tactic:
congr

Result:
case e_a

⊢ 1 = Nat.unaryCast 1