harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_dvd_norm_of_mem {I : Ideal S} {x : S} (h : x ∈ I) :
    ↑(Ideal.absNorm I) ∣ Algebra.norm ℤ x

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ ↑(absNorm I) ∣ (Algebra.norm ℤ) x

Tactic:
rw [← Int.dvd_natAbs, ← absNorm_span_singleton x, Int.natCast_dvd_natCast]

Result:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
x : S
h : x ∈ I
⊢ absNorm I ∣ absNorm (span {x})

Tactic:
exact absNorm_dvd_absNorm_of_le ((span_singleton_le_iff_mem _).mpr h)

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_add : exp (x + y) = exp x * exp y

Proof state:
x y : ℝ
⊢ rexp (x + y) = rexp x * rexp y

Tactic:
simp [exp_add, exp]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem smul'_mul {A : Type*} [Semiring A] [Algebra R A] (x : T) (p₁ p₂ : LocalizedModule S A) :
    x • p₁ * p₂ = x • (p₁ * p₂)

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
p₁ p₂ : LocalizedModule S A
⊢ x • p₁ * p₂ = x • (p₁ * p₂)

Tactic:
induction p₁, p₂ using induction_on₂ with | _ a₁ s₁ a₂ s₂ => _

Result:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ x • mk a₁ a₂ * mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)

Proof state:
case h
R : Type u
inst✝⁵ : CommSemiring R
S : Submonoid R
T : Type u_1
inst✝⁴ : CommSemiring T
inst✝³ : Algebra R T
inst✝² : IsLocalization S T
A : Type u_2
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : T
a₁ s₁ : A
a₂ s₂ : ↥S
⊢ x • mk a₁ a₂ * mk s₁ s₂ = x • (mk a₁ a₂ * mk s₁ s₂)

Tactic:
rw [mk_mul_mk, smul_def, smul_def, mk_mul_mk, mul_assoc, smul_mul_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_mk_self (f : X ⟶ Y) [Mono f] :
    (mk f).factorThru f (mk_factors_self f) = (underlyingIso f).inv

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (mk f).factorThru f ⋯ = (underlyingIso f).inv

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (mk f).factorThru f ⋯ ≫ (mk f).arrow = (underlyingIso f).inv ≫ (mk f).arrow

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
inst✝ : Mono f
⊢ (mk f).factorThru f ⋯ ≫ (mk f).arrow = (underlyingIso f).inv ≫ (mk f).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Restrict.lean
@[simp, reassoc]
lemma map_restrictFullyFaithful_unit_app (X : C) :
    iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
D' : Type u₄
inst✝ : Category.{v₄, u₄} D'
iC : C ⥤ C'
iD : D ⥤ D'
L' : C' ⥤ D'
R' : D' ⥤ C'
adj : L' ⊣ R'
hiC : iC.FullyFaithful
hiD : iD.FullyFaithful
L : C ⥤ D
R : D ⥤ C
comm1 : iC ⋙ L' ≅ L ⋙ iD
comm2 : iD ⋙ R' ≅ R ⋙ iC
X : C
⊢ iC.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).unit.app X) =
    adj.unit.app (iC.obj X) ≫ R'.map (comm1.hom.app X) ≫ comm2.hom.app (L.obj X)

Tactic:
simp [restrictFullyFaithful]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem polar_neg (f : M → N) (x y : M) : polar (-f) x y = -polar f x y

Proof state:
M : Type u_4
N : Type u_5
inst✝¹ : AddCommGroup M
inst✝ : AddCommGroup N
f : M → N
x y : M
⊢ polar (-f) x y = -polar f x y

Tactic:
simp only [polar, Pi.neg_apply, sub_eq_add_neg, neg_add]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Plus.lean
theorem plusMap_zero [Preadditive D] (P Q : Cᵒᵖ ⥤ D) : J.plusMap (0 : P ⟶ Q) = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
⊢ J.plusMap 0 = 0

Tactic:
ext : 2

Result:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (J.plusMap 0).app x✝ = NatTrans.app 0 x✝

Proof state:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
⊢ (J.plusMap 0).app x✝ = NatTrans.app 0 x✝

Tactic:
refine colimit.hom_ext (fun S => ?_)

Result:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap 0).app x✝ = colimit.ι (J.diagram P (unop x✝)) S ≫ NatTrans.app 0 x✝

