harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/SetTheory/Ordinal/NaturalOps.lean
theorem mul_le_nmul (a b : Ordinal.{u}) : a * b ≤ a ⨳ b

Proof state:
case refine_1
a b : Ordinal.{u}
⊢ a * 0 ≤ a ⨳ 0

Tactic:
simp

Result:
no goals

Proof state:
case refine_3.inr.mk
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
i : Ordinal.{u}
hi : i ∈ Iio c
⊢ a * ↑⟨i, hi⟩ ≤ a ⨳ c

Tactic:
exact (H i hi).trans (nmul_le_nmul_left hi.le a)

Result:
no goals

Proof state:
case refine_2
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), a * o ≤ a ⨳ o → a * succ o ≤ a ⨳ succ o

Tactic:
intro c h

Result:
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * succ c ≤ a ⨳ succ c

Proof state:
case refine_3.inr
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ ∀ (i : ↑(Iio c)), a * ↑i ≤ a ⨳ c

Tactic:
rintro ⟨i, hi⟩

Result:
case refine_3.inr.mk
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
i : Ordinal.{u}
hi : i ∈ Iio c
⊢ a * ↑⟨i, hi⟩ ≤ a ⨳ c

Proof state:
case refine_3.inl
b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, 0 * o' ≤ 0 ⨳ o'
⊢ 0 * c ≤ 0 ⨳ c

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * c + a ≤ a ⨳ c ♯ a

Tactic:
exact (add_le_nadd _ a).trans (nadd_le_nadd_right h a)

Result:
no goals

Proof state:
case refine_3.inr
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ a * c ≤ a ⨳ c

Tactic:
rw [(isNormal_mul_right ha).apply_of_isLimit hc, Ordinal.iSup_le_iff]

Result:
case refine_3.inr
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ ∀ (i : ↑(Iio c)), a * ↑i ≤ a ⨳ c

Proof state:
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * succ c ≤ a ⨳ succ c

Tactic:
rw [mul_succ, nmul_succ]

Result:
case refine_2
a b c : Ordinal.{u}
h : a * c ≤ a ⨳ c
⊢ a * c + a ≤ a ⨳ c ♯ a

Proof state:
case refine_3
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
⊢ a * c ≤ a ⨳ c

Tactic:
rcases eq_zero_or_pos a with (rfl | ha)

Result:
case refine_3.inl
b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, 0 * o' ≤ 0 ⨳ o'
⊢ 0 * c ≤ 0 ⨳ c

case refine_3.inr
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
ha : 0 < a
⊢ a * c ≤ a ⨳ c

Proof state:
case refine_3
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), o.IsLimit → (∀ o' < o, a * o' ≤ a ⨳ o') → a * o ≤ a ⨳ o

Tactic:
intro c hc H

Result:
case refine_3
a b c : Ordinal.{u}
hc : c.IsLimit
H : ∀ o' < c, a * o' ≤ a ⨳ o'
⊢ a * c ≤ a ⨳ c

Proof state:
a b : Ordinal.{u}
⊢ a * b ≤ a ⨳ b

Tactic:
refine b.limitRecOn ?_ ?_ ?_

Result:
case refine_1
a b : Ordinal.{u}
⊢ a * 0 ≤ a ⨳ 0

case refine_2
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), a * o ≤ a ⨳ o → a * succ o ≤ a ⨳ succ o

case refine_3
a b : Ordinal.{u}
⊢ ∀ (o : Ordinal.{u}), o.IsLimit → (∀ o' < o, a * o' ≤ a ⨳ o') → a * o ≤ a ⨳ o
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem subOneIntegralPowerBasis'_gen [IsCyclotomicExtension {p} ℚ K]
    (hζ : IsPrimitiveRoot ζ p) :
    hζ.subOneIntegralPowerBasis'.gen = hζ.toInteger - 1 :=
  -- The `unusedHavesSuffices` linter incorrectly thinks this `have` is unnecessary.
  have : IsCyclotomicExtension {p ^ 1} ℚ K

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
this : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ IsPrimitiveRoot ζ ↑(p ^ 1)

Tactic:
rwa [pow_one]

Result:
no goals

Proof state:
p : ℕ+
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
hζ : IsPrimitiveRoot ζ ↑p
⊢ IsCyclotomicExtension {p ^ 1} ℚ K

Tactic:
rwa [pow_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
  {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
    setWidth w (x.setWidth (i + 1)) =
      setWidth w (x.setWidth i)

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
subst hik

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i)

Proof state:
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
⊢ setWidth w (setWidth (i + 1) x) = setWidth w (setWidth i x)

Tactic:
ext k h

Result:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x)).getLsbD k

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
by_cases hik : i = k

Result:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
hik : i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

case neg
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
hik : ¬i = k
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Tactic:
by_cases hik' : k < i + 1 <;> simp [hik'] <;> omega

Result:
no goals

Proof state:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
⊢ (setWidth w (setWidth (i + 1) x)).getLsbD k = (setWidth w (setWidth i x)).getLsbD k

