harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EpiMono.lean
theorem SplitEpi.epi {X Y : C} {f : X ⟶ Y} (se : SplitEpi f) : Epi f :=
  { left_cancellation := fun g h w => by replace w := se.section_ ≫= w; simpa using w }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h

Tactic:
simpa using w

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : f ≫ g = f ≫ h
⊢ g = h

Tactic:
replace w := se.section_ ≫= w

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
f : X ⟶ Y
se : SplitEpi f
Z✝ : C
g h : Y ⟶ Z✝
w : se.section_ ≫ f ≫ g = se.section_ ≫ f ≫ h
⊢ g = h
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem mker_inl : mker (inl M N) = ⊥

Proof state:
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
⊢ mker (inl M N) = ⊥

Tactic:
ext x

Result:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥

Proof state:
case h
M : Type u_1
N : Type u_2
inst✝¹ : MulOneClass M
inst✝ : MulOneClass N
x : M
⊢ x ∈ mker (inl M N) ↔ x ∈ ⊥

Tactic:
simp [mem_mker]

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem strictConvexOn_of_slope_strict_mono_adjacent (hs : Convex 𝕜 s)
    (hf :
      ∀ {x y z : 𝕜},
        x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)) :
    StrictConvexOn 𝕜 s f :=
  LinearOrder.strictConvexOn_of_lt hs fun x hx z hz hxz a b ha hb hab => by
    let y := a * x + b * z
    have hxy : x < y

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b

Tactic:
rw [eq_comm, ← sub_eq_iff_eq_add] at hab

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz✝ : x < z
a b : 𝕜
ha✝ : 0 < a
hb : 0 < b
hab : 1 - b = a
y : 𝕜 := a * x + b * z
hxy : x < y
hyz : y < z
this : (f y - f x) * (z - y) < (f z - f y) * (y - x)
hxz : 0 < z - x
ha : (z - y) / (z - x) = a
⊢ (y - x) / (z - x) = b

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • x + b • z) < a • f x + b • f z

Tactic:
let y := a * x + b * z

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) < (f z - f y) / (z - y)
x : 𝕜
hx : x ∈ s
z : 𝕜
hz : z ∈ s
hxz : x < z
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
y : 𝕜 := a * x + b * z
⊢ f (a • x + b • z) < a • f x + b • f z
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
lemma cos_le_one_sub_mul_cos_sq (hx : |x| ≤ π) : cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x✝ x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
rw [abs_of_nonneg hx₀] at hx

Result:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
have := (pow_le_pow_left₀ (by positivity) this 2).trans_eq (sin_sq_eq_half_sub _)

Result:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : (x / π) ^ 2 ≤ 1 / 2 - cos (2 * (x / 2)) / 2
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ 0 ≤ x / π

Tactic:
positivity

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
have : x / π ≤ sin (x / 2) := by simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)

Result:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this : x / π ≤ sin (x / 2)
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ}, |x| ≤ π → 0 ≤ x → cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
hx₀ : ¬0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_le hx₀

Result:
no goals

Proof state:
case inr
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ}, |x| ≤ π → 0 ≤ x → cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
hx₀ : ¬0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

x✝ x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_le hx₀

Result:
x✝ x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : x ^ 2 * π⁻¹ ^ 2 ≤ 1 / 2 + cos x * (-1 / 2)
⊢ cos x ≤ 1 - x ^ 2 * π⁻¹ ^ 2 * 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ π
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
wlog hx₀ : 0 ≤ x

Result:
case inr
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ}, |x| ≤ π → 0 ≤ x → cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
hx₀ : ¬0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

x✝ x : ℝ
hx : |x| ≤ π
hx₀ : 0 ≤ x
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : (x / π) ^ 2 ≤ 1 / 2 - cos (2 * (x / 2)) / 2
⊢ cos x ≤ 1 - 2 / π ^ 2 * x ^ 2

Tactic:
ring_nf at this ⊢

Result:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
this✝ : x / π ≤ sin (x / 2)
this : x ^ 2 * π⁻¹ ^ 2 ≤ 1 / 2 + cos x * (-1 / 2)
⊢ cos x ≤ 1 - x ^ 2 * π⁻¹ ^ 2 * 2

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / π ≤ sin (x / 2)

Tactic:
simpa using mul_le_sin (x := x / 2) (by positivity) (by linarith)

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ 0 ≤ x / 2

Tactic:
positivity

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≤ π
hx₀ : 0 ≤ x
⊢ x / 2 ≤ π / 2

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ π
this : ∀ {x : ℝ}, |x| ≤ π → 0 ≤ x → cos x ≤ 1 - 2 / π ^ 2 * x ^ 2
hx₀ : ¬0 ≤ x
⊢ |(-x)| ≤ π

