harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Lie/Solvable.lean
theorem coe_derivedSeries_eq_int (k : ℕ) :
    (derivedSeries R L k : Set L) = (derivedSeries ℤ L k : Set L)

Proof state:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal R L k ⊤, ∃ n ∈ derivedSeriesOfIdeal R L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
simp only [Subtype.exists, exists_prop, ih]

Result:
case succ
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) =
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Proof state:
case succ.a
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
k : ℕ
ih : ∀ (x : L), x ∈ derivedSeriesOfIdeal R L k ⊤ ↔ x ∈ derivedSeriesOfIdeal ℤ L k ⊤
⊢ ↑(Submodule.span R {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x}) ≤
    ↑(Submodule.span ℤ {x | ∃ x_1 ∈ derivedSeriesOfIdeal ℤ L k ⊤, ∃ n ∈ derivedSeriesOfIdeal ℤ L k ⊤, ⁅x_1, n⁆ = x})

Tactic:
exact coe_derivedSeries_eq_int_aux _ _ L k ih

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_one_right [MulOneClass R] [NatPowAssoc R] (r : R) : multichoose r 1 = r

Proof state:
R : Type u_1
inst✝⁴ : AddCommMonoid R
inst✝³ : Pow R ℕ
inst✝² : BinomialRing R
inst✝¹ : MulOneClass R
inst✝ : NatPowAssoc R
r : R
⊢ multichoose r 1 = r

Tactic:
rw [multichoose_one_right', npow_one]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem isUnit_of_associated_mul [CancelCommMonoidWithZero M] {p b : M} (h : Associated (p * b) p)
    (hp : p ≠ 0) : IsUnit b

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ IsUnit b

Tactic:
refine isUnit_of_mul_eq_one b a ((mul_right_inj' hp).mp ?_)

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1

Proof state:
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p b : M
h : p * b ~ᵤ p
hp : p ≠ 0
⊢ IsUnit b

Tactic:
obtain ⟨a, ha⟩ := h

Result:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ IsUnit b

Proof state:
case intro
M : Type u_1
inst✝ : CancelCommMonoidWithZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1

Tactic:
rwa [← mul_assoc, mul_one]

Result:
no goals
-- Mathlib/Probability/Process/Adapted.lean
theorem Filtration.adapted_natural [MetrizableSpace β] [mβ : MeasurableSpace β] [BorelSpace β]
    {u : ι → Ω → β} (hum : ∀ i, StronglyMeasurable[m] (u i)) :
    Adapted (Filtration.natural u hum) u

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
⊢ Adapted (natural u hum) u

Tactic:
intro i

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ StronglyMeasurable (u i)

Tactic:
rw [stronglyMeasurable_iff_measurable_separable]

Result:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))

Proof state:
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : TopologicalSpace β
inst✝² : Preorder ι
inst✝¹ : MetrizableSpace β
mβ : MeasurableSpace β
inst✝ : BorelSpace β
u : ι → Ω → β
hum : ∀ (i : ι), StronglyMeasurable (u i)
i : ι
⊢ Measurable (u i) ∧ IsSeparable (Set.range (u i))

Tactic:
exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Basic.lean
/-- If the `ChartedSpace` structure on a manifold `M` is given by an open embedding `e : M → H`,
then the inverse of `e` is `C^n`. -/
lemma contMDiffOn_isOpenEmbedding_symm [Nonempty M] :
    haveI := h.singletonChartedSpace; ContMDiffOn I I
      n (IsOpenEmbedding.toPartialHomeomorph e h).symm (range e)

Proof state:
case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝ : IsManifold I ω M
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
this : ↑I.symm z ∈ range e
⊢ ↑I (e (↑(IsOpenEmbedding.toPartialHomeomorph e h).symm (↑I.symm z))) = z

Tactic:
rw [h.toPartialHomeomorph_right_inv e this]

Result:
case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this✝ : IsManifold I ω M
z✝ : H
hz✝ : M
z : E
hz :
  z ∈
    (extChartAt I z✝).target ∩
      ↑(extChartAt I z✝).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz✝).source)
this : ↑I.symm z ∈ range e
⊢ ↑I (↑I.symm z) = z

Proof state:
case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
⊢ ∀ (x : H) (y : M),
    ContDiffOn 𝕜 n (↑(extChartAt I y) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I x).symm)
      ((extChartAt I x).target ∩
        ↑(extChartAt I x).symm ⁻¹'
          (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I y).source))

Tactic:
intros z hz