Proof state:
case w.h
C : Type u
inst✝⁴ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝³ : Category.{max v u, w} D
inst✝² : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝¹ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
inst✝ : Preadditive D
P Q : Cᵒᵖ ⥤ D
x✝ : Cᵒᵖ
S : (J.Cover (unop x✝))ᵒᵖ
⊢ colimit.ι (J.diagram P (unop x✝)) S ≫ (J.plusMap 0).app x✝ = colimit.ι (J.diagram P (unop x✝)) S ≫ NatTrans.app 0 x✝

Tactic:
erw [comp_zero, colimit.ι_map, J.diagramNatTrans_zero, zero_comp]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem inl_isoPushout_hom (h : IsPushout f g inl inr) [HasPushout f g] :
    inl ≫ h.isoPushout.hom = pushout.inl _ _

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
h : IsPushout f g inl inr
inst✝ : HasPushout f g
⊢ inl ≫ h.isoPushout.hom = pushout.inl f g

Tactic:
simp [← Iso.eq_comp_inv]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_le {x y : PartENat} : withTopEquiv x ≤ withTopEquiv y ↔ x ≤ y

Proof state:
x y : PartENat
⊢ withTopEquiv x ≤ withTopEquiv y ↔ x ≤ y

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[simp]
lemma ΓIso_inv {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] (U : Y.Opens) :
    (ΓIso f U).inv = f.appLE (f.opensRange ⊓ U) (f⁻¹ᵁ U)
      (by rw [← f.image_preimage_eq_opensRange_inter, f.preimage_image_eq])

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ (ΓIso f U).inv = Scheme.Hom.appLE f (Scheme.Hom.opensRange f ⊓ U) (f ⁻¹ᵁ U) ⋯

Tactic:
simp only [ΓIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv, eqToIso.inv, eqToHom_op,
  asIso_inv, IsIso.comp_inv_eq, Iso.symm_inv, Scheme.Hom.appIso_hom', Scheme.Hom.map_appLE]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ Z : Scheme
f✝ : X✝ ⟶ Z
g : Y✝ ⟶ Z
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U : Y.Opens
⊢ f ⁻¹ᵁ U ≤ f ⁻¹ᵁ (Scheme.Hom.opensRange f ⊓ U)

Tactic:
rw [← f.image_preimage_eq_opensRange_inter, f.preimage_image_eq]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
@[simp]
lemma sum_tmul_tmul_eq {a : A} (repr : Repr R a)
    (a₁ : (i : repr.ι) → Repr R (repr.left i)) (a₂ : (i : repr.ι) → Repr R (repr.right i)) :
    ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index,
      (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i
      = ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index,
      repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a
a₁ : (i : repr.ι) → Repr R (repr.left i)
a₂ : (i : repr.ι) → Repr R (repr.right i)
⊢ ∑ i ∈ repr.index, ∑ j ∈ (a₁ i).index, (a₁ i).left j ⊗ₜ[R] (a₁ i).right j ⊗ₜ[R] repr.right i =
    ∑ i ∈ repr.index, ∑ j ∈ (a₂ i).index, repr.left i ⊗ₜ[R] (a₂ i).left j ⊗ₜ[R] (a₂ i).right j

Tactic:
simpa [(a₂ _).eq, ← (a₁ _).eq, ← TensorProduct.tmul_sum,
  TensorProduct.sum_tmul, ← repr.eq] using congr($(coassoc (R := R)) a)

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/RegularSheaves.lean
lemma equalizerCondition_w (P : Cᵒᵖ ⥤ D) {X B : C} {π : X ⟶ B} (c : PullbackCone π π) :
    P.map π.op ≫ P.map c.fst.op = P.map π.op ≫ P.map c.snd.op

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_4, u_1} C
inst✝ : Category.{u_5, u_2} D
P : Cᵒᵖ ⥤ D
X B : C
π : X ⟶ B
c : PullbackCone π π
⊢ P.map π.op ≫ P.map c.fst.op = P.map π.op ≫ P.map c.snd.op

Tactic:
simp only [← Functor.map_comp, ← op_comp, c.condition]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem run_bind [Monad m] (x : StateT σ m α) (f : α → StateT σ m β) (s : σ)
    : (x >>= f).run s = x.run s >>= λ p => (f p.1).run p.2

Proof state:
m : Type u_1 → Type u_2
σ α β : Type u_1
inst✝ : Monad m
x : StateT σ m α
f : α → StateT σ m β
s : σ
⊢ (x >>= f).run s = do
    let p ← x.run s
    (f p.fst).run p.snd

Tactic:
simp [bind, StateT.bind, run]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem ofReal_cpow_of_nonpos {x : ℝ} (hx : x ≤ 0) (y : ℂ) :
    (x : ℂ) ^ y = (-x : ℂ) ^ y * exp (π * I * y)

Proof state:
x : ℝ
hx : x ≤ 0
y : ℂ
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
rcases hx.eq_or_lt with (rfl | hlt)

Result:
case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Proof state:
case inl
y : ℂ
hx : 0 ≤ 0
⊢ ↑0 ^ y = (-↑0) ^ y * cexp (↑π * I * y)

Tactic:
rcases eq_or_ne y 0 with (rfl | hy) <;> simp [*]

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
rw [cpow_def_of_ne_zero hne, cpow_def_of_ne_zero (neg_ne_zero.2 hne), ← exp_add, ← add_mul, log,
  log, norm_neg, arg_ofReal_of_neg hlt, ← ofReal_neg, arg_ofReal_of_nonneg (neg_nonneg.2 hx),
  ofReal_zero, zero_mul, add_zero]

Result:
no goals

Proof state:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)