Tactic:
rwa [abs_neg]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/FunctorGamma.lean
theorem iff {j : ℕ} {i : Fin (j + 2)} : Isδ₀ (SimplexCategory.δ i) ↔ i = 0

Proof state:
case mp
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0

Tactic:
rintro ⟨_, h₂⟩

Result:
case mp.intro
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0

Proof state:
j : ℕ
⊢ ¬(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0

Tactic:
exact Fin.succ_ne_zero (0 : Fin (j + 1))

Result:
no goals

Proof state:
j : ℕ
⊢ (Hom.toOrderHom (SimplexCategory.δ 0)) 0 ≠ 0

Tactic:
dsimp

Result:
j : ℕ
⊢ ¬(Hom.toOrderHom (SimplexCategory.δ 0)) 0 = 0

Proof state:
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) ↔ i = 0

Tactic:
constructor

Result:
case mp
j : ℕ
i : Fin (j + 2)
⊢ Isδ₀ (SimplexCategory.δ i) → i = 0

case mpr
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)

Proof state:
case mpr
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)

Tactic:
exact ⟨rfl, by dsimp; exact Fin.succ_ne_zero (0 : Fin (j + 1))⟩

Result:
no goals

Proof state:
case mp.intro
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False

Tactic:
exact h₂ (Fin.succAbove_ne_zero_zero h)

Result:
no goals

Proof state:
case mp.intro
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
⊢ i = 0

Tactic:
by_contra h

Result:
case mp.intro
j : ℕ
i : Fin (j + 2)
left✝ : ⦋j + 1⦌.len = ⦋j⦌.len + 1
h₂ : (Hom.toOrderHom (SimplexCategory.δ i)) 0 ≠ 0
h : ¬i = 0
⊢ False

Proof state:
case mpr
j : ℕ
i : Fin (j + 2)
⊢ i = 0 → Isδ₀ (SimplexCategory.δ i)

Tactic:
rintro rfl

Result:
case mpr
j : ℕ
⊢ Isδ₀ (SimplexCategory.δ 0)
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/ENNReal.lean
lemma ENNReal.aefinStronglyMeasurable_of_aemeasurable (hf : ∫⁻ x, f x ∂μ ≠ ∞)
    (hf_meas : AEMeasurable f μ) :
    AEFinStronglyMeasurable f μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hf_meas : AEMeasurable f μ
⊢ ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ⊤

Tactic:
rwa [lintegral_congr_ae hf_meas.ae_eq_mk.symm]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hf_meas : AEMeasurable f μ
⊢ AEFinStronglyMeasurable f μ

Tactic:
refine ⟨hf_meas.mk f, ENNReal.finStronglyMeasurable_of_measurable ?_ hf_meas.measurable_mk,
  hf_meas.ae_eq_mk⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hf_meas : AEMeasurable f μ
⊢ ∫⁻ (x : α), AEMeasurable.mk f hf_meas x ∂μ ≠ ⊤
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem ofEquiv_aequiv {U : Type*} [CommRing U] [Algebra R U] (h : IsAdjoinRoot S f)
    (h' : IsAdjoinRoot U f) (e : S ≃ₐ[R] T) :
    (h.ofEquiv e).aequiv h' = e.symm.trans (h.aequiv h')

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
⊢ (h.ofEquiv e).aequiv h' = e.symm.trans (h.aequiv h')

Tactic:
ext a

Result:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ ((h.ofEquiv e).aequiv h') a = (e.symm.trans (h.aequiv h')) a

Proof state:
case h
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
f : R[X]
T : Type u_1
inst✝³ : CommRing T
inst✝² : Algebra R T
U : Type u_2
inst✝¹ : CommRing U
inst✝ : Algebra R U
h : IsAdjoinRoot S f
h' : IsAdjoinRoot U f
e : S ≃ₐ[R] T
a : T
⊢ ((h.ofEquiv e).aequiv h') a = (e.symm.trans (h.aequiv h')) a

