harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Lattice/Prod.lean
/-- See also `Finset.sup'_prodMap`. -/
lemma prodMk_sup'_sup' (hs : s.Nonempty) (ht : t.Nonempty) (f : ι → α) (g : κ → β) :
    (sup' s hs f, sup' t ht g) = sup' (s ×ˢ t) (hs.product ht) (Prod.map f g) :=
  eq_of_forall_ge_iff fun i ↦ by
    obtain ⟨a, ha⟩ := hs
    obtain ⟨b, hb⟩ := ht
    simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]
    exact ⟨by aesop, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩

Proof state:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
aesop

Result:
no goals

Proof state:
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
hs : s.Nonempty
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
⊢ (s.sup' hs f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
obtain ⟨a, ha⟩ := hs

Result:
case intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Proof state:
case intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
ht : t.Nonempty
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
⊢ (s.sup' ⋯ f, t.sup' ht g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
obtain ⟨b, hb⟩ := ht

Result:
case intro.intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Proof state:
case intro.intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ (s.sup' ⋯ f, t.sup' ⋯ g) ≤ i ↔ (s ×ˢ t).sup' ⋯ (Prod.map f g) ≤ i

Tactic:
simp only [Prod.map, sup'_le_iff, mem_product, and_imp, Prod.forall, Prod.le_def]

Result:
case intro.intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) ↔ ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Proof state:
case intro.intro
ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) ↔ ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
exact ⟨by aesop, fun h ↦ ⟨fun i hi ↦ (h _ _ hi hb).1, fun j hj ↦ (h _ _ ha hj).2⟩⟩

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem eq_zero_or_eq_zero_of_mul_eq_zero [NoZeroDivisors R] (φ ψ : R⟦X⟧) (h : φ * ψ = 0) :
    φ = 0 ∨ ψ = 0

Proof state:
case h.h.h₀
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
⊢ ∀ b ∈ antidiagonal (m + n), b ≠ (m, n) → (coeff R b.1) φ * (coeff R b.2) ψ = 0

Tactic:
rintro ⟨i, j⟩ hij hne

Result:
case h.h.h₀.mk
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
hm₂ : ∀ k < m, ¬(coeff R k) φ ≠ 0
n : ℕ
ih : ∀ m < n, (coeff R m) ψ = 0
h : ∑ p ∈ antidiagonal (m + n), (coeff R p.1) φ * (coeff R p.2) ψ = 0
i j : ℕ
hij : (i, j) ∈ antidiagonal (m + n)
hne : (i, j) ≠ (m, n)
⊢ (coeff R (i, j).1) φ * (coeff R (i, j).2) ψ = 0

Proof state:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
⊢ ψ = 0

Tactic:
have hm₁ : coeff R m φ ≠ 0 := Nat.find_spec ex

Result:
R : Type u_1
inst✝¹ : Ring R
inst✝ : NoZeroDivisors R
φ ψ : R⟦X⟧
h : φ * ψ = 0
H : ¬φ = 0
ex : ∃ m, (coeff R m) φ ≠ 0
m : ℕ := Nat.find ex
hm₁ : (coeff R m) φ ≠ 0
⊢ ψ = 0
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_bracket_eq [LieModule R L M] (hf₁ : f.ker = ⊥) (hf₂ : N₂ ≤ f.range) :
    comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆

Tactic:
rw [← map_bracket_eq, comap_map_eq _ f hf₁]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, N₂⁆ = ⁅I, comap f N₂⁆

Tactic:
conv_lhs => rw [← map_comap_eq N₂ f hf₂]

Result:
R : Type u
L : Type v
M : Type w
M₂ : Type w₁
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : LieRingModule L M
inst✝⁵ : AddCommGroup M₂
inst✝⁴ : Module R M₂
inst✝³ : LieRingModule L M₂
N₂ : LieSubmodule R L M₂
f : M →ₗ⁅R,L⁆ M₂
inst✝² : LieAlgebra R L
inst✝¹ : LieModule R L M₂
I : LieIdeal R L
inst✝ : LieModule R L M
hf₁ : f.ker = ⊥
hf₂ : N₂ ≤ f.range
⊢ comap f ⁅I, map f (comap f N₂)⁆ = ⁅I, comap f N₂⁆
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- `binEntropy` is symmetric about 1/2. -/
lemma binEntropy_two_inv_add (p : ℝ) : binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Proof state:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)