Tactic:
have hne : (x : ℂ) ≠ 0 := ofReal_ne_zero.mpr hlt.ne

Result:
case inr
x : ℝ
hx : x ≤ 0
y : ℂ
hlt : x < 0
hne : ↑x ≠ 0
⊢ ↑x ^ y = (-↑x) ^ y * cexp (↑π * I * y)
-- Mathlib/Order/Disjoint.lean
theorem coe_le_coe : (a : α) ≤ b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : BoundedOrder α
a b : Complementeds α
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem μ_naturalityₗ {m n m' : M} (f : m ⟶ m') (X : C) [F.LaxMonoidal]:
    (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X =
      (μ F m n).app X ≫ (F.map (f ▷ n)).app X

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X =
    (F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X = (μ F m n).app X ≫ (F.map (f ▷ n)).app X

Tactic:
rw [← tensorHom_id, ← μ_naturality₂ F f (𝟙 n) X]

Result:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
m n m' : M
f : m ⟶ m'
X : C
inst✝ : F.LaxMonoidal
⊢ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X =
    (F.map (𝟙 n)).app ((F.obj m).obj X) ≫ (F.obj n).map ((F.map f).app X) ≫ (μ F m' n).app X
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem ball_ne_none {p : Option α → Prop} : (∀ x (_ : x ≠ none), p x) ↔ ∀ x, p (some x) :=
  ⟨fun h x => h (some x) (some_ne_none x),
    fun h x hx => by
      have := h <| x.get <| ne_none_iff_isSome.1 hx
      simp [some_get] at this ⊢
      exact this⟩

Proof state:
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p (some (x.get ⋯))
⊢ p x

Tactic:
simp [some_get] at this ⊢

Result:
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p x
⊢ p x

Proof state:
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
⊢ p x

Tactic:
have := h <| x.get <| ne_none_iff_isSome.1 hx

Result:
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p (some (x.get ⋯))
⊢ p x

Proof state:
α : Type u_1
p : Option α → Prop
h : ∀ (x : α), p (some x)
x : Option α
hx : x ≠ none
this : p x
⊢ p x

Tactic:
exact this

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma eval_polynomialZ (P : Fin 3 → R) : eval P W'.polynomialZ =
    P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z
      - (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 + C W'.a₁ * X x * X y + C (2 * W'.a₃) * X y * X z -
        (C W'.a₂ * X x ^ 2 + C (2 * W'.a₄) * X x * X z + C (3 * W'.a₆) * X z ^ 2)) =
    P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2)

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P) W'.polynomialZ =
    P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2)

Tactic:
rw [polynomialZ_eq]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
P : Fin 3 → R
⊢ (eval P)
      (X y ^ 2 + C W'.a₁ * X x * X y + C (2 * W'.a₃) * X y * X z -
        (C W'.a₂ * X x ^ 2 + C (2 * W'.a₄) * X x * X z + C (3 * W'.a₆) * X z ^ 2)) =
    P y ^ 2 + W'.a₁ * P x * P y + 2 * W'.a₃ * P y * P z -
      (W'.a₂ * P x ^ 2 + 2 * W'.a₄ * P x * P z + 3 * W'.a₆ * P z ^ 2)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem flatMap_reverse {β} (l : Vector α n) (f : α → Vector β m) :
    (l.reverse.flatMap f) = (l.flatMap (reverse ∘ f)).reverse

Proof state:
case mk
α : Type u_1
m : Nat
β : Type u_2
f : α → Vector β m
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.reverse.flatMap f =
    ({ toArray := l, size_toArray := ⋯ }.flatMap (reverse ∘ f)).reverse

Tactic:
simp [Array.flatMap_reverse, Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
β : Type u_2
l : Vector α n
f : α → Vector β m
⊢ l.reverse.flatMap f = (l.flatMap (reverse ∘ f)).reverse

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
β : Type u_2
f : α → Vector β m
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.reverse.flatMap f =
    ({ toArray := l, size_toArray := ⋯ }.flatMap (reverse ∘ f)).reverse
-- Mathlib/MeasureTheory/Measure/Map.lean
@[simp] lemma mapₗ_eq_zero_iff (hf : Measurable f) : Measure.mapₗ f μ = 0 ↔ μ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : Measurable f
⊢ (mapₗ f) μ = 0 ↔ μ = 0

Tactic:
rw [mapₗ_apply_of_measurable hf, map_eq_zero_iff hf.aemeasurable]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem mapRange_zero {f : M →+ N} (hf : Continuous f) :
    mapRange (0 : VectorMeasure α M) f hf = 0

Proof state:
α : Type u_1
inst✝⁴ : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous ⇑f
⊢ mapRange 0 f hf = 0

Tactic:
ext

Result:
case h
α : Type u_1
inst✝⁴ : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange 0 f hf) i✝ = ↑0 i✝

Proof state:
case h
α : Type u_1
inst✝⁴ : MeasurableSpace α
M : Type u_3
inst✝³ : AddCommMonoid M
inst✝² : TopologicalSpace M
N : Type u_4
inst✝¹ : AddCommMonoid N
inst✝ : TopologicalSpace N
f : M →+ N
hf : Continuous ⇑f
i✝ : Set α
a✝ : MeasurableSet i✝
⊢ ↑(mapRange 0 f hf) i✝ = ↑0 i✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Raw.lean
theorem WF.insert [BEq α] [Hashable α] {m : Raw α β} {a : α} {b : β a} (h : m.WF) :
    (m.insert a b).WF

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
a : α
b : β a
h : m.WF
⊢ (m.insert a b).WF

Tactic:
simpa [Raw.insert, h.size_buckets_pos] using .insert₀ h

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Diagonal.lean
theorem pullbackDiagonalMapIso.hom_fst :
    (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ pullback.fst _ _ =
      pullback.snd _ _ ≫ pullback.fst _ _

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ fst i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
simp only [limit.lift_π, PullbackCone.mk_pt, PullbackCone.mk_π_app]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ (pullbackDiagonalMapIso f i i₁ i₂).hom ≫ fst i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)

Tactic:
delta pullbackDiagonalMapIso

Result:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
X Y : C
inst✝¹ : HasPullbacks C
U V₁ V₂ : C
f : X ⟶ Y
i : U ⟶ Y
i₁ : V₁ ⟶ pullback f i
i₂ : V₂ ⟶ pullback f i
inst✝ : HasPullback i₁ i₂
⊢ { hom := hom f i i₁ i₂, inv := inv f i i₁ i₂, hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫ fst i₁ i₂ =
    snd (diagonal f) (map (i₁ ≫ snd f i) (i₂ ≫ snd f i) f f (i₁ ≫ fst f i) (i₂ ≫ fst f i) i ⋯ ⋯) ≫
      fst (i₁ ≫ snd f i) (i₂ ≫ snd f i)
-- Mathlib/Data/Real/Hyperreal.lean
theorem isSt_trans_real {r s t : ℝ} : IsSt r s → IsSt s t → IsSt r t

Proof state:
r s t : ℝ
⊢ r = s → s = t → r = t

Tactic:
exact Eq.trans

Result:
no goals

Proof state:
r s t : ℝ
⊢ (↑r).IsSt s → (↑s).IsSt t → (↑r).IsSt t

Tactic:
rw [isSt_real_iff_eq, isSt_real_iff_eq, isSt_real_iff_eq]

Result:
r s t : ℝ
⊢ r = s → s = t → r = t
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_sUnion : ∀ {x y : PSet.{u}}, y ∈ ⋃₀ x ↔ ∃ z ∈ x, y ∈ z
  | ⟨α, A⟩, y =>
    ⟨fun ⟨⟨a, c⟩, (e : Equiv y ((A a).Func c))⟩ =>
      have : Func (A a) c ∈ mk (A a).Type (A a).Func := Mem.mk (A a).Func c
      ⟨_, Mem.mk _ _, (Mem.congr_left e).2 (by rwa [eta] at this)⟩,
      fun ⟨⟨β, B⟩, ⟨a, (e : Equiv (mk β B) (A a))⟩, ⟨b, yb⟩⟩ => by
      rw [← eta (A a)] at e
      exact
        let ⟨βt, _⟩ := e
        let ⟨c, bc⟩ := βt b
        ⟨⟨a, c⟩, yb.trans bc⟩⟩

Proof state:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (mk (A a).Type (A a).Func)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
exact
  let ⟨βt, _⟩ := e
  let ⟨c, bc⟩ := βt b
  ⟨⟨a, c⟩, yb.trans bc⟩

Result:
no goals

Proof state:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (A a)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Tactic:
rw [← eta (A a)] at e

Result:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : ∃ z ∈ mk α A, y ∈ z
β : Type u
B : β → PSet.{u}
a : (mk α A).Type
e : (mk β B).Equiv (mk (A a).Type (A a).Func)
b : (mk β B).Type
yb : y.Equiv ((mk β B).Func b)
⊢ y ∈ ⋃₀ mk α A

Proof state:
α : Type u
A : α → PSet.{u}
y : PSet.{u}
x✝ : y ∈ ⋃₀ mk α A
a : (mk α A).Type
c : ((mk α A).Func a).Type
e : y.Equiv ((A a).Func c)
this : (A a).Func c ∈ mk (A a).Type (A a).Func
⊢ (A a).Func c ∈ A (?m.21379 α A y x✝ a c e this)

Tactic:
rwa [eta] at this

Result:
no goals
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem conGen_of_con (c : Con M) : conGen c = c :=
  le_antisymm (by rw [conGen_eq]; exact sInf_le fun _ _ => id) ConGen.Rel.of

Proof state:
M : Type u_1
inst✝ : Mul M
c : Con M
⊢ sInf {s | ∀ (x y : M), c x y → s x y} ≤ c

Tactic:
exact sInf_le fun _ _ => id

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
c : Con M
⊢ conGen ⇑c ≤ c

Tactic:
rw [conGen_eq]

Result:
M : Type u_1
inst✝ : Mul M
c : Con M
⊢ sInf {s | ∀ (x y : M), c x y → s x y} ≤ c
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem map_C [NonAssocSemiring S] (a : R) (f : R →+* S) :
    ((C a).map f : HahnSeries Γ S) = C (f a)

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
⊢ (C a).map f = C (f a)

Tactic:
ext g

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : OrderedCancelAddCommMonoid Γ
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
a : R
f : R →+* S
g : Γ
⊢ ((C a).map f).coeff g = (C (f a)).coeff g

Tactic:
by_cases h : g = 0 <;> simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Iterate.lean
theorem hIterate_eq {P : Nat → Sort _} (state : ∀(i : Nat), P i)
    {n : Nat} (f : ∀(i : Fin n), P i.val → P (i.val+1)) (s : P 0)
    (init : s = state 0)
    (step : ∀(i : Fin n), f i (state i) = state (i+1)) :
    hIterate P s f = state n

Proof state:
P : Nat → Sort u_1
state : (i : Nat) → P i
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s : P 0
init : s = state 0
step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)
⊢ hIterate P s f = state n

Tactic:
apply hIterate_elim (fun i s => s = state i) f s init

Result:
P : Nat → Sort u_1
state : (i : Nat) → P i
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s : P 0
init : s = state 0
step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)
⊢ ∀ (k : Fin n) (s : P ↑k), s = state ↑k → f k s = state (↑k + 1)

Proof state:
P : Nat → Sort u_1
state : (i : Nat) → P i
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s✝ : P 0
init : s✝ = state 0
step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)
i : Fin n
s : P ↑i
s_eq : s = state ↑i
⊢ f i s = state (↑i + 1)

Tactic:
simp only [s_eq, step]

Result:
no goals

Proof state:
P : Nat → Sort u_1
state : (i : Nat) → P i
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s : P 0
init : s = state 0
step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)
⊢ ∀ (k : Fin n) (s : P ↑k), s = state ↑k → f k s = state (↑k + 1)

Tactic:
intro i s s_eq

Result:
P : Nat → Sort u_1
state : (i : Nat) → P i
n : Nat
f : (i : Fin n) → P ↑i → P (↑i + 1)
s✝ : P 0
init : s✝ = state 0
step : ∀ (i : Fin n), f i (state ↑i) = state (↑i + 1)
i : Fin n
s : P ↑i
s_eq : s = state ↑i
⊢ f i s = state (↑i + 1)