Tactic:
rw [← (h.ofEquiv e).map_repr a, aequiv_map, AlgEquiv.trans_apply, ofEquiv_map_apply,
  e.symm_apply_apply, aequiv_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem Fin.sizeOf (a : Fin n) : sizeOf a = a.val + 1

Proof state:
n : Nat
a : Fin n
⊢ sizeOf a = ↑a + 1

Tactic:
cases a

Result:
case mk
n val✝ : Nat
isLt✝ : val✝ < n
⊢ sizeOf ⟨val✝, isLt✝⟩ = ↑⟨val✝, isLt✝⟩ + 1

Proof state:
case mk
n val✝ : Nat
isLt✝ : val✝ < n
⊢ sizeOf ⟨val✝, isLt✝⟩ = ↑⟨val✝, isLt✝⟩ + 1

Tactic:
simp_arith

Result:
no goals
-- Mathlib/Topology/Instances/CantorSet.lean
/-- The preCantor sets are closed. -/
lemma isClosed_preCantorSet (n : ℕ) : IsClosed (preCantorSet n)

Proof state:
n : ℕ
⊢ IsClosed (preCantorSet n)

Tactic:
let f := Homeomorph.mulLeft₀ (1 / 3 : ℝ) (by norm_num)

Result:
n : ℕ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
⊢ IsClosed (preCantorSet n)

Proof state:
case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x => x / 3) '' preCantorSet n)

Tactic:
simpa [f, div_eq_inv_mul] using f.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih

Result:
no goals

Proof state:
n : ℕ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
⊢ IsClosed (preCantorSet n)

Tactic:
let g := (Homeomorph.addLeft (2 : ℝ)).trans f

Result:
n : ℕ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
⊢ IsClosed (preCantorSet n)

Proof state:
case zero
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
⊢ IsClosed (preCantorSet 0)

Tactic:
exact isClosed_Icc

Result:
no goals

Proof state:
case succ.refine_2
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x => (2 + x) / 3) '' preCantorSet n)

Tactic:
simpa [g, f, div_eq_inv_mul] using g.isClosedEmbedding.isClosed_iff_image_isClosed.mp ih

Result:
no goals

Proof state:
case succ
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed (preCantorSet (n + 1))

Tactic:
refine IsClosed.union ?_ ?_

Result:
case succ.refine_1
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x => x / 3) '' preCantorSet n)

case succ.refine_2
f : ℝ ≃ₜ ℝ := Homeomorph.mulLeft₀ (1 / 3) ⋯
g : ℝ ≃ₜ ℝ := (Homeomorph.addLeft 2).trans f
n : ℕ
ih : IsClosed (preCantorSet n)
⊢ IsClosed ((fun x => (2 + x) / 3) '' preCantorSet n)

Proof state:
n : ℕ
⊢ 1 / 3 ≠ 0

Tactic:
norm_num

Result:
no goals
-- Mathlib/Algebra/Order/Group/Action.lean
lemma pow_smul_le {G : Type*} [Monoid G] {α : Type*} [Preorder α] {g : G} {a : α}
    [MulAction G α] [CovariantClass G α HSMul.hSMul LE.le]
    (h : g • a ≤ a) (n : ℕ) : g ^ n • a ≤ a

Proof state:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a

Tactic:
exact (smul_mono_right g hn).trans h

Result:
no goals

Proof state:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a

Tactic:
rw [pow_succ', mul_smul]

Result:
case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g • g ^ n • a ≤ a

Proof state:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g ^ 0 • a ≤ a

Tactic:
rw [pow_zero, one_smul]

Result:
no goals

Proof state:
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
⊢ g ^ n • a ≤ a

Tactic:
induction' n with n hn

Result:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g ^ 0 • a ≤ a

case succ
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
n : ℕ
hn : g ^ n • a ≤ a
⊢ g ^ (n + 1) • a ≤ a
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem euler_criterion_units (x : (ZMod p)ˣ) : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Proof state:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
subst hc

Result:
case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ ringChar (ZMod p) ≠ 2

Tactic:
rwa [ringChar_zmod_n]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ IsSquare x

Tactic:
rw [isSquare_iff_exists_sq x]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ ∃ r, x = r ^ 2

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ ∃ r, x = r ^ 2

Tactic:
simp_rw [eq_comm]

Result:
no goals

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
rw [hs]

Result:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1

Tactic:
rwa [card p] at h₀

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
by_cases hc : p = 2

Result:
case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x := by
  rw [isSquare_iff_exists_sq x]
  simp_rw [eq_comm]

Result:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ y, y ^ 2 = x) ↔ IsSquare x
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Proof state:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x

Result:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (p / 2) = 1

Proof state:
case pos
inst✝ : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ y, y ^ 2 = x) ↔ x ^ (2 / 2) = 1

Tactic:
simp only [eq_iff_true_of_subsingleton, exists_const]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma cyclesMap'_add :
    cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ +
      cyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
