harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findSome?_replicate : findSome? f (replicate n a) = if n = 0 then none else f a

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
n : Nat
a : α✝¹
⊢ findSome? f (replicate n a) = if n = 0 then none else f a

Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [replicate_succ, findSome?_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case succ
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
n : Nat
⊢ findSome? f (replicate (n + 1) a) = if n + 1 = 0 then none else f a

Tactic:
simp only [replicate_succ, findSome?_cons]

Result:
case succ
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
n : Nat
⊢ (match f a with
    | some b => some b
    | none => findSome? f (replicate n a)) =
    if n + 1 = 0 then none else f a

Proof state:
case zero
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
⊢ findSome? f (replicate 0 a) = if 0 = 0 then none else f a

Tactic:
simp

Result:
no goals

Proof state:
case succ
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → Option α✝
a : α✝¹
n : Nat
⊢ (match f a with
    | some b => some b
    | none => findSome? f (replicate n a)) =
    if n + 1 = 0 then none else f a

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem mul_neg_left (xs ys : IntList) : (-xs) * ys = -(xs * ys)

Proof state:
case nil
ys : IntList
⊢ -[] * ys = -([] * ys)

Tactic:
simp

Result:
no goals

Proof state:
case cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), -xs * ys = -(xs * ys)
ys : IntList
⊢ -(x :: xs) * ys = -((x :: xs) * ys)

Tactic:
cases ys with
| nil => simp
| cons y ys => simp_all [Int.neg_mul]

Result:
no goals

Proof state:
xs ys : IntList
⊢ -xs * ys = -(xs * ys)

Tactic:
induction xs generalizing ys with
| nil => simp
| cons x xs ih =>
  cases ys with
  | nil => simp
  | cons y ys => simp_all [Int.neg_mul]

Result:
no goals

Proof state:
case cons.nil
x : Int
xs : List Int
ih : ∀ (ys : IntList), -xs * ys = -(xs * ys)
⊢ -(x :: xs) * [] = -((x :: xs) * [])

Tactic:
simp

Result:
no goals

Proof state:
case cons.cons
x : Int
xs : List Int
ih : ∀ (ys : IntList), -xs * ys = -(xs * ys)
y : Int
ys : List Int
⊢ -(x :: xs) * (y :: ys) = -((x :: xs) * (y :: ys))

Tactic:
simp_all [Int.neg_mul]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma jacobiTheta₂_undef (z : ℂ) {τ : ℂ} (hτ : im τ ≤ 0) : jacobiTheta₂ z τ = 0

Proof state:
z τ : ℂ
hτ : τ.im ≤ 0
⊢ jacobiTheta₂ z τ = 0

Tactic:
apply tsum_eq_zero_of_not_summable

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂_term b z τ

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im

Tactic:
exact not_lt.mpr hτ

Result:
no goals

Proof state:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬Summable fun b => jacobiTheta₂_term b z τ

Tactic:
rw [summable_jacobiTheta₂_term_iff]