Tactic:
ring_nf

Result:
no goals

Proof state:
p : ℝ
⊢ binEntropy (2⁻¹ + p) = binEntropy (2⁻¹ - p)

Tactic:
rw [← binEntropy_one_sub]

Result:
p : ℝ
⊢ binEntropy (1 - (2⁻¹ + p)) = binEntropy (2⁻¹ - p)
-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma krullTopology_mem_nhds_one_iff_of_isGalois [IsGalois k K] (A : Set (K ≃ₐ[k] K)) :
    A ∈ 𝓝 1 ↔ ∃ (L : FiniteGaloisIntermediateField k K), (L.fixingSubgroup : Set _) ⊆ A

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
A : Set (K ≃ₐ[k] K)
⊢ A ∈ 𝓝 1 ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Tactic:
rw [krullTopology_mem_nhds_one_iff_of_normal]

Result:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
A : Set (K ≃ₐ[k] K)
⊢ (∃ E, FiniteDimensional k ↥E ∧ Normal k ↥E ∧ ↑E.fixingSubgroup ⊆ A) ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Proof state:
k : Type u_3
K : Type u_4
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
A : Set (K ≃ₐ[k] K)
⊢ (∃ E, FiniteDimensional k ↥E ∧ Normal k ↥E ∧ ↑E.fixingSubgroup ⊆ A) ↔ ∃ L, ↑L.fixingSubgroup ⊆ A

Tactic:
exact ⟨fun ⟨L, _, hL, hsub⟩ ↦ ⟨{ toIntermediateField := L, isGalois := ⟨⟩ }, hsub⟩,
  fun ⟨L, hL⟩ ↦ ⟨L, inferInstance, inferInstance, hL⟩⟩

Result:
no goals
-- Mathlib/Order/Monotone/Union.lean
theorem StrictMonoOn.Iic_union_Ici (h₁ : StrictMonoOn f (Iic a))
    (h₂ : StrictMonoOn f (Ici a)) : StrictMono f

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)

Tactic:
exact StrictMonoOn.union h₁ h₂ isGreatest_Iic isLeast_Ici

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMono f

Tactic:
rw [← strictMonoOn_univ, ← @Iic_union_Ici _ _ a]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
a : α
f : α → β
h₁ : StrictMonoOn f (Iic a)
h₂ : StrictMonoOn f (Ici a)
⊢ StrictMonoOn f (Iic a ∪ Ici a)
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem norm_lt_iff_of_compact [CompactSpace α] {f : α →ᵇ β} {M : ℝ} (M0 : 0 < M) :
    ‖f‖ < M ↔ ∀ x, ‖f x‖ < M

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M

Tactic:
exact dist_lt_iff_of_compact M0

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ ‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M

Tactic:
simp_rw [norm_def, ← dist_zero_right]

Result:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : CompactSpace α
f : α →ᵇ β
M : ℝ
M0 : 0 < M
⊢ dist f 0 < M ↔ ∀ (x : α), dist (f x) 0 < M
-- Mathlib/Dynamics/TopologicalEntropy/NetEntropy.lean
@[simp]
lemma netMaxcard_empty {T : X → X} {U : Set (X × X)} {n : ℕ} : netMaxcard T ∅ U n = 0

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
⊢ ∀ (i : Finset X), IsDynNetIn T ∅ U n ↑i → ↑i.card = ⊥

Tactic:
intro s s_net

Result:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : IsDynNetIn T ∅ U n ↑s
⊢ ↑s.card = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
⊢ netMaxcard T ∅ U n = 0