Tactic:
simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]

Result:
case pred
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
k : Nat
h : k < w
⊢ (decide (k < i + 1) && x.getLsbD k) = (decide (k < i) && x.getLsbD k)

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
hx : x.getLsbD i = false
h : i < w
⊢ (decide (i < i + 1) && x.getLsbD i) = (decide (i < i) && x.getLsbD i)

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem forall_measure_preimage_mul_iff (μ : Measure G) :
    (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔
      IsMulLeftInvariant μ

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ μ ((fun h => g * h) ⁻¹' A) = μ A ↔ (Measure.map (fun x => g * x) μ) A = μ A

Tactic:
rw [map_apply (measurable_const_mul g) hA]

Result:
no goals

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G) (s : Set G), MeasurableSet s → (Measure.map (fun x => g * x) μ) s = μ s

Tactic:
refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Result:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ μ ((fun h => g * h) ⁻¹' A) = μ A ↔ (Measure.map (fun x => g * x) μ) A = μ A

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x => g * x) μ = μ) ↔ μ.IsMulLeftInvariant

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x => g * x) μ = μ

Tactic:
simp_rw [Measure.ext_iff]

Result:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => g * h) ⁻¹' A) = μ A) ↔
    ∀ (g : G) (s : Set G), MeasurableSet s → (Measure.map (fun x => g * x) μ) s = μ s
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem hausdorffDist_le_diam (hs : s.Nonempty) (bs : IsBounded s) (ht : t.Nonempty)
    (bt : IsBounded t) : hausdorffDist s t ≤ diam (s ∪ t)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
hs : s.Nonempty
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases hs with ⟨x, xs⟩

Result:
case intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)

Tactic:
exact fun z hz => ⟨y, yt, dist_le_diam_of_mem (bs.union bt) (subset_union_left hz)
  (subset_union_right yt)⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
refine hausdorffDist_le_of_mem_dist diam_nonneg ?_ ?_

Result:
case intro.intro.refine_1
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ s, ∃ y ∈ t, dist x y ≤ diam (s ∪ t)

case intro.intro.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)

Proof state:
case intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
ht : t.Nonempty
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Tactic:
rcases ht with ⟨y, yt⟩

Result:
case intro.intro
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ hausdorffDist s t ≤ diam (s ∪ t)

Proof state:
case intro.intro.refine_2
α : Type u
inst✝ : PseudoMetricSpace α
s t : Set α
bs : Bornology.IsBounded s
bt : Bornology.IsBounded t
x : α
xs : x ∈ s
y : α
yt : y ∈ t
⊢ ∀ x ∈ t, ∃ y ∈ s, dist x y ≤ diam (s ∪ t)

Tactic:
exact fun z hz => ⟨x, xs, dist_le_diam_of_mem (bs.union bt) (subset_union_right hz)
  (subset_union_left xs)⟩

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Mates.lean
theorem conjugateEquiv_symm_of_iso (α : R₁ ⟶ R₂)
    [IsIso ((conjugateEquiv adj₁ adj₂).symm α)] : IsIso α

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso α

Tactic:
suffices IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
  by simpa using this

Result:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
⊢ IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
L₁ L₂ : C ⥤ D
R₁ R₂ : D ⥤ C
adj₁ : L₁ ⊣ R₁
adj₂ : L₂ ⊣ R₂
α : R₁ ⟶ R₂
inst✝ : IsIso ((conjugateEquiv adj₁ adj₂).symm α)
this : IsIso ((conjugateEquiv adj₁ adj₂) ((conjugateEquiv adj₁ adj₂).symm α))
⊢ IsIso α

Tactic:
simpa using this

Result:
no goals
-- Mathlib/NumberTheory/Modular.lean
theorem g_eq_of_c_eq_one (hc : g 1 0 = 1) : g = T ^ g 0 0 * S * T ^ g 1 1

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)

Tactic:
simp only [hg, sub_eq_add_neg, hc, coe_mul, coe_T_zpow, coe_S, mul_fin_two, mul_zero, mul_one,
  zero_add, one_mul, add_zero, zero_mul]

Result:
no goals

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1

Tactic:
omega

Result:
no goals

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = (↑g).det
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1

Tactic:
rw [det_fin_two, hc] at hg

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)

Tactic:
conv_lhs => rw [(g : Matrix _ _ ℤ).eta_fin_two]

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ !![↑g 0 0, ↑g 0 1; ↑g 1 0, ↑g 1 1] = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1

Tactic:
refine Subtype.ext ?_

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ ↑g = ↑(T ^ ↑g 0 0 * S * T ^ ↑g 1 1)

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1

Tactic:
have hg := g.det_coe.symm

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = (↑g).det
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1

Proof state:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = (↑g).det
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1

Tactic:
replace hg : g 0 1 = g 0 0 * g 1 1 - 1 := by rw [det_fin_two, hc] at hg; omega

