harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gaussian/GaussianIntegral.lean
theorem integrable_cexp_neg_mul_sq {b : ℂ} (hb : 0 < b.re) :
    Integrable fun x : ℝ => cexp (-b * (x : ℂ) ^ 2)

Proof state:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a => ‖cexp (-b * ↑a ^ 2)‖) volume

Tactic:
simp_rw [norm_cexp_neg_mul_sq]

Result:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a => rexp (-b.re * a ^ 2)) volume

Proof state:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x => cexp (-b * ↑x ^ 2)) volume

Tactic:
rw [← hasFiniteIntegral_norm_iff]

Result:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a => ‖cexp (-b * ↑a ^ 2)‖) volume

Proof state:
b : ℂ
hb : 0 < b.re
⊢ Integrable (fun x => cexp (-b * ↑x ^ 2)) volume

Tactic:
refine ⟨(Complex.continuous_exp.comp
  (continuous_const.mul (continuous_ofReal.pow 2))).aestronglyMeasurable, ?_⟩

Result:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun x => cexp (-b * ↑x ^ 2)) volume

Proof state:
b : ℂ
hb : 0 < b.re
⊢ HasFiniteIntegral (fun a => rexp (-b.re * a ^ 2)) volume

Tactic:
exact (integrable_exp_neg_mul_sq hb).2

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma _root_.RootSystem.reflection_perm_eq_reflection_perm_iff (P : RootSystem ι R M N) (i j : ι) :
    P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j

Proof state:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.reflection i) x = (P.reflection j) x

Tactic:
exact (P.reflection_perm_eq_reflection_perm_iff_of_span i j).mp h x <| by simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
⊢ P.reflection_perm i = P.reflection_perm j ↔ P.reflection i = P.reflection j

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Equiv.ext fun k ↦ P.root.injective <| by simp [h]⟩

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
⊢ P.reflection i = P.reflection j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
⊢ x ∈ span R (range ⇑P.root)

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
⊢ P.reflection i = P.reflection j

Tactic:
ext x

Result:
case h
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection_perm i = P.reflection_perm j
x : M
⊢ (P.reflection i) x = (P.reflection j) x

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootSystem ι R M N
i j : ι
h : P.reflection i = P.reflection j
k : ι
⊢ P.root ((P.reflection_perm i) k) = P.root ((P.reflection_perm j) k)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Convex/EGauge.lean
lemma egauge_zero_zero : egauge 𝕜 (0 : Set E) 0 = 0

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
⊢ egauge 𝕜 0 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem natDegree_smul_of_smul_regular {S : Type*} [Monoid S] [DistribMulAction S R] {k : S}
    (p : R[X]) (h : IsSMulRegular R k) : (k • p).natDegree = p.natDegree

Proof state:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0

Tactic:
contrapose! hp

Result:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0

Proof state:
case pos
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ (k • p).natDegree = p.natDegree

Tactic:
simp [hp]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).natDegree = p.natDegree

Tactic:
rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree hp, ← degree_eq_natDegree,
  degree_smul_of_smul_regular p h]

Result:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ k • p ≠ 0

Proof state:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = k • 0
⊢ p = 0

Tactic:
exact h.polynomial hp

Result:
no goals

Proof state:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = 0
⊢ p = 0

Tactic:
rw [← smul_zero k] at hp

Result:
case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : k • p = k • 0
⊢ p = 0

Proof state:
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
⊢ (k • p).natDegree = p.natDegree

Tactic:
by_cases hp : p = 0

Result:
case pos
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : p = 0
⊢ (k • p).natDegree = p.natDegree

