harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ImageToKernel.lean
theorem imageToKernel_comp_left {Z : V} (h : Z ⟶ A) (w : f ≫ g = 0) :
    imageToKernel (h ≫ f) g (by simp [w]) =
      Subobject.ofLE _ _ (imageSubobject_comp_le h f) ≫ imageToKernel f g w

Proof state:
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g ⋯ = (imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g w

Tactic:
ext

Result:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g ⋯ ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ (h ≫ f) ≫ g = 0

Tactic:
simp [w]

Result:
no goals

Proof state:
case h
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
A B C : V
f : A ⟶ B
g : B ⟶ C
inst✝¹ : HasKernels V
inst✝ : HasImages V
Z : V
h : Z ⟶ A
w : f ≫ g = 0
⊢ imageToKernel (h ≫ f) g ⋯ ≫ (kernelSubobject g).arrow =
    ((imageSubobject (h ≫ f)).ofLE (imageSubobject f) ⋯ ≫ imageToKernel f g w) ≫ (kernelSubobject g).arrow

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.mul_right_iff : IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
⊢ IsCoprime x (y * z) ↔ IsCoprime x y ∧ IsCoprime x z

Tactic:
rw [isCoprime_comm, IsCoprime.mul_left_iff, isCoprime_comm, @isCoprime_comm _ _ z]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_left_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    Real.Angle.tan (∡ p₃ p₁ p₂) = dist p₃ p₂ / dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂

Tactic:
rw [oangle_eq_angle_of_sign_eq_one hs, angle_comm, Real.Angle.tan_coe,
  tan_angle_of_angle_eq_pi_div_two (angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two h)]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).sign = 1