Tactic:
rw [netMaxcard, ← bot_eq_zero, iSup₂_eq_bot]

Result:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
⊢ ∀ (i : Finset X), IsDynNetIn T ∅ U n ↑i → ↑i.card = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : IsDynNetIn T ∅ U n ↑s
⊢ ↑s.card = ⊥

Tactic:
replace s_net := subset_empty_iff.1 s_net.1

Result:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : ↑s = ∅
⊢ ↑s.card = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : ↑s = ∅
⊢ ↑s.card = ⊥

Tactic:
norm_cast at s_net

Result:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : s = ∅
⊢ ↑s.card = ⊥

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
n : ℕ
s : Finset X
s_net : s = ∅
⊢ ↑s.card = ⊥

Tactic:
rw [s_net, Finset.card_empty, CharP.cast_eq_zero, bot_eq_zero']

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
theorem adjoin_induction' {p : adjoin R s → Prop} (mem : ∀ (x) (h : x ∈ s), p ⟨x, subset_adjoin h⟩)
    (algebraMap : ∀ r, p (algebraMap R _ r)) (add : ∀ x y, p x → p y → p (x + y))
    (mul : ∀ x y, p x → p y → p (x * y)) (x : adjoin R s) : p x :=
  Subtype.recOn x fun x hx => by
    induction hx using adjoin_induction with
    | mem _ h => exact mem _ h
    | algebraMap _ => exact algebraMap _
    | mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
    | add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂

Proof state:
case mem
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : ↥(adjoin R s) → Prop
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
x✝¹ : ↥(adjoin R s)
x x✝ : A
h : x✝ ∈ s
⊢ p ⟨x✝, ⋯⟩

Tactic:
exact mem _ h

Result:
no goals

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : ↥(adjoin R s) → Prop
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
⊢ p ⟨x, hx⟩

Tactic:
induction hx using adjoin_induction with
| mem _ h => exact mem _ h
| algebraMap _ => exact algebraMap _
| mul _ _ _ _ h₁ h₂ => exact mul _ _ h₁ h₂
| add _ _ _ _ h₁ h₂ => exact add _ _ h₁ h₂

Result:
no goals

Proof state:
case mul
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : ↥(adjoin R s) → Prop
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
x✝¹ : ↥(adjoin R s)
x x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ * y✝, ⋯⟩

Tactic:
exact mul _ _ h₁ h₂

Result:
no goals

Proof state:
case algebraMap
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : ↥(adjoin R s) → Prop
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
x✝ : ↥(adjoin R s)
x : A
r✝ : R
⊢ p ⟨(_root_.algebraMap R A) r✝, ⋯⟩

Tactic:
exact algebraMap _

Result:
no goals

Proof state:
case add
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : ↥(adjoin R s) → Prop
mem : ∀ (x : A) (h : x ∈ s), p ⟨x, ⋯⟩
algebraMap : ∀ (r : R), p ((_root_.algebraMap R ↥(adjoin R s)) r)
add : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x + y)
mul : ∀ (x y : ↥(adjoin R s)), p x → p y → p (x * y)
x✝¹ : ↥(adjoin R s)
x x✝ y✝ : A
hx✝ : x✝ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
h₁ : p ⟨x✝, hx✝⟩
h₂ : p ⟨y✝, hy✝⟩
⊢ p ⟨x✝ + y✝, ⋯⟩

Tactic:
exact add _ _ h₁ h₂

Result:
no goals
-- Mathlib/FieldTheory/SplittingField/Construction.lean
theorem splits (n : ℕ) :
    ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f :=
  Nat.recOn (motive := fun n => ∀ {K : Type u} [Field K],
      ∀ (f : K[X]) (_hfn : f.natDegree = n), Splits (algebraMap K <| SplittingFieldAux n f) f) n
    (fun {_} _ _ hf =>
      splits_of_degree_le_one _
        (le_trans degree_le_natDegree <| hf.symm ▸ WithBot.coe_le_coe.2 zero_le_one))
    fun n ih {K} _ f hf => by
    rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits,
      ← X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]
    exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : 0 = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