case neg
R : Type u
inst✝² : Semiring R
S : Type u_1
inst✝¹ : Monoid S
inst✝ : DistribMulAction S R
k : S
p : R[X]
h : IsSMulRegular R k
hp : ¬p = 0
⊢ (k • p).natDegree = p.natDegree
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem ext {χ χ' : MulChar R R'} (h : ∀ a : Rˣ, χ a = χ' a) : χ = χ'

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
⊢ χ a = χ' a

Tactic:
by_cases ha : IsUnit a

Result:
case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : IsUnit a
⊢ χ a = χ' a

case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : ¬IsUnit a
⊢ χ a = χ' a

Proof state:
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ χ = χ'

Tactic:
apply ext'

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ ∀ (a : R), χ a = χ' a

Proof state:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
⊢ ∀ (a : R), χ a = χ' a

Tactic:
intro a

Result:
case h
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
⊢ χ a = χ' a

Proof state:
case neg
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : ¬IsUnit a
⊢ χ a = χ' a

Tactic:
rw [map_nonunit χ ha, map_nonunit χ' ha]

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝¹ : CommMonoid R
R' : Type u_2
inst✝ : CommMonoidWithZero R'
χ χ' : MulChar R R'
h : ∀ (a : Rˣ), χ ↑a = χ' ↑a
a : R
ha : IsUnit a
⊢ χ a = χ' a

Tactic:
exact h ha.unit

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Basic.lean
theorem epimorphisms.iff : (epimorphisms C) f ↔ Epi f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
⊢ epimorphisms C f ↔ Epi f

Tactic:
rfl

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
@[simp]
lemma moment_zero_measure : moment X p (0 : Measure Ω) = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
p : ℕ
⊢ moment X p 0 = 0

Tactic:
simp [moment]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Ideal.lean
theorem FG.map {R S : Type*} [Semiring R] [Semiring S] {I : Ideal R} (h : I.FG) (f : R →+* S) :
    (I.map f).FG

Proof state:
case intro
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ span ↑(Finset.image (⇑f) s) = Ideal.map f I

Tactic:
rw [Finset.coe_image, ← Ideal.map_span, hs]

Result:
no goals

Proof state:
case intro
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ (Ideal.map f I).FG

Tactic:
refine ⟨s.image f, ?_⟩

Result:
case intro
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ span ↑(Finset.image (⇑f) s) = Ideal.map f I

Proof state:
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ (Ideal.map f I).FG

Tactic:
classical
  obtain ⟨s, hs⟩ := h
  refine ⟨s.image f, ?_⟩
  rw [Finset.coe_image, ← Ideal.map_span, hs]

Result:
no goals

Proof state:
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
h : I.FG
f : R →+* S
⊢ (Ideal.map f I).FG

Tactic:
obtain ⟨s, hs⟩ := h

Result:
case intro
R : Type u_3
S : Type u_4
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R →+* S
s : Finset R
hs : span ↑s = I
⊢ (Ideal.map f I).FG
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_add [Fintype n] (A : Matrix m n α) (x y : n → α) :
    A *ᵥ (x + y) = A *ᵥ x + A *ᵥ y

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

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x + y)) x✝ = (A *ᵥ x + A *ᵥ y) x✝

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x y : n → α
x✝ : m
⊢ (A *ᵥ (x + y)) x✝ = (A *ᵥ x + A *ᵥ y) x✝