Tactic:
rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ (∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂

Tactic:
have hs : (∡ p₃ p₁ p₂).sign = 1 := by rw [← oangle_rotate_sign, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
hs : (∡ p₃ p₁ p₂).sign = 1
⊢ (∡ p₃ p₁ p₂).tan = dist p₃ p₂ / dist p₁ p₂
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma sum_mul_sum {κ : Type*} (s : Finset ι) (t : Finset κ) (f : ι → α) (g : κ → α) :
    (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Proof state:
ι : Type u_1
α : Type u_3
inst✝ : NonUnitalNonAssocSemiring α
κ : Type u_7
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
⊢ (∑ i ∈ s, f i) * ∑ j ∈ t, g j = ∑ i ∈ s, ∑ j ∈ t, f i * g j

Tactic:
simp_rw [sum_mul, ← mul_sum]

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
lemma AnalyticAt.hasFPowerSeriesAt {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
    [CharZero 𝕜] {f : 𝕜 → 𝕜} {x : 𝕜} (h : AnalyticAt 𝕜 f x) :
    HasFPowerSeriesAt f
      (FormalMultilinearSeries.ofScalars 𝕜 (fun n ↦ iteratedDeriv n f x / n.factorial)) x

Proof state:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ ↑n.factorial ≠ 0

Tactic:
norm_cast

Result:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ ¬n.factorial = 0

Proof state:
case h.e'_10.intro.h.H.h
𝕜 : Type u_3
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : CompleteSpace 𝕜
inst✝ : CharZero 𝕜
f : 𝕜 → 𝕜
x : 𝕜
p : FormalMultilinearSeries 𝕜 𝕜 𝕜
r : ENNReal
hpr : HasFPowerSeriesOnBall f p x r
n : ℕ
u : Fin n → 𝕜
h_fact_smul : ∀ (n : ℕ), ↑n.factorial * p.coeff n = (iteratedFDeriv 𝕜 n f x) fun x => 1
⊢ ¬n.factorial = 0

Tactic:
exact Nat.factorial_ne_zero _

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_eq_of_cospherical_subset {s : AffineSubspace ℝ P} {ps : Set P} (h : ps ⊆ s)
    [Nonempty s] {n : ℕ} [FiniteDimensional ℝ s.direction] (hd : finrank ℝ s.direction = n)
    (hc : Cospherical ps) {sx₁ sx₂ : Simplex ℝ P n} (hsx₁ : Set.range sx₁.points ⊆ ps)
    (hsx₂ : Set.range sx₂.points ⊆ ps) : sx₁.circumcenter = sx₂.circumcenter

Proof state:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rw [hr sx₁ hsx₁, hr sx₂ hsx₂]

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
⊢ sx₁.circumcenter = sx₂.circumcenter

Tactic:
rcases exists_circumcenter_eq_of_cospherical_subset h hd hc with ⟨r, hr⟩

Result:
case intro
V : Type u_1
P : Type u_2
inst✝⁵ : NormedAddCommGroup V
inst✝⁴ : InnerProductSpace ℝ V
inst✝³ : MetricSpace P
inst✝² : NormedAddTorsor V P
s : AffineSubspace ℝ P
ps : Set P
h : ps ⊆ ↑s
inst✝¹ : Nonempty ↥s
n : ℕ
inst✝ : FiniteDimensional ℝ ↥s.direction
hd : finrank ℝ ↥s.direction = n
hc : Cospherical ps
sx₁ sx₂ : Simplex ℝ P n
hsx₁ : Set.range sx₁.points ⊆ ps
hsx₂ : Set.range sx₂.points ⊆ ps
r : P
hr : ∀ (sx : Simplex ℝ P n), Set.range sx.points ⊆ ps → sx.circumcenter = r
⊢ sx₁.circumcenter = sx₂.circumcenter
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.of_mul_monic_right (hq : q.Monic) (hpq : (p * q).Monic) : p.Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : (p * q).Monic
⊢ p.Monic

Tactic:
contrapose! hpq

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.Monic
⊢ ¬(p * q).Monic

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.Monic
⊢ ¬(p * q).Monic

Tactic:
rw [Monic.def] at hpq ⊢

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
hq : q.Monic
hpq : ¬p.leadingCoeff = 1
⊢ ¬(p * q).leadingCoeff = 1

Tactic:
rwa [leadingCoeff_mul_monic hq]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ind_mk {C : Real → Prop} (x : Real) (h : ∀ y, C (mk y)) : C x

Proof state:
C : ℝ → Prop
x : ℝ
h : ∀ (y : CauSeq ℚ abs), C (mk y)
⊢ C x

Tactic:
obtain ⟨x⟩ := x

Result:
case ofCauchy
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy abs
⊢ C { cauchy := x }

Proof state:
case ofCauchy.h
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : CauSeq ℚ abs
⊢ C { cauchy := Quot.mk (⇑equiv) x }

Tactic:
exact h x

Result:
no goals

Proof state:
case ofCauchy
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : Cauchy abs
⊢ C { cauchy := x }

Tactic:
induction' x using Quot.induction_on with x

Result:
case ofCauchy.h
C : ℝ → Prop
h : ∀ (y : CauSeq ℚ abs), C (mk y)
x : CauSeq ℚ abs
⊢ C { cauchy := Quot.mk (⇑equiv) x }
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_C (a : R) : natDegree (C a) = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ (C a).natDegree = 0

Tactic:
have : C a = 0 := by rw [ha, C_0]

Result:
case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
this : C a = 0
⊢ (C a).natDegree = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
this : C a = 0
⊢ (C a).natDegree = 0

Tactic:
rw [natDegree, degree_eq_bot.2 this, WithBot.unbotD_bot]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ C a = 0

Tactic:
rw [ha, C_0]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
a : R
⊢ (C a).natDegree = 0

Tactic:
by_cases ha : a = 0

Result:
case pos
R : Type u
inst✝ : Semiring R
a : R
ha : a = 0
⊢ (C a).natDegree = 0

case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0

Proof state:
case neg
R : Type u
inst✝ : Semiring R
a : R
ha : ¬a = 0
⊢ (C a).natDegree = 0

Tactic:
rw [natDegree, degree_C ha, WithBot.unbotD_zero]

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem evariance_lt_top_iff_memLp [IsFiniteMeasure μ] (hX : AEStronglyMeasurable X μ) :
    evariance X μ < ∞ ↔ MemLp X 2 μ where
  mp

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ⊤

Tactic:
exact evariance_eq_top hX

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → ⊤ ≤ eVar[X; μ]

Tactic:
rw [top_le_iff]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → eVar[X; μ] = ⊤

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ eVar[X; μ] < ⊤ → MemLp X 2 μ

Tactic:
contrapose!

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hX : AEStronglyMeasurable X μ
⊢ ¬MemLp X 2 μ → ⊤ ≤ eVar[X; μ]
-- Mathlib/Order/SuccPred/WithBot.lean
lemma pred_strictMono [NoMinOrder α] : StrictMono (pred : WithTop α → α)
  | (b : α), ⊤, hab => by simp
  | (a : α), (b : α), hab => Order.pred_lt_pred (by simpa using hab)

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
b : α
hab : ↑b < ⊤
⊢ (↑b).pred < ⊤.pred

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Preorder α
inst✝² : OrderTop α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
hab : ↑a < ↑b
⊢ a < b

Tactic:
simpa using hab

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem pop_mk {data : Array α} {size : data.size = n} :
    (Vector.mk data size).pop = Vector.mk data.pop (by simp [size]) := rfl

Proof state:
α : Type ?u.3119
n : Nat
data : Array α
size : data.size = n
⊢ data.pop.size = n - 1

Tactic:
simp [size]

Result:
no goals
-- Mathlib/Algebra/Field/Rat.lean
lemma den_inv_of_ne_zero {q : ℚ≥0} (hq : q ≠ 0) : q⁻¹.den = q.num

Proof state:
q : ℚ≥0
hq : q ≠ 0
⊢ q⁻¹.den = q.num

Tactic:
rw [inv_def, divNat, den, coe_mk, Rat.divInt_ofNat, ← Rat.mk_eq_mkRat _ _ (num_ne_zero.mpr hq)]

Result:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Proof state:
q : ℚ≥0
hq : q ≠ 0
⊢ (↑q.den).natAbs.Coprime q.num

Tactic:
simpa using q.coprime_num_den.symm

Result:
no goals
-- Mathlib/RingTheory/Congruence/Basic.lean
theorem coe_iInf {ι : Sort*} (f : ι → RingCon R) : ⇑(iInf f) = ⨅ i, ⇑(f i)

Proof state:
R : Type u_2
inst✝¹ : Add R
inst✝ : Mul R
ι : Sort u_3
f : ι → RingCon R
⊢ ⇑(iInf f) = ⨅ i, ⇑(f i)

Tactic:
rw [iInf, coe_sInf, ← Set.range_comp, sInf_range, Function.comp_def]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
theorem dist_iteratedFDerivWithin_one (f g : E → F) {y}
    (hsx : UniqueDiffWithinAt 𝕜 s x) (hyt : UniqueDiffWithinAt 𝕜 t y) :
    dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y)
      = dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
x : E
f g : E → F
y : E
hsx : UniqueDiffWithinAt 𝕜 s x
hyt : UniqueDiffWithinAt 𝕜 t y
⊢ dist
      ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 f s x))
      ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 g t y)) =
    dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)

