harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem map_attach {l : List α} (f : { x // x ∈ l } → β) :
    l.attach.map f = l.pmap (fun a h => f ⟨a, h⟩) (fun _ => id)

Proof state:
case cons
α : Type u_1
β : Type u_2
x : α
xs : List α
ih : ∀ (f : { x // x ∈ xs } → β), map f xs.attach = pmap (fun a h => f ⟨a, h⟩) xs ⋯
f : { x_1 // x_1 ∈ x :: xs } → β
⊢ pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯ = pmap (fun a h => f ⟨a, h⟩) xs ⋯

Tactic:
apply pmap_congr_left

Result:
case cons.h
α : Type u_1
β : Type u_2
x : α
xs : List α
ih : ∀ (f : { x // x ∈ xs } → β), map f xs.attach = pmap (fun a h => f ⟨a, h⟩) xs ⋯
f : { x_1 // x_1 ∈ x :: xs } → β
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ xs) (h₂ : a ∈ x :: xs), f ⟨a, ⋯⟩ = f ⟨a, h₂⟩

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : { x // x ∈ l } → β
⊢ map f l.attach = pmap (fun a h => f ⟨a, h⟩) l ⋯

Tactic:
induction l with
| nil => rfl
| cons x xs ih =>
  simp only [attach_cons, map_cons, map_map, Function.comp_apply, pmap, cons.injEq, true_and, ih]
  apply pmap_congr_left
  simp

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
x : α
xs : List α
ih : ∀ (f : { x // x ∈ xs } → β), map f xs.attach = pmap (fun a h => f ⟨a, h⟩) xs ⋯
f : { x_1 // x_1 ∈ x :: xs } → β
⊢ map f (x :: xs).attach = pmap (fun a h => f ⟨a, h⟩) (x :: xs) ⋯

Tactic:
simp only [attach_cons, map_cons, map_map, Function.comp_apply, pmap, cons.injEq, true_and, ih]

Result:
case cons
α : Type u_1
β : Type u_2
x : α
xs : List α
ih : ∀ (f : { x // x ∈ xs } → β), map f xs.attach = pmap (fun a h => f ⟨a, h⟩) xs ⋯
f : { x_1 // x_1 ∈ x :: xs } → β
⊢ pmap (fun a h => f ⟨a, ⋯⟩) xs ⋯ = pmap (fun a h => f ⟨a, h⟩) xs ⋯

Proof state:
case cons.h
α : Type u_1
β : Type u_2
x : α
xs : List α
ih : ∀ (f : { x // x ∈ xs } → β), map f xs.attach = pmap (fun a h => f ⟨a, h⟩) xs ⋯
f : { x_1 // x_1 ∈ x :: xs } → β
⊢ ∀ (a : α), a ∈ xs → ∀ (h₁ : a ∈ xs) (h₂ : a ∈ x :: xs), f ⟨a, ⋯⟩ = f ⟨a, h₂⟩

Tactic:
simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : { x // x ∈ [] } → β
⊢ map f [].attach = pmap (fun a h => f ⟨a, h⟩) [] ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one (q : ℕ) [ExpChar F q] (hm : f.Monic)
    (h : f.natSepDegree = 1) : ∃ (m n : ℕ) (y : F),
      m ≠ 0 ∧ (n = 0 ∨ y ∉ (frobenius F q).range) ∧ f = (X ^ q ^ n - C y) ^ m

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
h : f.natSepDegree = 1
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f

Tactic:
rw [hf, natSepDegree_mul_of_isCoprime _ c <| IsCoprime.pow_left <|
  (hI.isCoprime_or_dvd c).resolve_right H, natSepDegree_pow_of_ne_zero _ hne, hD,
  add_right_eq_self, natSepDegree_eq_zero_iff] at h

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
F : Type u
inst✝¹ : Field F
f : F[X]
q : ℕ
inst✝ : ExpChar F q
hm : f.Monic
p : F[X]
hM : p.Monic
hI : Irreducible p
hf✝ : p ∣ f
hD : p.natSepDegree = 1
n : ℕ
y : F
H✝ : n = 0 ∨ y ∉ (frobenius F q).range
hp : p = X ^ q ^ n - C y
hF : FiniteMultiplicity p f
hne : multiplicity p f ≠ 0
c : F[X]
h : c.natDegree = 0
hf : f = p ^ multiplicity p f * c
H : ¬p ∣ c
⊢ f = (X ^ q ^ n - C y) ^ multiplicity p f
-- Mathlib/Data/Nat/Pairing.lean
theorem right_le_pair (a b : ℕ) : b ≤ pair a b

Proof state:
case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b

Tactic:
simpa [pair, h] using le_trans (le_mul_self _) (Nat.le_add_right _ _)

Result:
no goals

Proof state:
case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b

Tactic:
simp [pair, h]

Result:
no goals

Proof state:
a b : ℕ
⊢ b ≤ pair a b

Tactic:
by_cases h : a < b

Result:
case pos
a b : ℕ
h : a < b
⊢ b ≤ pair a b

case neg
a b : ℕ
h : ¬a < b
⊢ b ≤ pair a b
-- Mathlib/Analysis/Normed/Algebra/Exponential.lean
theorem expSeries_radius_eq_top : (expSeries 𝕂 𝔸).radius = ∞

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => ‖(↑(n + 1))⁻¹‖) atTop (𝓝 0)

Tactic:
apply norm_zero (E := 𝕂) ▸ Filter.Tendsto.norm

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun x => (↑(x + 1))⁻¹) atTop (𝓝 0)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => ‖(↑n.succ !)⁻¹‖ / ‖(↑n !)⁻¹‖) atTop (𝓝 0)

Tactic:
simp_rw [← norm_div, Nat.factorial_succ, Nat.cast_mul, mul_inv_rev, mul_div_right_comm,
  inv_div_inv, norm_mul, div_self this, norm_one, one_mul]

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => ‖(↑(n + 1))⁻¹‖) atTop (𝓝 0)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun x => (↑(x + 1))⁻¹) atTop (𝓝 0)

Tactic:
apply (Filter.tendsto_add_atTop_iff_nat (f := fun n => (n : 𝕂)⁻¹) 1).mpr

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
n : ℕ
⊢ (↑n !)⁻¹ ≠ 0

Tactic:
simp [this]

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ (expSeries 𝕂 𝔸).radius = ⊤

Tactic:
apply expSeries_eq_ofScalars 𝕂 𝔸 ▸
  ofScalars_radius_eq_top_of_tendsto 𝔸 _ (Eventually.of_forall fun n => ?_)

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => ‖(↑n.succ !)⁻¹‖ / ‖(↑n !)⁻¹‖) atTop (𝓝 0)

𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
n : ℕ
⊢ (↑n !)⁻¹ ≠ 0

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ Tendsto (fun n => (↑n)⁻¹) atTop (𝓝 0)

Tactic:
exact RCLike.tendsto_inverse_atTop_nhds_zero_nat 𝕂

Result:
no goals

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
⊢ (expSeries 𝕂 𝔸).radius = ⊤

Tactic:
have {n : ℕ} : (Nat.factorial n : 𝕂) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.factorial_ne_zero n)

Result:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝² : RCLike 𝕂
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕂 𝔸
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ (expSeries 𝕂 𝔸).radius = ⊤
-- Mathlib/MeasureTheory/Group/AEStabilizer.lean
lemma aestabilizer_of_aeconst (hs : EventuallyConst s (ae μ)) : aestabilizer G μ s = ⊤

Proof state:
case inr
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᶠ[ae μ] univ
⊢ g ∈ aestabilizer G μ s

Tactic:
simp [aestabilizer_congr h]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ aestabilizer G μ s

Tactic:
cases eventuallyConst_set'.mp hs with
| inl h => simp [aestabilizer_congr h]
| inr h => simp [aestabilizer_congr h]

Result:
no goals

Proof state:
case inl
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
h : s =ᶠ[ae μ] ∅
⊢ g ∈ aestabilizer G μ s

Tactic:
simp [aestabilizer_congr h]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
⊢ aestabilizer G μ s = ⊤

Tactic:
refine top_unique fun g _ ↦ ?_

Result:
G : Type u_1
α : Type u_2
inst✝² : Group G
inst✝¹ : MulAction G α
x✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
s : Set α
hs : EventuallyConst s (ae μ)
g : G
x✝ : g ∈ ⊤
⊢ g ∈ aestabilizer G μ s
-- Mathlib/Order/KrullDimension.lean
/--
The height of an element is infinite iff there exist series of arbitrary length ending in that
element.
-/
lemma height_eq_top_iff {x : α} :
    height x = ⊤ ↔ ∀ n, ∃ p : LTSeries α, p.last = x ∧ p.length = n where
  mp h n

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ∀ (x_1 : ℕ), ∃ y ∈ Set.range fun x_2 => (↑x_2).length, x_1 < y

Tactic:
intro n

Result:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
⊢ ∃ y ∈ Set.range fun x_1 => (↑x_1).length, n < y

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ n < p.length

Tactic:
simp [hp]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
⊢ ∃ y ∈ Set.range fun x_1 => (↑x_1).length, n < y

Tactic:
obtain ⟨p, hlast, hp⟩ := h (n+1)

Result:
case intro.intro
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ ∃ y ∈ Set.range fun x_1 => (↑x_1).length, n < y

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ ↑n ≤ height x

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ ∃ p, RelSeries.last p = x ∧ p.length = n

Tactic:
apply exists_series_of_le_height x (n := n)

Result:
α : Type u_1
inst✝ : Preorder α
x : α
h : height x = ⊤
n : ℕ
⊢ ↑n ≤ height x

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ height x = ⊤

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype', ENat.iSup_coe_eq_top, bddAbove_def]

Result:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬∃ x_1, ∀ y ∈ Set.range fun x_2 => (↑x_2).length, y ≤ x_1

Proof state:
case intro.intro
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ ∃ y ∈ Set.range fun x_1 => (↑x_1).length, n < y

Tactic:
exact ⟨p.length, ⟨⟨⟨p, hlast⟩, by simp [hp]⟩, by simp [hp]⟩⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ¬∃ x_1, ∀ y ∈ Set.range fun x_2 => (↑x_2).length, y ≤ x_1

Tactic:
push_neg

Result:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
⊢ ∀ (x_1 : ℕ), ∃ y ∈ Set.range fun x_2 => (↑x_2).length, x_1 < y

Proof state:
α : Type u_1
inst✝ : Preorder α
x : α
h : ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n
n : ℕ
p : LTSeries α
hlast : RelSeries.last p = x
hp : p.length = n + 1
⊢ (fun x_1 => (↑x_1).length) ⟨p, hlast⟩ = p.length

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Symmetric.lean
theorem reverse_inj [h : HasInvolutiveReverse V] {a b : V}
    (f g : a ⟶ b) : reverse f = reverse g ↔ f = g

Proof state:
case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

Tactic:
rintro h

Result:
case mp
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g

Proof state:
case mpr
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g

Tactic:
congr

Result:
no goals

Proof state:
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g ↔ f = g

Tactic:
constructor

Result:
case mp
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ reverse f = reverse g → f = g

case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g

Proof state:
case mp
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : reverse f = reverse g
⊢ f = g

Tactic:
simpa using congr_arg Quiver.reverse h

Result:
no goals

Proof state:
case mpr
V : Type u_2
inst✝ : Quiver V
h : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
⊢ f = g → reverse f = reverse g

Tactic:
rintro h

Result:
case mpr
V : Type u_2
inst✝ : Quiver V
h✝ : HasInvolutiveReverse V
a b : V
f g : a ⟶ b
h : f = g
⊢ reverse f = reverse g
-- Mathlib/Data/Nat/Factorization/Induction.lean
lemma prime_composite_induction {P : ℕ → Prop} (zero : P 0) (one : P 1)
    (prime : ∀ p : ℕ, p.Prime → P p) (composite : ∀ a, 2 ≤ a → P a → ∀ b, 2 ≤ b → P b → P (a * b))
    (n : ℕ) : P n

Proof state:
case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : Prime p
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))

Tactic:
exact composite _ hp.two_le (prime _ hp) _ a.one_lt_succ_succ ha

Result:
no goals

Proof state:
case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : Prime p
ha : P (0 + 1)
⊢ P (p * (0 + 1))

Tactic:
simpa using prime _ hp

Result:
no goals

Proof state:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : Prime p
ha : P 0
⊢ P (p * 0)

Tactic:
simpa

Result:
no goals

Proof state:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ P n

Tactic:
refine induction_on_primes zero one ?_ _

Result:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), Prime p → P a → P (p * a)

Proof state:
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n : ℕ
⊢ ∀ (p a : ℕ), Prime p → P a → P (p * a)

Tactic:
rintro p (_ | _ | a) hp ha

Result:
case zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : Prime p
ha : P 0
⊢ P (p * 0)

case succ.zero
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p : ℕ
hp : Prime p
ha : P (0 + 1)
⊢ P (p * (0 + 1))

case succ.succ
P : ℕ → Prop
zero : P 0
one : P 1
prime : ∀ (p : ℕ), Prime p → P p
composite : ∀ (a : ℕ), 2 ≤ a → P a → ∀ (b : ℕ), 2 ≤ b → P b → P (a * b)
n p a : ℕ
hp : Prime p
ha : P (a + 1 + 1)
⊢ P (p * (a + 1 + 1))
-- Mathlib/RingTheory/EisensteinCriterion.lean
theorem irreducible_of_eisenstein_criterion {f : R[X]} {P : Ideal R} (hP : P.IsPrime)
    (hfl : f.leadingCoeff ∉ P) (hfP : ∀ n : ℕ, ↑n < degree f → f.coeff n ∈ P) (hfd0 : 0 < degree f)
    (h0 : f.coeff 0 ∉ P ^ 2) (hu : f.IsPrimitive) : Irreducible f :=
  have hf0 : f ≠ 0 := fun _ => by simp_all only [not_true, Submodule.zero_mem, coeff_zero]
  have hf : f.map (mk P) = C (mk P (leadingCoeff f)) * X ^ natDegree f :=
    map_eq_C_mul_X_pow_of_forall_coeff_mem hfP
  have hfd0 : 0 < f.natDegree := WithBot.coe_lt_coe.1 (lt_of_lt_of_le hfd0 degree_le_natDegree)
  ⟨mt degree_eq_zero_of_isUnit fun h => by simp_all only [lt_irrefl], by
    rintro p q rfl
    rw [Polynomial.map_mul] at hf
    rcases mul_eq_mul_prime_pow
        (show Prime (X : Polynomial (R ⧸ P)) from monic_X.prime_of_degree_eq_one degree_X) hf with
      ⟨m, n, b, c, hmnd, hbc, hp, hq⟩
    have hmn : 0 < m → 0 < n → False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
P : Ideal R
hP : P.IsPrime
p q : R[X]
hfl : (p * q).leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < (p * q).degree → (p * q).coeff n ∈ P
hfd0✝ : 0 < (p * q).degree
h0 : (p * q).coeff 0 ∉ P ^ 2
hu : (p * q).IsPrimitive
hf0 : p * q ≠ 0
hf : map (mk P) p * map (mk P) q = C ((mk P) (p * q).leadingCoeff) * X ^ (p * q).natDegree
hfd0 : 0 < (p * q).natDegree
m n : ℕ
b c : (R ⧸ P)[X]
hmnd : m + n = (p * q).natDegree
hp : map (mk P) p = b * X ^ m
hq : map (mk P) q = c * X ^ n
hmn : 0 < m → 0 < n → False
hpql0 : (mk P) (p * q).leadingCoeff ≠ 0
hp0 : p ≠ 0
hq0 : q ≠ 0
hbc : (C ((mk P) (p * q).leadingCoeff)).degree = (b * c).degree
⊢ b.degree = 0 ∧ c.degree = 0

Tactic:
rwa [degree_C hpql0, degree_mul, eq_comm, Nat.WithBot.add_eq_zero_iff] at hbc

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
f : R[X]
P : Ideal R
hP : P.IsPrime
hfl : f.leadingCoeff ∉ P
hfP : ∀ (n : ℕ), ↑n < f.degree → f.coeff n ∈ P
hfd0✝ : 0 < f.degree
h0 : f.coeff 0 ∉ P ^ 2
hu : f.IsPrimitive
hf0 : f ≠ 0
hf : map (mk P) f = C ((mk P) f.leadingCoeff) * X ^ f.natDegree
hfd0 : 0 < f.natDegree
h : f.degree = 0
⊢ False

Tactic:
simp_all only [lt_irrefl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n

Proof state:
n : Nat
i : Fin n
⊢ natAdd n i = i.addNat n

Tactic:
ext

Result:
case h
n : Nat
i : Fin n
⊢ ↑(natAdd n i) = ↑(i.addNat n)

Proof state:
case h
n : Nat
i : Fin n
⊢ ↑(natAdd n i) = ↑(i.addNat n)

Tactic:
simp

Result:
case h
n : Nat
i : Fin n
⊢ n + ↑i = ↑i + n

Proof state:
case h
n : Nat
i : Fin n
⊢ n + ↑i = ↑i + n

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finsupp/Order.lean
theorem le_iff' (f g : ι →₀ α) {s : Finset ι} (hf : f.support ⊆ s) : f ≤ g ↔ ∀ i ∈ s, f i ≤ g i :=
  ⟨fun h s _hs => h s, fun h s => by
    classical exact
        if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)⟩

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
⊢ f s ≤ g s

Tactic:
exact
if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝² : AddCommMonoid α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
f g : ι →₀ α
s✝ : Finset ι
hf : f.support ⊆ s✝
h : ∀ i ∈ s✝, f i ≤ g i
s : ι
⊢ f s ≤ g s

Tactic:
classical exact
    if H : s ∈ f.support then h s (hf H) else (not_mem_support_iff.1 H).symm ▸ zero_le (g s)

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem mul_lt_top_iff {a b : ℝ≥0∞} : a * b < ∞ ↔ a < ∞ ∧ b < ∞ ∨ a = 0 ∨ b = 0

Proof state:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

Tactic:
rw [← or_assoc, or_iff_not_imp_right, or_iff_not_imp_right]

Result:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
⊢ ¬b = 0 → ¬a = 0 → a < ⊤ ∧ b < ⊤

Proof state:
case mpr
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤

Tactic:
rintro (⟨ha, hb⟩ | rfl | rfl) <;> [exact mul_lt_top ha hb; simp; simp]

Result:
no goals

Proof state:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ⊤ ∧ b < ⊤

Tactic:
exact ⟨lt_top_of_mul_ne_top_left h.ne hb, lt_top_of_mul_ne_top_right h.ne ha⟩

Result:
no goals

Proof state:
case mp
a b : ℝ≥0∞
⊢ a * b < ⊤ → a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

Tactic:
intro h

Result:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

Proof state:
a b : ℝ≥0∞
⊢ a * b < ⊤ ↔ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

Tactic:
constructor

Result:
case mp
a b : ℝ≥0∞
⊢ a * b < ⊤ → a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0

case mpr
a b : ℝ≥0∞
⊢ a < ⊤ ∧ b < ⊤ ∨ a = 0 ∨ b = 0 → a * b < ⊤

Proof state:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
⊢ ¬b = 0 → ¬a = 0 → a < ⊤ ∧ b < ⊤

Tactic:
intro hb ha

Result:
case mp
a b : ℝ≥0∞
h : a * b < ⊤
hb : ¬b = 0
ha : ¬a = 0
⊢ a < ⊤ ∧ b < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast_insertList_of_mem [BEq α] [LawfulBEq α]
    {l toInsert : List ((a : α) × β a)}
    {k k' : α} (k_beq : k == k') (v : β k)
    (distinct_l : DistinctKeys l)
    (distinct_toInsert : toInsert.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ toInsert)
    {h} :
    getValueCast k' (insertList l toInsert) h =
    cast (by congr; exact LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
h : containsKey k' (insertList l toInsert) = true
⊢ k = k'

Tactic:
exact LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
h : containsKey k' (insertList l toInsert) = true
⊢ getValueCast k' (insertList l toInsert) h = cast ⋯ v

Tactic:
rw [← Option.some_inj, ← getValueCast?_eq_some_getValueCast,
  getValueCast?_insertList_of_mem k_beq distinct_l distinct_toInsert mem]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
h : containsKey k' (insertList l toInsert) = true
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
γ : α → Type w
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l toInsert : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
distinct_l : DistinctKeys l
distinct_toInsert : List.Pairwise (fun a b => (a.fst == b.fst) = false) toInsert
mem : ⟨k, v⟩ ∈ toInsert
h : containsKey k' (insertList l toInsert) = true
⊢ k = k'