harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Action.lean
theorem smul_ae (c : G) : c • ae μ = ae μ

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
⊢ c • ae μ = ae μ

Tactic:
ext s

Result:
case h
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ s ∈ c • ae μ ↔ s ∈ ae μ

Proof state:
case h
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ s ∈ c • ae μ ↔ s ∈ ae μ

Tactic:
simp only [mem_smul_filter, preimage_smul, smul_mem_ae]

Result:
no goals
-- Mathlib/Data/Set/List.lean
theorem range_list_getD (d : α) : (range fun n : Nat => l[n]?.getD d) = insert d { x | x ∈ l } :=
  calc
    (range fun n => l[n]?.getD d) = (fun o : Option α => o.getD d) '' range (l[·]?)

Proof state:
α : Type u_1
l : List α
d : α
⊢ (range fun n => l[n]?.getD d) = (fun o => o.getD d) '' range fun x => l[x]?

Tactic:
simp only [← range_comp, Function.comp_def]

Result:
α : Type u_1
l : List α
d : α
⊢ (range fun n => l[n]?.getD d) = range fun x => l[x]?.getD d

Proof state:
α : Type u_1
l : List α
d : α
⊢ (range fun n => l[n]?.getD d) = range fun x => l[x]?.getD d

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
d : α
⊢ ((fun o => o.getD d) '' range fun x => l[x]?) = insert d {x | x ∈ l}

Tactic:
simp only [Option.getD, range_list_getElem?, image_insert_eq, image_image, image_id']

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_filter_le_left {a b : α} [DecidablePred (· ≤ a)] (hab : a < b) :
    {x ∈ Ico a b | x ≤ a} = {a}

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}

Tactic:
rw [mem_filter, mem_Ico, mem_singleton, and_right_comm, ← le_antisymm_iff, eq_comm]

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a

Proof state:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
⊢ filter (fun x => x ≤ a) (Ico a b) = {a}

Tactic:
ext x

Result:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x ∈ filter (fun x => x ≤ a) (Ico a b) ↔ x ∈ {a}

Proof state:
case h
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
a b : α
inst✝ : DecidablePred fun x => x ≤ a
hab : a < b
x : α
⊢ x = a ∧ x < b ↔ x = a

Tactic:
exact and_iff_left_of_imp fun h => h.le.trans_lt hab

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem monic_of_b_eq_one (ha : P.a = 0) (hb : P.b = 1) : P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
⊢ P.toPoly.Monic

Tactic:
nontriviality R

Result:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 1
a✝ : Nontrivial R
⊢ P.toPoly.Monic

Tactic:
rw [Monic, leadingCoeff_of_b_ne_zero ha (hb ▸ one_ne_zero), hb]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
private lemma u₄_sq : S.u₄ ^ 2 = 1

Proof state:
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
⊢ FermatLastTheoremForThreeGen.Solution.u₄ S ^ 2 = 1