Tactic:
apply (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearIsometry.postcomp.dist_map

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
x : E
f g : E → F
y : E
hsx : UniqueDiffWithinAt 𝕜 s x
hyt : UniqueDiffWithinAt 𝕜 t y
⊢ dist (iteratedFDerivWithin 𝕜 1 f s x) (iteratedFDerivWithin 𝕜 1 g t y) =
    dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)

Tactic:
simp only [iteratedFDerivWithin_succ_eq_comp_left, comp_apply,
  LinearIsometryEquiv.dist_map, iteratedFDerivWithin_zero_eq_comp,
  LinearIsometryEquiv.comp_fderivWithin, hsx, hyt]

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s t : Set E
x : E
f g : E → F
y : E
hsx : UniqueDiffWithinAt 𝕜 s x
hyt : UniqueDiffWithinAt 𝕜 t y
⊢ dist
      ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 f s x))
      ((↑{ toLinearEquiv := (continuousMultilinearCurryFin0 𝕜 E F).symm.toLinearEquiv, continuous_toFun := ⋯,
              continuous_invFun := ⋯ }).comp
        (fderivWithin 𝕜 g t y)) =
    dist (fderivWithin 𝕜 f s x) (fderivWithin 𝕜 g t y)
-- Mathlib/Topology/Order.lean
theorem TopologicalSpace.isOpen_top_iff {α} (U : Set α) : IsOpen[⊤] U ↔ U = ∅ ∨ U = univ :=
  ⟨fun h => by
    induction h with
    | basic _ h => exact False.elim h
    | univ => exact .inr rfl
    | inter _ _ _ _ h₁ h₂ =>
      rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
    | sUnion _ _ ih => exact sUnion_mem_empty_univ ih, by
      rintro (rfl | rfl)
      exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]⟩

Proof state:
case sUnion
α : Type u_2
U : Set α
S✝ : Set (Set α)
a✝ : ∀ s ∈ S✝, GenerateOpen (OrderDual.ofDual (OrderDual.ofDual ⊥)) s
ih : ∀ s ∈ S✝, s = ∅ ∨ s = univ
⊢ ⋃₀ S✝ = ∅ ∨ ⋃₀ S✝ = univ

Tactic:
exact sUnion_mem_empty_univ ih

Result:
no goals

Proof state:
α : Type u_2
U : Set α
⊢ U = ∅ ∨ U = univ → IsOpen U

Tactic:
rintro (rfl | rfl)

Result:
case inl
α : Type u_2
⊢ IsOpen ∅

case inr
α : Type u_2
⊢ IsOpen univ