Tactic:
apply dotProduct_add

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
lemma map_inr :
    (H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫
      (mapHomologicalComplexIso φ H).hom =
    inr ((Functor.mapHomologicalComplex H (ComplexShape.up ℤ)).map φ)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
⊢ (H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom =
    inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)

Tactic:
ext n

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom).f n =
    (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ H.map ((inr φ).f n) ≫ (mapHomologicalComplexXIso φ H n).hom =
    (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n

Tactic:
simp only [mapHomologicalComplexXIso_eq φ H n (n + 1) rfl, mappingCone.ext_to_iff _ _ _ rfl,
  Functor.mapHomologicalComplex_obj_X, mapHomologicalComplexXIso'_hom, comp_add,
  add_comp, assoc, inl_v_fst_v, comp_id, inr_f_fst_v, comp_zero, add_zero, inl_v_snd_v,
  inr_f_snd_v, zero_add, ← H.map_comp, H.map_zero, H.map_id, and_self]

Result:
no goals

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map (inr φ) ≫ (mapHomologicalComplexIso φ H).hom).f n =
    (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n

Tactic:
dsimp [mapHomologicalComplexIso]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : Preadditive D
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝² : HasHomotopyCofiber φ
H : C ⥤ D
inst✝¹ : H.Additive
inst✝ : HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)
n : ℤ
⊢ H.map ((inr φ).f n) ≫ (mapHomologicalComplexXIso φ H n).hom =
    (inr ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).f n
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Equation P) (hQ : W.Equation Q) (hPz : P z ≠ 0)
    (hQz : Q z ≠ 0) (hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2) : W.addXYZ P Q = addZ P Q •
      ![W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        W.toAffine.addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          (W.toAffine.slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
⊢ W.addXYZ P Q =
    addZ P Q •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
have hZ {n : ℕ} : IsUnit <| addZ P Q ^ n := (isUnit_addZ_of_X_ne hx).pow n

Result:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ W.addXYZ P Q =
    addZ P Q •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hP : W.Equation P
hQ : W.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ^ 2 ≠ Q x * P z ^ 2
hZ : ∀ {n : ℕ}, IsUnit (addZ P Q ^ n)
⊢ W.addXYZ P Q =
    addZ P Q •
      ![(toAffine W).addX (P x / P z ^ 2) (Q x / Q z ^ 2)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        (toAffine W).addY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3)
          ((toAffine W).slope (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (Q y / Q z ^ 3)),
        1]

Tactic:
erw [addXYZ, smul_fin3, ← addX_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel,
  ← addY_of_Z_ne_zero hP hQ hPz hQz hx, hZ.mul_div_cancel, mul_one]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/TrailingDegree.lean
theorem natTrailingDegree_eq_support_min' (h : p ≠ 0) :
    natTrailingDegree p = p.support.min' (nonempty_support_iff.mpr h)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p ≠ 0
⊢ p.natTrailingDegree = p.support.min' ⋯

Tactic:
rw [natTrailingDegree, trailingDegree, ← Finset.coe_min', ENat.some_eq_coe, ENat.toNat_coe]

Result:
no goals
-- Mathlib/CategoryTheory/LiftingProperties/Basic.lean
lemma RetractArrow.leftLiftingProperty
    {X Y Z W Z' W' : C} {g : Z ⟶ W} {g' : Z' ⟶ W'}
    (h : RetractArrow g' g) (f : X ⟶ Y) [HasLiftingProperty g f] : HasLiftingProperty g' f where
  sq_hasLift := fun {u v} sq ↦ by
    have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v)

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst✝ : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v)
⊢ sq.HasLift

Tactic:
exact
  ⟨⟨{ l := h.i.right ≫ sq'.lift
      fac_left := by
        simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc,
          Arrow.mk_left, Category.id_comp]}⟩⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst✝ : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
⊢ sq.HasLift

Tactic:
have sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v) := by simp only [Arrow.mk_left,
  Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst✝ : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v)
⊢ sq.HasLift

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst✝ : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
sq' : CommSq (h.r.left ≫ u) g f (h.r.right ≫ v)
⊢ g' ≫ h.i.right ≫ sq'.lift = u

Tactic:
simp only [← h.i_w_assoc, sq'.fac_left, h.retract_left_assoc,
  Arrow.mk_left, Category.id_comp]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X Y Z W Z' W' : C
g : Z ⟶ W
g' : Z' ⟶ W'
h : RetractArrow g' g
f : X ⟶ Y
inst✝ : HasLiftingProperty g f
u : Z' ⟶ X
v : W' ⟶ Y
sq : CommSq u g' f v
⊢ CommSq (h.r.left ≫ u) g f (h.r.right ≫ v)

Tactic:
simp only [Arrow.mk_left,
Arrow.mk_right, Category.assoc, sq.w, Arrow.w_mk_right_assoc, Arrow.mk_hom, CommSq.mk]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma add_lt_add_left [LT α] [AddLeftStrictMono α] (hx : x ≠ ⊥) :
    y < z → x + y < x + z

Proof state:
α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
hx : x ≠ ⊥
⊢ y < z → x + y < x + z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Proof state:
case intro
α : Type u
inst✝² : Add α
y z : WithBot α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x : α
⊢ y < z → ↑x + y < ↑x + z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddLeftStrictMono α
x a✝¹ a✝ : α
⊢ a✝¹ < a✝ → x + a✝¹ < x + a✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem Char.sizeOf (a : Char) : sizeOf a = a.toNat + 4

Proof state:
case mk
val✝ : UInt32
valid✝ : val✝.isValidChar
⊢ sizeOf { val := val✝, valid := valid✝ } = { val := val✝, valid := valid✝ }.toNat + 4

Tactic:
simp_arith [Char.toNat]

Result:
no goals

Proof state:
a : Char
⊢ sizeOf a = a.toNat + 4

Tactic:
cases a

Result:
case mk
val✝ : UInt32
valid✝ : val✝.isValidChar
⊢ sizeOf { val := val✝, valid := valid✝ } = { val := val✝, valid := valid✝ }.toNat + 4
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
@[simp]
lemma pairing_reflection_perm_self_right (i j : ι) :
    P.pairing i (P.reflection_perm j j) = - P.pairing i j

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ P.pairing i ((P.reflection_perm j) j) = -P.pairing i j

Tactic:
rw [pairing, ← reflection_perm_coroot, root_coroot_eq_pairing, pairing_same, two_smul,
  sub_add_cancel_left, ← toLin_toPerfectPairing, map_neg, toLin_toPerfectPairing,
  root_coroot_eq_pairing]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem udiv_zero {x : BitVec n} : x / 0#n = 0#n

Proof state:
n : Nat
x : BitVec n
⊢ x / 0#n = 0#n

Tactic:
simp [udiv_def]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem borel_eq_generateFrom_Ioi : borel α = .generateFrom (range Ioi) :=
  @borel_eq_generateFrom_Iio αᵒᵈ _ (by infer_instance : SecondCountableTopology α) _ _

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ SecondCountableTopology α

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem lcm_pos {m n : ℕ} : 0 < m → 0 < n → 0 < m.lcm n

Proof state:
m n : ℕ
⊢ 0 < m → 0 < n → 0 < m.lcm n

Tactic:
simp_rw [Nat.pos_iff_ne_zero]

Result:
m n : ℕ
⊢ m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0

Proof state:
m n : ℕ
⊢ m ≠ 0 → n ≠ 0 → m.lcm n ≠ 0

Tactic:
exact lcm_ne_zero

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma defaultRatCDF_le_one (q : ℚ) : defaultRatCDF q ≤ 1

Proof state:
q : ℚ
⊢ (if q < 0 then 0 else 1) ≤ 1

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
q : ℚ
⊢ defaultRatCDF q ≤ 1

Tactic:
unfold defaultRatCDF

Result:
q : ℚ
⊢ (if q < 0 then 0 else 1) ≤ 1
-- Mathlib/Data/Matrix/Block.lean
@[simp]
lemma toBlocks₁₁_diagonal (v : l ⊕ m → α) :
    toBlocks₁₁ (diagonal v) = diagonal (fun i => v (Sum.inl i))

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (diagonal v).toBlocks₁₁ = diagonal fun i => v (Sum.inl i)

Tactic:
unfold toBlocks₁₁

Result:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j => diagonal v (Sum.inl i) (Sum.inl j)) = diagonal fun i => v (Sum.inl i)

Proof state:
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
⊢ (of fun i j => diagonal v (Sum.inl i) (Sum.inl j)) = diagonal fun i => v (Sum.inl i)

Tactic:
funext i j

Result:
case h.h
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : l
⊢ of (fun i j => diagonal v (Sum.inl i) (Sum.inl j)) i j = diagonal (fun i => v (Sum.inl i)) i j

Proof state:
case h.h
l : Type u_1
m : Type u_2
α : Type u_12
inst✝² : DecidableEq l
inst✝¹ : DecidableEq m
inst✝ : Zero α
v : l ⊕ m → α
i j : l
⊢ of (fun i j => diagonal v (Sum.inl i) (Sum.inl j)) i j = diagonal (fun i => v (Sum.inl i)) i j

Tactic:
simp only [ne_eq, Sum.inl.injEq, of_apply, diagonal_apply]

Result:
no goals