Result:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
⊢ g = T ^ ↑g 0 0 * S * T ^ ↑g 1 1
-- Mathlib/Data/Real/Cardinality.lean
theorem cantorFunctionAux_nonneg (h : 0 ≤ c) : 0 ≤ cantorFunctionAux c f n

Proof state:
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
cases h' : f n

Result:
case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = false
⊢ 0 ≤ cantorFunctionAux c f n

case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n

Proof state:
case true
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = true
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
simpa [h'] using pow_nonneg h _

Result:
no goals

Proof state:
case false
c : ℝ
f : ℕ → Bool
n : ℕ
h : 0 ≤ c
h' : f n = false
⊢ 0 ≤ cantorFunctionAux c f n

Tactic:
simp [h']

Result:
no goals
-- Mathlib/Order/WellFoundedSet.lean
theorem induction (hs : s.WellFoundedOn r) (hx : x ∈ s) {P : α → Prop}
    (hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y) : P x

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ P x

Tactic:
change Q ⟨x, hx⟩

Result:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ Q ⟨x, hx⟩

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ Q ⟨x, hx⟩

Tactic:
refine WellFounded.induction hs ⟨x, hx⟩ ?_

Result:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ ∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ ∀ (x : ↑s), (∀ (y : ↑s), r ↑y ↑x → Q y) → Q x

Tactic:
simpa only [Subtype.forall]

Result:
no goals

Proof state:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
⊢ P x

Tactic:
let Q : s → Prop := fun y => P y

Result:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y => P ↑y
⊢ P x
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem isHashSelf_eraseₘaux [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] (m : Raw₀ α β)
    (a : α) (h : Raw.WFImp m.1) : IsHashSelf (m.eraseₘaux a).1.buckets

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.erase a l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
rw [AssocList.toList_erase] at hp

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ eraseKey a l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ IsHashSelf (m.eraseₘaux a).val.buckets

Tactic:
apply h.buckets_hash_self.updateBucket (fun l p hp => ?_)

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ (AssocList.erase a l).toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
l : AssocList α β
p : (a : α) × β a
hp : p ∈ eraseKey a l.toList
⊢ containsKey p.fst l.toList = true ∨ hash p.fst = hash a

Tactic:
exact Or.inl (containsKey_of_mem ((sublist_eraseKey.mem hp)))

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma lt_of_mul_self_lt_mul_self₀ (hb : 0 ≤ b) : a * a < b * b → a < b

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a b : M₀
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b

Tactic:
exact lt_of_pow_lt_pow_left₀ _ hb

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a b : M₀
hb : 0 ≤ b
⊢ a * a < b * b → a < b

Tactic:
simp_rw [← sq]

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : LinearOrder M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
a b : M₀
hb : 0 ≤ b
⊢ a ^ 2 < b ^ 2 → a < b
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem tendsto_nat_ceil_div_atTop : Tendsto (fun x ↦ (⌈x⌉₊ : R) / x) atTop (𝓝 1)

Proof state:
R : Type u_4
inst✝³ : TopologicalSpace R
inst✝² : LinearOrderedField R
inst✝¹ : OrderTopology R
inst✝ : FloorRing R
⊢ Tendsto (fun x => ↑⌈x⌉₊ / x) atTop (𝓝 1)

Tactic:
simpa using tendsto_nat_ceil_mul_div_atTop (zero_le_one' R)

Result:
no goals
-- Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
lemma IsLocalRing.finrank_CotangentSpace_eq_one_iff [IsNoetherianRing R] [IsLocalRing R]
    [IsDomain R] : finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Proof state:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : ¬IsField R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
exact (IsDiscreteValuationRing.TFAE R hR).out 5 0

Result:
no goals

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
letI := hR.toField

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
simp only [finrank_cotangentSpace_eq_zero, zero_ne_one, false_iff]

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ ¬IsDiscreteValuationRing R

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
this : Field R := hR.toField
⊢ ¬IsDiscreteValuationRing R

Tactic:
exact fun h ↦ h.3 maximalIdeal_eq_bot

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

Tactic:
by_cases hR : IsField R

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : IsField R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R

case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
hR : ¬IsField R
⊢ finrank (ResidueField R) (CotangentSpace R) = 1 ↔ IsDiscreteValuationRing R
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem two_mul_sub_one {n : Nat} (n_pos : n > 0) : (2*n - 1) % 2 = 1

Proof state:
n : Nat
n_pos : n > 0
⊢ (2 * n - 1) % 2 = 1

Tactic:
omega

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem Perm.extendDomain_trans (e e' : Perm α') :
    (e.extendDomain f).trans (e'.extendDomain f) = Perm.extendDomain (e.trans e') f

Proof state:
α' : Type u_9
β' : Type u_10
p : β' → Prop
inst✝ : DecidablePred p
f : α' ≃ Subtype p
e e' : Perm α'
⊢ Equiv.trans (e.extendDomain f) (e'.extendDomain f) = extendDomain (Equiv.trans e e') f

Tactic:
simp [Perm.extendDomain, permCongr_trans]

Result:
no goals