Result:
case h
z τ : ℂ
hτ : τ.im ≤ 0
⊢ ¬0 < τ.im
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma negPart_eq_of_eq_PosPart_sub {a c : A} (hac : a = a⁺ - c) (hc : 0 ≤ c

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : autoParam (0 ≤ c) _auto✝
ha : IsSelfAdjoint a
⊢ a⁻ = c

Tactic:
nth_rw 1 [← posPart_sub_negPart a] at hac

Result:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a⁺ - a⁻ = a⁺ - c
hc : autoParam (0 ≤ c) _auto✝
ha : IsSelfAdjoint a
⊢ a⁻ = c

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : autoParam (0 ≤ c) _auto✝
⊢ a⁻ = c

Tactic:
have ha := hac.symm ▸ (posPart_nonneg a).isSelfAdjoint.sub hc.isSelfAdjoint

Result:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a = a⁺ - c
hc : autoParam (0 ≤ c) _auto✝
ha : IsSelfAdjoint a
⊢ a⁻ = c

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a c : A
hac : a⁺ - a⁻ = a⁺ - c
hc : autoParam (0 ≤ c) _auto✝
ha : IsSelfAdjoint a
⊢ a⁻ = c

Tactic:
simpa using hac

Result:
no goals
-- Mathlib/NumberTheory/SumTwoSquares.lean
theorem Nat.sq_add_sq_mul {a b x y u v : ℕ} (ha : a = x ^ 2 + y ^ 2) (hb : b = u ^ 2 + v ^ 2) :
    ∃ r s : ℕ, a * b = r ^ 2 + s ^ 2

Proof state:
a b x y u v : ℕ
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ ∃ r s, a * b = r ^ 2 + s ^ 2

Tactic:
zify at ha hb ⊢

Result:
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2

Proof state:
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2

Tactic:
obtain ⟨r, s, h⟩ := _root_.sq_add_sq_mul ha hb

Result:
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2

Proof state:
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ∃ r s, ↑a * ↑b = ↑r ^ 2 + ↑s ^ 2

Tactic:
refine ⟨r.natAbs, s.natAbs, ?_⟩

Result:
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ↑a * ↑b = ↑r.natAbs ^ 2 + ↑s.natAbs ^ 2

Proof state:
case intro.intro
a b x y u v : ℕ
ha : ↑a = ↑x ^ 2 + ↑y ^ 2
hb : ↑b = ↑u ^ 2 + ↑v ^ 2
r s : ℤ
h : ↑a * ↑b = r ^ 2 + s ^ 2
⊢ ↑a * ↑b = ↑r.natAbs ^ 2 + ↑s.natAbs ^ 2

Tactic:
simpa only [Int.natCast_natAbs, sq_abs]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
@[to_additive addMeasure_map_restrict_apply]
lemma measure_map_restrict_apply (s : Set α) {U : Set (Quotient α_mod_G)}
    (meas_U : MeasurableSet U) :
    (μ.restrict s).map π U = μ ((π ⁻¹' U) ∩ s)

Proof state:
G : Type u_1
α : Type u_3
inst✝² : Group G
inst✝¹ : MulAction G α
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
U : Set (Quotient α_mod_G)
meas_U : MeasurableSet U
⊢ (Measure.map (Quotient.mk α_mod_G) (μ.restrict s)) U = μ (Quotient.mk α_mod_G ⁻¹' U ∩ s)

Tactic:
rw [map_apply (f := π) (fun V hV ↦ measurableSet_quotient.mp hV) meas_U,
  Measure.restrict_apply (t := (Quotient.mk α_mod_G ⁻¹' U)) (measurableSet_quotient.mp meas_U)]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_pos (ha : a ≠ 0) (h'a : a ≠ ∞) (n : ℤ) : 0 < a ^ n

Proof state:
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
n : ℤ
⊢ 0 < a ^ n

Tactic:
cases n

Result:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Proof state:
case negSucc
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.negSucc a✝

Tactic:
simp only [h'a, pow_eq_top_iff, zpow_negSucc, Ne, not_false, ENNReal.inv_pos, false_and,
  not_false_eq_true]

Result:
no goals

Proof state:
case ofNat
a : ℝ≥0∞
ha : a ≠ 0
h'a : a ≠ ⊤
a✝ : ℕ
⊢ 0 < a ^ Int.ofNat a✝

Tactic:
simpa using ENNReal.pow_pos ha.bot_lt _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insertMany_list_of_mem [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} {fallback : β k'}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).getD k' fallback = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
fallback : β k'
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).getD k' fallback = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.getD_insertMany_list_of_mem

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
lemma extChartAt_mem_closure_interior {x₀ x : M}
    (hx : x ∈ closure (interior s)) (h'x : x ∈ (extChartAt I x₀).source) :
    extChartAt I x₀ x ∈
      closure (interior ((extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ↑(extChartAt I x₀) x ∈ closure (interior (↑(extChartAt I x₀).symm ⁻¹' s ∩ (extChartAt I x₀).target))

Tactic:
simp_rw [mem_closure_iff, interior_inter, ← inter_assoc]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
y : M
ys : y ∈ interior s
yo : y ∈ ↑(extChartAt I x₀) ⁻¹' o
hy : y ∈ (extChartAt I x₀).source
⊢ s ∈ 𝓝 y

Tactic:
exact mem_interior_iff_mem_nhds.mp ys

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
⊢ ∀ (o : Set E),
    IsOpen o →
      ↑(extChartAt I x₀) x ∈ o →
        (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty

Tactic:
intro o o_open ho

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
I : ModelWithCorners 𝕜 E H
s : Set M
inst✝ : ChartedSpace H M
x₀ x : M
hx : x ∈ closure (interior s)
h'x : x ∈ (extChartAt I x₀).source
o : Set E
o_open : IsOpen o
ho : ↑(extChartAt I x₀) x ∈ o
⊢ (o ∩ interior (↑(extChartAt I x₀).symm ⁻¹' s) ∩ interior (extChartAt I x₀).target).Nonempty
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_strictMono_of_nonempty [h : Nonempty n] :
    StrictMono (matricesOver (R := R) n) :=
  matricesOver_monotone n |>.strictMono_of_injective <| fun I J eq => by
    ext x
    have : _ ↔ _ := congr((Matrix.of fun _ _ => x) ∈ $eq)
    simpa only [mem_matricesOver, of_apply, forall_const] using this

Proof state:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
h : Nonempty n
I J : TwoSidedIdeal R
eq : matricesOver n I = matricesOver n J
x : R
this : (of fun x_1 x_2 => x) ∈ matricesOver n I ↔ (of fun x_1 x_2 => x) ∈ matricesOver n J
⊢ x ∈ I ↔ x ∈ J

Tactic:
simpa only [mem_matricesOver, of_apply, forall_const] using this

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
h : Nonempty n
I J : TwoSidedIdeal R
eq : matricesOver n I = matricesOver n J
⊢ I = J

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
h : Nonempty n
I J : TwoSidedIdeal R
eq : matricesOver n I = matricesOver n J
x : R
⊢ x ∈ I ↔ x ∈ J

Proof state:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
h : Nonempty n
I J : TwoSidedIdeal R
eq : matricesOver n I = matricesOver n J
x : R
⊢ x ∈ I ↔ x ∈ J

Tactic:
have : _ ↔ _ := congr((Matrix.of fun _ _ => x) ∈ $eq)

Result:
case h
R : Type u_1
inst✝¹ : Ring R
n : Type u_2
inst✝ : Fintype n
h : Nonempty n
I J : TwoSidedIdeal R
eq : matricesOver n I = matricesOver n J
x : R
this : (of fun x_1 x_2 => x) ∈ matricesOver n I ↔ (of fun x_1 x_2 => x) ∈ matricesOver n J
⊢ x ∈ I ↔ x ∈ J
-- Mathlib/RepresentationTheory/Rep.lean
theorem leftRegularHomEquiv_symm_single {A : Rep k G} (x : A) (g : G) :
    ((leftRegularHomEquiv A).symm x).hom (Finsupp.single g 1) = A.ρ g x

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
A : Rep k G
x : ↑A.V
g : G
⊢ (ConcreteCategory.hom (A.leftRegularHomEquiv.symm x).hom) (Finsupp.single g 1) = (A.ρ g) x

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Lemmas.lean
theorem lt_div_iff_mul_lt (h : 0 < k) : x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
have t := le_div_iff_mul_le h (x := x + 1) (y := y)

Result:
k x y : Nat
h : 0 < k
t : x + 1 ≤ y / k ↔ (x + 1) * k ≤ y
⊢ x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k < y - (k - 1)
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
exact t

Result:
no goals

Proof state:
k x y : Nat
h : 0 < k
t : x + 1 ≤ y / k ↔ (x + 1) * k ≤ y
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
rw [succ_le, add_one_mul] at t

Result:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + k ≤ y
⊢ x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + k ≤ y
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
have s : k = k - 1 + 1 := by omega

Result:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + k ≤ y
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + (k - 1 + 1) ≤ y
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
rw [← Nat.add_assoc, succ_le, add_lt_iff_lt_sub_right] at t

Result:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k < y - (k - 1)
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + k ≤ y
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Tactic:
conv at t => rhs; lhs; rhs; rw [s]

Result:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + (k - 1 + 1) ≤ y
s : k = k - 1 + 1
⊢ x < y / k ↔ x * k < y - (k - 1)

Proof state:
k x y : Nat
h : 0 < k
t : x < y / k ↔ x * k + k ≤ y
⊢ k = k - 1 + 1

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma succ_mod_two_eq_zero_iff : (m + 1) % 2 = 0 ↔ m % 2 = 1

Proof state:
m : ℕ
⊢ (m + 1) % 2 = 0 ↔ m % 2 = 1

Tactic:
simp [← Nat.even_iff, ← Nat.not_even_iff, parity_simps]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsSwap.isCycle : IsSwap f → IsCycle f

Proof state:
case intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
x y : α
hxy : x ≠ y
⊢ (swap x y).IsCycle

Tactic:
exact isCycle_swap hxy

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableEq α
⊢ f.IsSwap → f.IsCycle

Tactic:
rintro ⟨x, y, hxy, rfl⟩

Result:
case intro.intro.intro
α : Type u_2
inst✝ : DecidableEq α
x y : α
hxy : x ≠ y
⊢ (swap x y).IsCycle
-- Mathlib/Topology/DerivedSet.lean
theorem Continuous.image_derivedSet {β : Type*} [TopologicalSpace β] {A : Set X} {f : X → β}
    (hf1 : Continuous f) (hf2 : Function.Injective f) :
    f '' derivedSet A ⊆ derivedSet (f '' A)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
x : β
hx : ∃ x_1, AccPt x_1 (𝓟 A) ∧ f x_1 = x
⊢ x ∈ derivedSet (f '' A)

Tactic:
obtain ⟨y, hy1, rfl⟩ := hx

Result:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
⊢ f '' derivedSet A ⊆ derivedSet (f '' A)

Tactic:
intro x hx

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
x : β
hx : x ∈ f '' derivedSet A
⊢ x ∈ derivedSet (f '' A)

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
x : β
hx : x ∈ f '' derivedSet A
⊢ x ∈ derivedSet (f '' A)

Tactic:
simp only [Set.mem_image, mem_derivedSet] at hx

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
x : β
hx : ∃ x_1, AccPt x_1 (𝓟 A) ∧ f x_1 = x
⊢ x ∈ derivedSet (f '' A)

Proof state:
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A)

Tactic:
convert hy1.map hf1.continuousAt hf2

Result:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))

Proof state:
case a
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
A : Set X
f : X → β
hf1 : Continuous f
hf2 : Function.Injective f
y : X
hy1 : AccPt y (𝓟 A)
⊢ f y ∈ derivedSet (f '' A) ↔ AccPt (f y) (map f (𝓟 A))

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Ideal.lean
theorem exists_radical_pow_le_of_fg {R : Type*} [CommSemiring R] (I : Ideal R) (h : I.radical.FG) :
    ∃ n : ℕ, I.radical ^ n ≤ I

Proof state:
case refine_1
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
x : R
hx : Submodule.span R {x} ≤ I.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I

Tactic:
obtain ⟨n, hn⟩ := hx (subset_span (Set.mem_singleton x))

Result:
case refine_1.intro
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
x : R
hx : Submodule.span R {x} ≤ I.radical
n : ℕ
hn : x ^ n ∈ I
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I

Proof state:
case refine_2.intro.intro
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ ∃ n, (J ⊔ K) ^ n ≤ I

Tactic:
use n + m

Result:
case h
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
⊢ (J ⊔ K) ^ (n + m) ≤ I

Proof state:
case refine_1
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ ∀ (x : R), (fun J => J ≤ I.radical → ∃ n, J ^ n ≤ I) (Submodule.span R {x})

Tactic:
intro x hx

Result:
case refine_1
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
x : R
hx : Submodule.span R {x} ≤ I.radical
⊢ ∃ n, Submodule.span R {x} ^ n ≤ I

Proof state:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ n + m - i

Tactic:
rw [add_comm, Nat.add_sub_assoc h.le]

Result:
case h.inr
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h✝ : I.radical.FG
J K : Submodule R R
hJ : J ≤ I.radical → ∃ n, J ^ n ≤ I
hK : K ≤ I.radical → ∃ n, K ^ n ≤ I
hJK : J ⊔ K ≤ I.radical
n : ℕ
hn : J ^ n ≤ I
m : ℕ
hm : K ^ m ≤ I
i : ℕ
x✝ : i ∈ Finset.range (n + m + 1)
h : i < n
⊢ m ≤ m + (n - i)

Proof state:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
this : I.radical ≤ I.radical
⊢ ∃ n, I.radical ^ n ≤ I

Tactic:
revert this

Result:
R : Type u_3
inst✝ : CommSemiring R
I : Ideal R
h : I.radical.FG
⊢ I.radical ≤ I.radical → ∃ n, I.radical ^ n ≤ I
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem ext_iff {f g : E →ₗ.[R] F} :
    f = g ↔
      f.domain = g.domain ∧
        ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩ :=
  ⟨by rintro rfl; simp, fun ⟨deq, feq⟩ ↦ ext deq feq⟩

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
⊢ f = g → f.domain = g.domain ∧ ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩

Tactic:
rintro rfl

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ f.domain = f.domain ∧ ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄, ↑f ⟨x, hf⟩ = ↑f ⟨x, hg⟩

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
⊢ f.domain = f.domain ∧ ∀ ⦃x : E⦄ ⦃hf hg : x ∈ f.domain⦄, ↑f ⟨x, hf⟩ = ↑f ⟨x, hg⟩

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sign.lean
theorem sign_mul_self (x : α) : sign x * x = |x|

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
x : α
⊢ ↑(sign x) * x = |x|

Tactic:
rcases lt_trichotomy x 0 with hx | rfl | hx <;> simp [*, abs_of_pos, abs_of_neg]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma add_eq_two_iff : m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

Proof state:
m n : ℕ
⊢ m + n = 2 ↔ m = 0 ∧ n = 2 ∨ m = 1 ∧ n = 1 ∨ m = 2 ∧ n = 0

Tactic:
omega

Result:
no goals