Tactic:
rcases S.u₄_eq_one_or_neg_one with h | h <;> simp [h]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_finset_prod {ι : Type*} (s : Finset ι) (f : ι → MvPolynomial σ R) :
    (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (s.prod f).totalDegree ≤ ∑ i ∈ s, (f i).totalDegree

Tactic:
refine le_trans (totalDegree_multiset_prod _) ?_

Result:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (Multiset.map totalDegree (Multiset.map f s.val)).sum ≤ ∑ i ∈ s, (f i).totalDegree

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (Multiset.map totalDegree (Multiset.map f s.val)).sum ≤ ∑ i ∈ s, (f i).totalDegree

Tactic:
simp only [Multiset.map_map, comp_apply, Finset.sum_map_val, le_refl]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem IsNormal.le_set' {f o} (H : IsNormal f) (p : Set α) (p0 : p.Nonempty) (g : α → Ordinal) (b)
    (H₂ : ∀ o, b ≤ o ↔ ∀ a ∈ p, g a ≤ o) : f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

Proof state:
α : Type u_1
f : Ordinal.{u_4} → Ordinal.{u_5}
o : Ordinal.{u_5}
H : IsNormal f
p : Set α
p0 : p.Nonempty
g : α → Ordinal.{u_4}
b : Ordinal.{u_4}
H₂ : ∀ (o : Ordinal.{u_4}), b ≤ o ↔ ∀ a ∈ p, g a ≤ o
⊢ f b ≤ o ↔ ∀ a ∈ p, f (g a) ≤ o

Tactic:
simpa [H₂] using H.le_set (g '' p) (p0.image g) b

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableAt_of_isInvertible_mfderiv
    (hf : (mfderiv I I' f x).IsInvertible) : MDifferentiableAt I I' f x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hf : (mfderiv I I' f x).IsInvertible
⊢ MDifferentiableAt I I' f x

Tactic:
simp only [← mdifferentiableWithinAt_univ, ← mfderivWithin_univ] at hf ⊢

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hf : (mfderivWithin I I' f univ x).IsInvertible
⊢ MDifferentiableWithinAt I I' f univ x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
hf : (mfderivWithin I I' f univ x).IsInvertible
⊢ MDifferentiableWithinAt I I' f univ x

Tactic:
exact mdifferentiableWithinAt_of_isInvertible_mfderivWithin hf

Result:
no goals
-- Mathlib/Geometry/Manifold/Instances/Sphere.lean
theorem hasFDerivAt_stereoInvFunAux_comp_coe (v : E) :
    HasFDerivAt (stereoInvFunAux v ∘ ((↑) : (ℝ ∙ v)ᗮ → E)) (ℝ ∙ v)ᗮ.subtypeL 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
⊢ HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (Submodule.span ℝ {v})ᗮ.subtypeL 0

Tactic:
have : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((ℝ ∙ v)ᗮ.subtypeL 0) :=
  hasFDerivAt_stereoInvFunAux v

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
this : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.span ℝ {v})ᗮ.subtypeL 0)
⊢ HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (Submodule.span ℝ {v})ᗮ.subtypeL 0

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
this : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.span ℝ {v})ᗮ.subtypeL 0)
⊢ HasFDerivAt (stereoInvFunAux v ∘ Subtype.val) (Submodule.span ℝ {v})ᗮ.subtypeL 0

Tactic:
refine this.comp (0 : (ℝ ∙ v)ᗮ) (by apply ContinuousLinearMap.hasFDerivAt)

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
v : E
this : HasFDerivAt (stereoInvFunAux v) (ContinuousLinearMap.id ℝ E) ((Submodule.span ℝ {v})ᗮ.subtypeL 0)
⊢ HasFDerivAt ⇑(Submodule.span ℝ {v})ᗮ.subtypeL ?m.102770 0

Tactic:
apply ContinuousLinearMap.hasFDerivAt

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Resolution.lean
lemma cocomplex_exactAt_succ (n : ℕ) :
    I.cocomplex.ExactAt (n + 1)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ ExactAt I.cocomplex (n + 1)

Tactic:
rw [← quasiIsoAt_iff_exactAt I.ι (n + 1) (exactAt_succ_single_obj _ _)]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
Z : C
I : InjectiveResolution Z
n : ℕ
⊢ QuasiIsoAt I.ι (n + 1)
-- Mathlib/Data/Finset/BooleanAlgebra.lean
theorem compl_ne_univ_iff_nonempty (s : Finset α) : sᶜ ≠ univ ↔ s.Nonempty

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
s : Finset α
⊢ sᶜ ≠ univ ↔ s.Nonempty

Tactic:
simp [eq_univ_iff_forall, Finset.Nonempty]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/NonPreadditive.lean
theorem add_comp (X Y Z : C) (f g : X ⟶ Y) (h : Y ⟶ Z) : (f + g) ≫ h = f ≫ h + g ≫ h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : NonPreadditiveAbelian C
X Y Z : C
f g : X ⟶ Y
h : Y ⟶ Z
⊢ (f + g) ≫ h = f ≫ h + g ≫ h

Tactic:
rw [add_def, sub_comp, neg_def, sub_comp, zero_comp, add_def, neg_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Monadic.lean
theorem forM_congr [Monad m] {as bs : Vector α n} (w : as = bs)
    {f : α → m PUnit} :
    forM as f = forM bs f

Proof state:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
inst✝ : Monad m
f : α → m PUnit
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
w : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
⊢ forM { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } f =
    forM { toArray := toArray✝, size_toArray := size_toArray✝ } f

Tactic:
simp_all

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
inst✝ : Monad m
as bs : Vector α n
w : as = bs
f : α → m PUnit
⊢ forM as f = forM bs f

Tactic:
cases as <;> cases bs

Result:
case mk.mk
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
inst✝ : Monad m
f : α → m PUnit
toArray✝¹ : Array α
size_toArray✝¹ : toArray✝¹.size = n
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
w : { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } = { toArray := toArray✝, size_toArray := size_toArray✝ }
⊢ forM { toArray := toArray✝¹, size_toArray := size_toArray✝¹ } f =
    forM { toArray := toArray✝, size_toArray := size_toArray✝ } f
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
@[simp]
lemma rlp_coproducts : (coproducts.{w} T).rlp = T.rlp

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp

Tactic:
exact antitone_rlp T.le_coproducts

Result:
no goals

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Tactic:
rw [← le_llp_iff_le_rlp]

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp = T.rlp

Tactic:
apply le_antisymm

Result:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ (coproducts.{w, v, u} T).rlp ≤ T.rlp

case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ (coproducts.{w, v, u} T).rlp

Proof state:
case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ coproducts.{w, v, u} T ≤ T.rlp.llp

Tactic:
exact T.coproducts_le_llp_rlp

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma hasFPowerSeriesAt_mgf (hv : v ∈ interior (integrableExpSet X μ)) :
    HasFPowerSeriesAt (mgf X μ)
      (FormalMultilinearSeries.ofScalars ℝ
        (fun n ↦ (μ[fun ω ↦ X ω ^ n * exp (v * X ω)] : ℝ) / n !)) v

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
⊢ HasFPowerSeriesAt (mgf X μ)
    (FormalMultilinearSeries.ofScalars ℝ fun n => (∫ (x : Ω), (fun ω => X ω ^ n * rexp (v * X ω)) x ∂μ) / ↑n !) v

Tactic:
convert (analyticAt_mgf hv).hasFPowerSeriesAt

Result:
case h.e'_10.h.h.h.h.e'_8.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
e_5✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedField.toNormedSpace
x✝ : ℕ
⊢ ∫ (x : Ω), (fun ω => X ω ^ x✝ * rexp (v * X ω)) x ∂μ = iteratedDeriv x✝ (mgf X μ) v

Proof state:
case h.e'_10.h.h.h.h.e'_8.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
e_5✝ : normedAddCommGroup = NonUnitalNormedRing.toNormedAddCommGroup
he✝ : InnerProductSpace.toNormedSpace = NormedField.toNormedSpace
x✝ : ℕ
⊢ ∫ (x : Ω), (fun ω => X ω ^ x✝ * rexp (v * X ω)) x ∂μ = iteratedDeriv x✝ (mgf X μ) v

Tactic:
rw [iteratedDeriv_mgf hv]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_pos_iff {a b : EReal} : 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Proof state:
case pos_bot
x✝ : ℝ
hx : 0 < x✝
⊢ 0 < ↑x✝ * ⊥ ↔ 0 < ↑x✝ ∧ 0 < ⊥ ∨ ↑x✝ < 0 ∧ ⊥ < 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]

Result:
no goals

Proof state:
case top_zero

⊢ 0 < ⊤ * 0 ↔ 0 < ⊤ ∧ 0 < 0 ∨ ⊤ < 0 ∧ 0 < 0

Tactic:
simp

Result:
no goals

Proof state:
case symm
x✝ y✝ : EReal
h : 0 < x✝ * y✝ ↔ 0 < x✝ ∧ 0 < y✝ ∨ x✝ < 0 ∧ y✝ < 0
⊢ 0 < y✝ * x✝ ↔ 0 < y✝ ∧ 0 < x✝ ∨ y✝ < 0 ∧ x✝ < 0

Tactic:
simp [EReal.mul_comm, h, and_comm]

Result:
no goals

Proof state:
a b : EReal
⊢ 0 < a * b ↔ 0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0

Tactic:
induction a, b using EReal.induction₂_symm with
| symm h => simp [EReal.mul_comm, h, and_comm]
| top_top => simp
| top_pos _ hx => simp [EReal.top_mul_coe_of_pos hx, hx]
| top_zero => simp
| top_neg _ hx => simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]
| top_bot => simp
| pos_bot _ hx => simp [hx, EReal.coe_mul_bot_of_pos hx, le_of_lt]
| coe_coe x y => simp [← coe_mul, _root_.mul_pos_iff]
| zero_bot => simp
| neg_bot _ hx => simp [hx, EReal.coe_mul_bot_of_neg hx]
| bot_bot => simp

Result:
no goals

Proof state:
case coe_coe
x y : ℝ
⊢ 0 < ↑x * ↑y ↔ 0 < ↑x ∧ 0 < ↑y ∨ ↑x < 0 ∧ ↑y < 0

Tactic:
simp [← coe_mul, _root_.mul_pos_iff]

Result:
no goals

Proof state:
case neg_bot
x✝ : ℝ
hx : x✝ < 0
⊢ 0 < ↑x✝ * ⊥ ↔ 0 < ↑x✝ ∧ 0 < ⊥ ∨ ↑x✝ < 0 ∧ ⊥ < 0

Tactic:
simp [hx, EReal.coe_mul_bot_of_neg hx]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
hx : 0 < x✝
⊢ 0 < ⊤ * ↑x✝ ↔ 0 < ⊤ ∧ 0 < ↑x✝ ∨ ⊤ < 0 ∧ ↑x✝ < 0

Tactic:
simp [EReal.top_mul_coe_of_pos hx, hx]

Result:
no goals

Proof state:
case top_bot

⊢ 0 < ⊤ * ⊥ ↔ 0 < ⊤ ∧ 0 < ⊥ ∨ ⊤ < 0 ∧ ⊥ < 0

Tactic:
simp

Result:
no goals

Proof state:
case bot_bot

⊢ 0 < ⊥ * ⊥ ↔ 0 < ⊥ ∧ 0 < ⊥ ∨ ⊥ < 0 ∧ ⊥ < 0

Tactic:
simp

Result:
no goals

Proof state:
case zero_bot

⊢ 0 < 0 * ⊥ ↔ 0 < 0 ∧ 0 < ⊥ ∨ 0 < 0 ∧ ⊥ < 0

Tactic:
simp

Result:
no goals

Proof state:
case top_neg
x✝ : ℝ
hx : x✝ < 0
⊢ 0 < ⊤ * ↑x✝ ↔ 0 < ⊤ ∧ 0 < ↑x✝ ∨ ⊤ < 0 ∧ ↑x✝ < 0

Tactic:
simp [hx, EReal.top_mul_coe_of_neg hx, le_of_lt]

Result:
no goals

Proof state:
case top_top

⊢ 0 < ⊤ * ⊤ ↔ 0 < ⊤ ∧ 0 < ⊤ ∨ ⊤ < 0 ∧ ⊤ < 0

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem IsCycle.existsUnique_cycle_subtype {f : Perm α} (hf : IsCycle f) :
    ∃! s : { s : Cycle α // s.Nodup }, (s : Cycle α).formPerm s.prop = f

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∃! s_1, (↑s_1).formPerm ⋯ = s.formPerm hs

Tactic:
refine ⟨⟨s, hs⟩, rfl, ?_⟩

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = s.formPerm hs) y → y = ⟨s, hs⟩

Proof state:
case intro.intro.intro.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
t : Cycle α
ht : t.Nodup
ht' : (↑⟨t, ht⟩).formPerm ⋯ = s.formPerm hs
⊢ ⟨t, ht⟩ = ⟨s, hs⟩

Tactic:
simpa using hs' _ ⟨ht, ht'⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
f : Perm α
hf : f.IsCycle
⊢ ∃! s, (↑s).formPerm ⋯ = f

Tactic:
obtain ⟨s, ⟨hs, rfl⟩, hs'⟩ := hf.existsUnique_cycle

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∃! s_1, (↑s_1).formPerm ⋯ = s.formPerm hs

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
⊢ ∀ (y : { s // s.Nodup }), (fun s_1 => (↑s_1).formPerm ⋯ = s.formPerm hs) y → y = ⟨s, hs⟩

Tactic:
rintro ⟨t, ht⟩ ht'

Result:
case intro.intro.intro.mk
α : Type u_1
inst✝¹ : Finite α
inst✝ : DecidableEq α
s : Cycle α
hs : s.Nodup
hf : (s.formPerm hs).IsCycle
hs' : ∀ (y : Cycle α), (fun s_1 => ∃ (h : s_1.Nodup), s_1.formPerm h = s.formPerm hs) y → y = s
t : Cycle α
ht : t.Nodup
ht' : (↑⟨t, ht⟩).formPerm ⋯ = s.formPerm hs
⊢ ⟨t, ht⟩ = ⟨s, hs⟩
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_of_g_is_cokernel (hS : IsColimit (CokernelCofork.ofπ S.g S.zero))
    [S.HasHomology] : S.Exact

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.Exact

Tactic:
rw [exact_iff_mono_fromOpcycles]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ Mono S.fromOpcycles

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ Mono S.fromOpcycles

Tactic:
have : IsSplitMono S.fromOpcycles :=
  ⟨⟨{ retraction := hS.desc (CokernelCofork.ofπ S.pOpcycles S.f_pOpcycles)
      id := by
        rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]
        exact Cofork.IsColimit.π_desc hS }⟩⟩

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
this : IsSplitMono S.fromOpcycles
⊢ Mono S.fromOpcycles

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.g ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = S.pOpcycles

Tactic:
exact Cofork.IsColimit.π_desc hS

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
this : IsSplitMono S.fromOpcycles
⊢ Mono S.fromOpcycles

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.fromOpcycles ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = 𝟙 S.opcycles

Tactic:
rw [← cancel_epi S.pOpcycles, p_fromOpcycles_assoc, comp_id]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsColimit (CokernelCofork.ofπ S.g ⋯)
inst✝ : S.HasHomology
⊢ S.g ≫ hS.desc (CokernelCofork.ofπ S.pOpcycles ⋯) = S.pOpcycles
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_mkVector (a : α) (n i : Nat) (h : i < n) : (mkVector n a)[i] = a

Proof state:
α : Type u_1
a : α
n i : Nat
h : i < n
⊢ (mkVector n a)[i] = a

Tactic:
rw [mkVector_eq_mk_mkArray, getElem_mk]

Result:
α : Type u_1
a : α
n i : Nat
h : i < n
⊢ (mkArray n a)[i] = a

Proof state:
α : Type u_1
a : α
n i : Nat
h : i < n
⊢ (mkArray n a)[i] = a

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Prime.lean
theorem minFac_to_nat (n : PosNum) : (minFac n : ℕ) = Nat.minFac n

Proof state:
n : PosNum
⊢ ↑n * (1 + 1 + 1) < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))