cases hf

Result:
no goals

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ Splits (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
    ((X - C (AdjoinRoot.root f.factor)) * f.removeFactor)

Tactic:
exact splits_mul _ (splits_X_sub_C _) (ih _ (natDegree_removeFactor' hf))

Result:
no goals

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
h : f.natDegree = 0
⊢ False

Tactic:
rw [h] at hf

Result:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : 0 = n.succ
h : f.natDegree = 0
⊢ False

Proof state:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ Splits (algebraMap K (SplittingFieldAux n.succ f)) f

Tactic:
rw [← splits_id_iff_splits, algebraMap_succ, ← map_map, splits_id_iff_splits,
  ← X_sub_C_mul_removeFactor f fun h => by rw [h] at hf; cases hf]

Result:
n✝ : ℕ
K✝ : Type u
inst✝ : Field K✝
n : ℕ
ih :
  (fun n =>
      ∀ {K : Type u} [inst : Field K] (f : K[X]), f.natDegree = n → Splits (algebraMap K (SplittingFieldAux n f)) f)
    n
K : Type u
x✝ : Field K
f : K[X]
hf : f.natDegree = n.succ
⊢ Splits (algebraMap (AdjoinRoot f.factor) (SplittingFieldAux n f.removeFactor))
    ((X - C (AdjoinRoot.root f.factor)) * f.removeFactor)
-- Mathlib/Data/Stream/Init.lean
theorem nats_eq : nats = cons 0 (map succ nats)

Proof state:
case a.zero

⊢ nats.get 0 = (0 :: map succ nats).get 0

Tactic:
rfl

Result:
no goals

Proof state:
case a.succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case a.succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)

Tactic:
rw [get_succ]

Result:
case a.succ
n✝ : ℕ
⊢ nats.tail.get n✝ = (0 :: map succ nats).get (n✝ + 1)

Proof state:
case a

⊢ ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n

Tactic:
intro n

Result:
case a
n : ℕ
⊢ nats.get n = (0 :: map succ nats).get n

Proof state:
case a
n : ℕ
⊢ nats.get n = (0 :: map succ nats).get n

Tactic:
cases n

Result:
case a.zero

⊢ nats.get 0 = (0 :: map succ nats).get 0

case a.succ
n✝ : ℕ
⊢ nats.get (n✝ + 1) = (0 :: map succ nats).get (n✝ + 1)

Proof state:
⊢ nats = 0 :: map succ nats

Tactic:
apply Stream'.ext

Result:
case a

⊢ ∀ (n : ℕ), nats.get n = (0 :: map succ nats).get n
-- Mathlib/CategoryTheory/Galois/Basic.lean
/-- An object that is neither initial or connected has a non-trivial subobject. -/
lemma has_non_trivial_subobject_of_not_isConnected_of_not_initial (X : C) (hc : ¬ IsConnected X)
    (hi : IsInitial X → False) :
    ∃ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) ∧ Mono v ∧ (¬ IsIso v)

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
hc : ¬IsConnected X
hi : IsInitial X → False
⊢ ∃ Y v, (IsInitial Y → False) ∧ Mono v ∧ ¬IsIso v

Tactic:
contrapose! hc

Result:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
hi : IsInitial X → False
hc : ∀ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) → Mono v → IsIso v
⊢ IsConnected X

Proof state:
C : Type u₁
inst✝ : Category.{u₂, u₁} C
X : C
hi : IsInitial X → False
hc : ∀ (Y : C) (v : Y ⟶ X), (IsInitial Y → False) → Mono v → IsIso v
⊢ IsConnected X

Tactic:
exact ⟨hi, fun Y i hm hni ↦ hc Y i hni hm⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem natCast_mul (a b : Nat) : ((a * b : Nat) : Int) = (a : Int) * (b : Int)