Proof state:
case inl
α : Type u_2
⊢ IsOpen ∅

case inr
α : Type u_2
⊢ IsOpen univ

Tactic:
exacts [@isOpen_empty _ ⊤, @isOpen_univ _ ⊤]

Result:
no goals

Proof state:
α : Type u_2
U : Set α
h : IsOpen U
⊢ U = ∅ ∨ U = univ

Tactic:
induction h with
| basic _ h => exact False.elim h
| univ => exact .inr rfl
| inter _ _ _ _ h₁ h₂ =>
  rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp
| sUnion _ _ ih => exact sUnion_mem_empty_univ ih

Result:
no goals

Proof state:
case basic
α : Type u_2
U s✝ : Set α
h : s✝ ∈ OrderDual.ofDual (OrderDual.ofDual ⊥)
⊢ s✝ = ∅ ∨ s✝ = univ

Tactic:
exact False.elim h

Result:
no goals

Proof state:
case inter
α : Type u_2
U s✝ t✝ : Set α
a✝¹ : GenerateOpen (OrderDual.ofDual (OrderDual.ofDual ⊥)) s✝
a✝ : GenerateOpen (OrderDual.ofDual (OrderDual.ofDual ⊥)) t✝
h₁ : s✝ = ∅ ∨ s✝ = univ
h₂ : t✝ = ∅ ∨ t✝ = univ
⊢ s✝ ∩ t✝ = ∅ ∨ s✝ ∩ t✝ = univ

Tactic:
rcases h₁ with (rfl | rfl) <;> rcases h₂ with (rfl | rfl) <;> simp

Result:
no goals

Proof state:
case univ
α : Type u_2
U : Set α
⊢ univ = ∅ ∨ univ = univ

Tactic:
exact .inr rfl

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
lemma rootForm_root_self (j : ι) :
    P.RootForm (P.root j) (P.root j) = ∑ (i : ι), (P.pairing j i) * (P.pairing j i)

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
inst✝ : Fintype ι
j : ι
⊢ (P.RootForm (P.root j)) (P.root j) = ∑ i : ι, P.pairing j i * P.pairing j i

Tactic:
simp [rootForm_apply_apply]

Result:
no goals
-- Mathlib/Order/CompactlyGenerated/Basic.lean
theorem wellFoundedGT_characterisations : List.TFAE
    [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ k : α, IsCompactElement k]

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 1 → 2 := @WellFoundedGT.isSupFiniteCompact α _

Result:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFoundedGT α
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 2 → 3 := IsSupFiniteCompact.isSupClosedCompact α

Result:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFoundedGT α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 2 ↔ 4 := isSupFiniteCompact_iff_all_elements_compact α

Result:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFoundedGT α
tfae_2_iff_4 : IsSupFiniteCompact α ↔ ∀ (k : α), IsCompactElement k
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Proof state:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE

Tactic:
tfae_have 3 → 1 := IsSupClosedCompact.wellFoundedGT α

Result:
α : Type u_2
inst✝ : CompleteLattice α
tfae_1_to_2 : WellFoundedGT α → IsSupFiniteCompact α
tfae_2_to_3 : IsSupFiniteCompact α → IsSupClosedCompact α
tfae_3_to_1 : IsSupClosedCompact α → WellFoundedGT α
⊢ [WellFoundedGT α, IsSupFiniteCompact α, IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem adjugate_fin_three (A : Matrix (Fin 3) (Fin 3) α) :
    adjugate A =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1,
      -(A 0 1 * A 2 2) + A 0 2 * A 2 1,
      A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0,
      A 0 0 * A 2 2 - A 0 2 * A 2 0,
      -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0,
      -(A 0 0 * A 2 1) + A 0 1 * A 2 0,
      A 0 0 * A 1 1 - A 0 1 * A 1 0]

Proof state:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A.adjugate i j =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]

Result:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Proof state:
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
⊢ A.adjugate =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
      -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
      A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]

Tactic:
ext i j

Result:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A.adjugate i j =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Proof state:
case a
α : Type w
inst✝ : CommRing α
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ (-1) ^ (↑j + ↑i) *
      (A.submatrix j.succAbove i.succAbove 0 0 * A.submatrix j.succAbove i.succAbove 1 1 -
        A.submatrix j.succAbove i.succAbove 0 1 * A.submatrix j.succAbove i.succAbove 1 0) =
    !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1;
        -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0;
        A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
      i j

Tactic:
fin_cases i <;> fin_cases j <;> simp [updateRow, Fin.succAbove, Fin.lt_def] <;> ring

Result:
no goals