Result:
case right
𝕜 : 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
e : M → H
h : IsOpenEmbedding e
n : WithTop ℕ∞
inst✝ : Nonempty M
this : IsManifold I ω M
z : H
hz : M
⊢ ContDiffOn 𝕜 n (↑(extChartAt I hz) ∘ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ∘ ↑(extChartAt I z).symm)
    ((extChartAt I z).target ∩
      ↑(extChartAt I z).symm ⁻¹'
        (range e ∩ ↑(IsOpenEmbedding.toPartialHomeomorph e h).symm ⁻¹' (extChartAt I hz).source))
-- Mathlib/Data/PNat/Xgcd.lean
theorem gcdB'_coe : (gcdB' a b : ℕ) = gcdY a b + gcdZ a b

Proof state:
a b : ℕ+
⊢ (a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)

Tactic:
rw [add_assoc]

Result:
no goals

Proof state:
a b : ℕ+
⊢ ↑(a.gcdB' b) = a.gcdY b + ↑(a.gcdZ b)

Tactic:
dsimp [gcdB', gcdY, gcdZ, XgcdType.z]

Result:
a b : ℕ+
⊢ (a.xgcd b).y + (a.xgcd b).zp + 1 = (a.xgcd b).y + ((a.xgcd b).zp + 1)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_eraseKey [BEq α] [PartialEquivBEq α] [Inhabited α] {l : List ((a : α) × β a)}
    {k a : α} (hl : DistinctKeys l) :
    getKey! a (eraseKey k l) = if k == a then default else getKey! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : PartialEquivBEq α
inst✝ : Inhabited α
l : List ((a : α) × β a)
k a : α
hl : DistinctKeys l
⊢ getKey! a (eraseKey k l) = if (k == a) = true then default else getKey! a l

Tactic:
simp [getKey!_eq_getKey?, getKey?_eraseKey hl, apply_ite Option.get!]

Result:
no goals
-- Mathlib/RingTheory/Flat/Localization.lean
theorem IsLocalization.flat : Module.Flat R S

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
p : Submonoid R
inst✝ : IsLocalization p S
P : Type u_1
x✝¹ : AddCommMonoid P
x✝ : Module R P
N : Submodule R P
h : IsBaseChange S (Submodule.toLocalized' S p ((TensorProduct.mk R S P) 1) (range N.subtype))
e : S ⊗[R] ↥N ≃ₗ[R] ↥(Submodule.localized' S p ((TensorProduct.mk R S P) 1) (range N.subtype)) :=
  LinearEquiv.lTensor S (LinearEquiv.ofInjective N.subtype ⋯) ≪≫ₗ LinearEquiv.restrictScalars R h.equiv
this : lTensor S N.subtype = (Submodule.localized₀ p ((TensorProduct.mk R S P) 1) (range N.subtype)).subtype ∘ₗ ↑e
⊢ Function.Injective ⇑(lTensor S N.subtype)

Tactic:
simpa [this] using e.injective

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findIdx?_append :
    (xs ++ ys : Array α).findIdx? p =
      (xs.findIdx? p).or ((ys.findIdx? p).map fun i => i + xs.size)

Proof state:
case mk
α : Type u_1
ys : Array α
p : α → Bool
xs : List α
⊢ findIdx? p ({ toList := xs } ++ ys) =
    (findIdx? p { toList := xs }).or (Option.map (fun i => i + { toList := xs }.size) (findIdx? p ys))

Tactic:
rcases ys with ⟨ys⟩

Result:
case mk.mk
α : Type u_1
p : α → Bool
xs ys : List α
⊢ findIdx? p ({ toList := xs } ++ { toList := ys }) =
    (findIdx? p { toList := xs }).or (Option.map (fun i => i + { toList := xs }.size) (findIdx? p { toList := ys }))

Proof state:
case mk.mk
α : Type u_1
p : α → Bool
xs ys : List α
⊢ findIdx? p ({ toList := xs } ++ { toList := ys }) =
    (findIdx? p { toList := xs }).or (Option.map (fun i => i + { toList := xs }.size) (findIdx? p { toList := ys }))

Tactic:
simp [List.findIdx?_append]

Result:
no goals

Proof state:
α : Type u_1
xs ys : Array α
p : α → Bool
⊢ findIdx? p (xs ++ ys) = (findIdx? p xs).or (Option.map (fun i => i + xs.size) (findIdx? p ys))

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
ys : Array α
p : α → Bool
xs : List α
⊢ findIdx? p ({ toList := xs } ++ ys) =
    (findIdx? p { toList := xs }).or (Option.map (fun i => i + { toList := xs }.size) (findIdx? p ys))
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem exists_unit_of_abs (a : ℤ) : ∃ (u : ℤ) (_ : IsUnit u), (Int.natAbs a : ℤ) = u * a

Proof state:
case inl
a : ℤ
h : a = ↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
use 1, isUnit_one

Result:
case h
a : ℤ
h : a = ↑a.natAbs
⊢ ↑a.natAbs = 1 * a

Proof state:
case h
a : ℤ
h : a = ↑a.natAbs
⊢ ↑a.natAbs = 1 * a

Tactic:
rw [← h, one_mul]

Result:
no goals

Proof state:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ ↑a.natAbs = -1 * a

Tactic:
rw [← neg_eq_iff_eq_neg.mpr h]

Result:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ -a = -1 * a

Proof state:
a : ℤ
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
rcases natAbs_eq a with h | h

Result:
case inl
a : ℤ
h : a = ↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Proof state:
case inr
a : ℤ
h : a = -↑a.natAbs
⊢ ∃ u x, ↑a.natAbs = u * a

Tactic:
use -1, isUnit_one.neg

Result:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ ↑a.natAbs = -1 * a

Proof state:
case h
a : ℤ
h : a = -↑a.natAbs
⊢ -a = -1 * a

Tactic:
simp only [neg_mul, one_mul]

Result:
no goals
-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem IsQuadratic.comp {χ : MulChar R R'} (hχ : χ.IsQuadratic) (f : R' →+* R'') :
    (χ.ringHomComp f).IsQuadratic

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
⊢ (χ.ringHomComp f).IsQuadratic

Tactic:
intro a

Result:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1

Proof state:
R : Type u_1
inst✝² : CommMonoid R
R' : Type u_2
inst✝¹ : CommRing R'
R'' : Type u_3
inst✝ : CommRing R''
χ : MulChar R R'
hχ : χ.IsQuadratic
f : R' →+* R''
a : R
⊢ (χ.ringHomComp f) a = 0 ∨ (χ.ringHomComp f) a = 1 ∨ (χ.ringHomComp f) a = -1

Tactic:
rcases hχ a with (ha | ha | ha) <;> simp [ha]

Result:
no goals
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
lemma IsSymm.nondegenerate_restrict_of_isCompl_ker {B : M →ₗ[R] M →ₗ[R] R} (hB : B.IsSymm)
    {W : Submodule R M} (hW : IsCompl W (LinearMap.ker B)) :
    (B.domRestrict₁₂ W W).Nondegenerate

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ ⟨x, hx⟩ = 0

Tactic:
simp only [Submodule.mk_eq_zero]

Result:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ x = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ (y : ↥W), ((B.domRestrict₁₂ W W) ⟨x, hx⟩) y = 0
⊢ x = 0

Tactic:
replace hx' : ∀ y ∈ W, B x y = 0 := by simpa [Subtype.forall] using hx'

Result:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
x : M
hx : x ∈ W
hx' : ∀ y ∈ W, (B x) y = 0
⊢ x = 0

Proof state:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
⊢ (B.domRestrict₁₂ W W).Nondegenerate

Tactic:
rw [LinearMap.IsRefl.nondegenerate_iff_separatingLeft hB']

Result:
R : Type u_1
M : Type u_5
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : M →ₗ[R] M →ₗ[R] R
hB : B.IsSymm
W : Submodule R M
hW : IsCompl W (ker B)
hB' : (B.domRestrict₁₂ W W).IsRefl
⊢ (B.domRestrict₁₂ W W).SeparatingLeft
-- Mathlib/Data/Real/EReal.lean
lemma lt_div_iff (h : 0 < b) (h' : b ≠ ⊤) : a < c / b ↔ a * b < c

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c

Tactic:
rw [EReal.mul_div b a b, mul_comm a b]

Result:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ a < c / b ↔ a * b < c

Tactic:
nth_rw 1 [← @mul_div_cancel a b (ne_bot_of_gt h) h' (ne_of_gt h)]

Result:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * (a / b) < c / b ↔ a * b < c

Proof state:
a b c : EReal
h : 0 < b
h' : b ≠ ⊤
⊢ b * a / b < c / b ↔ b * a < c

Tactic:
exact (strictMono_div_right_of_pos h h').lt_iff_lt

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/LiftingProperty.lean
@[simp]
lemma rlp_retracts : T.retracts.rlp = T.rlp

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

Tactic:
exact antitone_rlp T.le_retracts

Result:
no goals

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

Tactic:
rw [← le_llp_iff_le_rlp]

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

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

Tactic:
exact T.retracts_le_llp_rlp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.retracts.rlp = T.rlp

Tactic:
apply le_antisymm

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

case a
C : Type u
inst✝ : Category.{v, u} C
T : MorphismProperty C
⊢ T.rlp ≤ T.retracts.rlp
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_image (hΦ : Isometry Φ) : infEdist (Φ x) (Φ '' t) = infEdist x t

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
inst✝ : PseudoEMetricSpace β
x : α
t : Set α
Φ : α → β
hΦ : Isometry Φ
⊢ infEdist (Φ x) (Φ '' t) = infEdist x t

Tactic:
simp only [infEdist, iInf_image, hΦ.edist_eq]

Result:
no goals
-- Mathlib/Order/Filter/Lift.lean
theorem tendsto_prod_self_iff {f : α × α → β} {x : Filter α} {y : Filter β} :
    Filter.Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ x x' : α, x ∈ U → x' ∈ U → f (x, x') ∈ W

Proof state:
α : Type u_1
β : Type u_2
f : α × α → β
x : Filter α
y : Filter β
⊢ Tendsto f (x ×ˢ x) y ↔ ∀ W ∈ y, ∃ U ∈ x, ∀ (x x' : α), x ∈ U → x' ∈ U → f (x, x') ∈ W

Tactic:
simp only [tendsto_def, mem_prod_same_iff, prod_sub_preimage_iff, exists_prop]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Flat.lean
lemma holdsForLocalizationAway : HoldsForLocalizationAway Flat

Proof state:
case h.e'_5.h.e'_5.h
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
r✝ : R
x✝ : S
⊢ (algebraMap R S) r✝ * x✝ = (algebraMap R S) r✝ * x✝

Tactic:
rfl

Result:
no goals

Proof state:
⊢ HoldsForLocalizationAway fun {R S} [CommRing R] [CommRing S] => Flat

Tactic:
introv R h

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).Flat

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Module.Flat R S

Tactic:
exact IsLocalization.flat _ (Submonoid.powers r)

Result:
no goals

Proof state:
case h.e'_5.h.e'_5.h
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Tactic:
simp_rw [Algebra.smul_def]

Result:
case h.e'_5.h.e'_5.h
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
r✝ : R
x✝ : S
⊢ (algebraMap R S) r✝ * x✝ = (algebraMap R S) r✝ * x✝

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ (algebraMap R S).Flat

Tactic:
suffices Module.Flat R S by
  rw [RingHom.Flat]; convert this; ext; simp_rw [Algebra.smul_def]; rfl

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
⊢ Module.Flat R S

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
⊢ (algebraMap R S).Flat

Tactic:
rw [RingHom.Flat]

Result:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
⊢ Module.Flat R S

Proof state:
case h.e'_5.h.e'_5
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
⊢ (algebraMap R S).toAlgebra = inst✝

Tactic:
ext

Result:
case h.e'_5.h.e'_5.h
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
r✝ : R
x✝ : S
⊢ (let_fun I := (algebraMap R S).toAlgebra;
    r✝ • x✝) =
    r✝ • x✝

Proof state:
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
⊢ Module.Flat R S

Tactic:
convert this

Result:
case h.e'_5.h.e'_5
R S : Type u_4
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
r : R
h : IsLocalization.Away r S
this : Module.Flat R S
⊢ (algebraMap R S).toAlgebra = inst✝
-- Mathlib/NumberTheory/Fermat.lean
/-- `Fₙ = 2^(2^n)+1` is prime if `3^((Fₙ - 1)/2) = -1 mod Fₙ` (**Pépin's test**). -/
lemma pepin_primality' (n : ℕ) (h : 3 ^ ((fermatNumber n - 1) / 2) = (-1 : ZMod (fermatNumber n))) :
    (fermatNumber n).Prime

Proof state:
case h.e_a
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 2 ^ (2 ^ n - 1) = (n.fermatNumber - 1) / 2

Tactic:
rw [fermatNumber, add_tsub_cancel_right, Nat.pow_div Nat.one_le_two_pow Nat.zero_lt_two]

Result:
no goals

Proof state:
case h
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = -1

Tactic:
rw [← h]

Result:
case h
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)

Proof state:
case h
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = 3 ^ ((n.fermatNumber - 1) / 2)

Tactic:
congr

Result:
case h.e_a
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 2 ^ (2 ^ n - 1) = (n.fermatNumber - 1) / 2

Proof state:
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ Prime n.fermatNumber

Tactic:
apply pepin_primality

Result:
case h
n : ℕ
h : 3 ^ ((n.fermatNumber - 1) / 2) = -1
⊢ 3 ^ 2 ^ (2 ^ n - 1) = -1
-- Mathlib/Data/Finset/Card.lean
theorem card_eq_one : #s = 1 ↔ ∃ a, s = {a}

Proof state:
α : Type u_1
s : Finset α
⊢ #s = 1 ↔ ∃ a, s = {a}

Tactic:
cases s

Result:
case mk
α : Type u_1
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ #{ val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}

Proof state:
case mk
α : Type u_1
val✝ : Multiset α
nodup✝ : val✝.Nodup
⊢ #{ val := val✝, nodup := nodup✝ } = 1 ↔ ∃ a, { val := val✝, nodup := nodup✝ } = {a}

Tactic:
simp only [Multiset.card_eq_one, Finset.card, ← val_inj, singleton_val]

Result:
no goals