have γ : LeftHomologyMapData φ h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
have γ' : LeftHomologyMapData φ' h₁ h₂ := default

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
γ : LeftHomologyMapData φ h₁ h₂
γ' : LeftHomologyMapData φ' h₁ h₂
⊢ cyclesMap' (φ + φ') h₁ h₂ = cyclesMap' φ h₁ h₂ + cyclesMap' φ' h₁ h₂

Tactic:
simp only [γ.cyclesMap'_eq, γ'.cyclesMap'_eq,
  (γ.add γ').cyclesMap'_eq, LeftHomologyMapData.add_φK]

Result:
no goals
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk'_one (x) : f.mk' x (1 : S) = f.toMap x

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ f.toMap x * ↑1⁻¹ = f.toMap x

Tactic:
exact mul_one _

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ f.mk' x 1 = f.toMap x

Tactic:
rw [mk', MonoidHom.map_one]

Result:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x : M
⊢ f.toMap x * ↑1⁻¹ = f.toMap x
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
/-- If `s` is a non-empty open subset of `M`, every chart of `s` is the restriction
of some chart on `M`. -/
lemma chart_eq {s : Opens M} (hs : Nonempty s) {e : PartialHomeomorph s H} (he : e ∈ atlas H s) :
    ∃ x : s, e = (chartAt H (x : M)).subtypeRestr hs

Proof state:
case intro.intro.intro
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : PartialHomeomorph (↥s) H
xset : Set (PartialHomeomorph (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs

Tactic:
exact ⟨x, mem_singleton_iff.mp (by convert he)⟩

Result:
no goals

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : PartialHomeomorph (↥s) H
he : e ∈ atlas H ↥s
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs

Tactic:
rcases he with ⟨xset, ⟨x, hx⟩, he⟩

Result:
case intro.intro.intro
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : PartialHomeomorph (↥s) H
xset : Set (PartialHomeomorph (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ ∃ x, e = (chartAt H ↑x).subtypeRestr hs

Proof state:
H : Type u
M : Type u_2
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
s : Opens M
hs : Nonempty ↥s
e : PartialHomeomorph (↥s) H
xset : Set (PartialHomeomorph (↥s) H)
he : e ∈ xset
x : ↥s
hx : (fun x => {(chartAt H ↑x).subtypeRestr ⋯}) x = xset
⊢ e ∈ {(chartAt H ↑x).subtypeRestr hs}

Tactic:
convert he

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem natCast_div (m n : ℕ) : ((m / n : ℕ) : Ordinal) = m / n

Proof state:
case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
have hn' : (n : Ordinal) ≠ 0 := Nat.cast_ne_zero.2 hn

Result:
case inr
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Proof state:
case inr
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
apply le_antisymm

Result:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n

case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Proof state:
m n : ℕ
⊢ ↑(m / n) = ↑m / ↑n

Tactic:
rcases eq_or_ne n 0 with (rfl | hn)

Result:
case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

case inr
m n : ℕ
hn : n ≠ 0
⊢ ↑(m / n) = ↑m / ↑n

Proof state:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m

Tactic:
apply Nat.div_mul_le_self

Result:
no goals

Proof state:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑m / ↑n ≤ ↑(m / n)

Tactic:
rw [div_le hn', ← add_one_eq_succ, ← Nat.cast_succ, ← natCast_mul, Nat.cast_lt, mul_comm,
  ← Nat.div_lt_iff_lt_mul (Nat.pos_of_ne_zero hn)]

Result:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < (m / n).succ

Proof state:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ ↑(m / n) ≤ ↑m / ↑n

Tactic:
rw [le_div hn', ← natCast_mul, Nat.cast_le, mul_comm]

Result:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n * n ≤ m

Proof state:
case inr.a
m n : ℕ
hn : n ≠ 0
hn' : ↑n ≠ 0
⊢ m / n < (m / n).succ

Tactic:
apply Nat.lt_succ_self

Result:
no goals

Proof state:
case inl
m : ℕ
⊢ ↑(m / 0) = ↑m / ↑0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem or_all_distrib_left (l : List α) (p : α → Bool) (q : Bool) :
    (q || l.all p) = l.all fun a => q || p a

Proof state:
α : Type u_1
l : List α
p : α → Bool
q : Bool
⊢ (q || l.all p) = l.all fun a => q || p a

Tactic:
induction l with simp | cons _ _ ih => rw [Bool.or_and_distrib_left, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
q : Bool
head✝ : α
tail✝ : List α
ih : (q || tail✝.all p) = tail✝.all fun a => q || p a
⊢ (q || p head✝ && tail✝.all p) = ((q || p head✝) && tail✝.all fun a => q || p a)

Tactic:
rw [Bool.or_and_distrib_left, ih]

Result:
no goals