Tactic:
set_option simprocs false in simp [mul_lt_mul]

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n + ↑n + 1 ≤ ↑n + ↑n + ↑n

Tactic:
simp

Result:
no goals

Proof state:
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

Tactic:
simp [← two_mul]

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n.minFac = (↑n).minFac

Tactic:
obtain - | n := n

Result:
case one

⊢ ↑one.minFac = (↑one).minFac

case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac

case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Proof state:
case one

⊢ ↑one.minFac = (↑one).minFac

Tactic:
rfl

Result:
no goals

Proof state:
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))

Tactic:
calc
  (n : ℕ) + (n : ℕ) + 1 ≤ (n : ℕ) + (n : ℕ) + (n : ℕ) := by simp
  _ = (n : ℕ) * (1 + 1 + 1) := by simp only [mul_add, mul_one]
  _ < _ := by
    set_option simprocs false in simp [mul_lt_mul]

Result:
no goals

Proof state:
case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0

Tactic:
simp [← two_mul]

Result:
no goals

Proof state:
case bit1
n : PosNum
⊢ (↑n + ↑n + 1).sqrt < ↑n + (1 + 1 + 1)

Tactic:
rw [Nat.sqrt_lt]

Result:
case bit1
n : PosNum
⊢ ↑n + ↑n + 1 < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))