Proof state:
a b : Nat
⊢ ↑(a * b) = ↑a * ↑b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Deligne.lean
/-- Reformulation of the doubling formula in terms of `Gammaℝ`. -/
lemma Gammaℝ_mul_Gammaℝ_add_one (s : ℂ) : Gammaℝ s * Gammaℝ (s + 1) = Gammaℂ s

Proof state:
s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
⊢ 2 * 2 ^ (-s) * ↑π ^ (-1 / 2 - s + 1 / 2) * Gamma s = 2 * (2 ^ (-s) * ↑π ^ (-s)) * Gamma s

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
⊢ s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ

Tactic:
simp only [Gammaℝ_def, Gammaℂ_def]

Result:
s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) = 2 * (2 * ↑π) ^ (-s) * Gamma s

Proof state:
s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) = 2 * (2 * ↑π) ^ (-s) * Gamma s

Tactic:
calc
_ = (π ^ (-s / 2) * π ^ (-(s + 1) / 2)) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) := by ring_nf
_ = 2 ^ (1 - s) * (π ^ (-1 / 2 - s) * π ^ (1 / 2 : ℂ)) * Gamma s := by
  rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
    sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]
  ring_nf
_ = 2 * ((2 : ℝ) ^ (-s) * π ^ (-s)) * Gamma s := by
  rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
    ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]
  ring_nf
_ = 2 * (2 * π) ^ (-s) * Gamma s := by
  rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

Result:
no goals

Proof state:
s : ℂ
⊢ 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s = 2 * (2 * ↑π) ^ (-s) * Gamma s

Tactic:
rw [← mul_cpow_ofReal_nonneg two_pos.le pi_pos.le, ofReal_ofNat]

Result:
no goals

Proof state:
s : ℂ
⊢ 2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s = 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s

Tactic:
rw [sub_eq_add_neg, cpow_add _ _ two_ne_zero, cpow_one,
  ← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), ofReal_ofNat]

Result:
s : ℂ
⊢ 2 * 2 ^ (-s) * ↑π ^ (-1 / 2 - s + 1 / 2) * Gamma s = 2 * (2 ^ (-s) * ↑π ^ (-s)) * Gamma s

Proof state:
s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑π ^ (1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
ring_nf

Result:
no goals

Proof state:
s : ℂ
⊢ ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
rw [← cpow_add _ _ (ofReal_ne_zero.mpr pi_ne_zero), Complex.Gamma_mul_Gamma_add_half,
  sqrt_eq_rpow, ofReal_cpow pi_pos.le, ofReal_div, ofReal_one, ofReal_ofNat]

Result:
s : ℂ
⊢ ↑π ^ (-s / 2 + -(s + 1) / 2) * (Gamma (2 * (s / 2)) * 2 ^ (1 - 2 * (s / 2)) * ↑π ^ (1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s
-- Mathlib/SetTheory/Game/Domineering.lean
theorem moveRight_smaller {b : Board} {m : ℤ × ℤ} (h : m ∈ right b) :
    Finset.card (moveRight b m) / 2 < Finset.card b / 2

Proof state:
b : Board
m : ℤ × ℤ
h : m ∈ right b
⊢ Finset.card (moveRight b m) / 2 < Finset.card b / 2

Tactic:
simp [← moveRight_card h, lt_add_one]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem coePNat_nat (v : PrimeMultiset) : ((v : Multiset ℕ+) : Multiset ℕ) = (v : Multiset ℕ)

Proof state:
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v

Tactic:
congr

Result:
no goals

Proof state:
v : PrimeMultiset
⊢ Multiset.map PNat.val v.toPNatMultiset = v.toNatMultiset

Tactic:
change (v.map (Coe.coe : Nat.Primes → ℕ+)).map Subtype.val = v.map Subtype.val

Result:
v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v

Proof state:
v : PrimeMultiset
⊢ Multiset.map Subtype.val (Multiset.map Coe.coe v) = Multiset.map Subtype.val v

Tactic:
rw [Multiset.map_map]

Result:
v : PrimeMultiset
⊢ Multiset.map (Subtype.val ∘ Coe.coe) v = Multiset.map Subtype.val v