Proof state:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

Tactic:
swap

Result:
case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

Proof state:
n : PosNum
⊢ ↑n * (1 + 1 + 1) < (↑n + (1 + 1 + 1)) * (↑n + (1 + 1 + 1))

Tactic:
simp [mul_lt_mul]

Result:
no goals

Proof state:
case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

Tactic:
rfl

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n + ↑n + ↑n = ↑n * (1 + 1 + 1)

Tactic:
simp only [mul_add, mul_one]

Result:
no goals

Proof state:
case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)

Tactic:
simp only [cast_one, cast_bit1]

Result:
case bit1
n : PosNum
⊢ (↑n + ↑n + 1).sqrt < ↑n + (1 + 1 + 1)

Proof state:
case bit0
a✝ : PosNum
⊢ ↑2 = 2

Tactic:
rfl

Result:
no goals

Proof state:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

Tactic:
rw [minFacAux_to_nat]

Result:
case bit1
n : PosNum
⊢ (↑n.bit1).minFacAux ↑(bit1 1) = (↑n.bit1).minFacAux 3

case bit1
n : PosNum
⊢ (↑n.bit1).sqrt < ↑n + ↑(bit1 1)

Proof state:
case bit1
n : PosNum
⊢ ↑n.bit1.minFac = (↑n.bit1).minFac

Tactic:
rw [minFac, Nat.minFac_eq, if_neg]

Result:
case bit1
n : PosNum
⊢ ↑(n.bit1.minFacAux (↑n) 1) = (↑n.bit1).minFacAux 3

case bit1.hnc
n : PosNum
⊢ ¬2 ∣ ↑n.bit1

Proof state:
case bit0
a✝ : PosNum
⊢ ↑a✝.bit0.minFac = (↑a✝.bit0).minFac

Tactic:
rw [minFac, Nat.minFac_eq, if_pos]

Result:
case bit0
a✝ : PosNum
⊢ ↑2 = 2

case bit0.hc
a✝ : PosNum
⊢ 2 ∣ ↑a✝.bit0