harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Idempotents/Basic.lean
theorem isIdempotentComplete_iff_of_equivalence {D : Type*} [Category D] (ε : C ≌ D) :
    IsIdempotentComplete C ↔ IsIdempotentComplete D

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C

Tactic:
exact Equivalence.isIdempotentComplete ε.symm

Result:
no goals

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

Tactic:
exact Equivalence.isIdempotentComplete ε

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C ↔ IsIdempotentComplete D

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete C → IsIdempotentComplete D

case mpr
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
D : Type u_2
inst✝ : Category.{u_3, u_2} D
ε : C ≌ D
⊢ IsIdempotentComplete D → IsIdempotentComplete C
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem extract_size (as : Vector α n) : as.extract 0 n = as.cast (by simp)

Proof state:
case mk
α : Type u_1
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.extract = Vector.cast ⋯ { toArray := as, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.409555
n : Nat
as : Vector α n
⊢ n = min n n - 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
as : Vector α n
⊢ as.extract = Vector.cast ⋯ as

Tactic:
rcases as with ⟨as, rfl⟩

Result:
case mk
α : Type u_1
as : Array α
⊢ { toArray := as, size_toArray := ⋯ }.extract = Vector.cast ⋯ { toArray := as, size_toArray := ⋯ }
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem weightedVSub_mem_vectorSpan {s : Finset ι} {w : ι → k} (h : ∑ i ∈ s, w i = 0)
    (p : ι → P) : s.weightedVSub p w ∈ vectorSpan k (Set.range p)

Proof state:
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

Tactic:
rcases isEmpty_or_nonempty ι with (hι | ⟨⟨i0⟩⟩)

Result:
case inl
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
hι : IsEmpty ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)

case inr.intro
ι : Type u_1
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Finset ι
w : ι → k
h : ∑ i ∈ s, w i = 0
p : ι → P
i0 : ι
⊢ (s.weightedVSub p) w ∈ vectorSpan k (Set.range p)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_sublist (l : List α) : l.eraseP p <+ l

Proof state:
α : Type u_1
p : α → Bool
l : List α
⊢ eraseP p l <+ l

Tactic:
match exists_or_eq_self_of_eraseP p l with
| .inl h => rw [h]; apply Sublist.refl
| .inr ⟨c, l₁, l₂, _, _, h₃, h₄⟩ => rw [h₄, h₃]; simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ l <+ l

Tactic:
apply Sublist.refl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ eraseP p l <+ l

Tactic:
rw [h]

Result:
α : Type u_1
p : α → Bool
l : List α
h : eraseP p l = l
⊢ l <+ l

Proof state:
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ eraseP p l <+ l

Tactic:
rw [h₄, h₃]

Result:
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ l₁ ++ l₂ <+ l₁ ++ c :: l₂

Proof state:
α : Type u_1
p : α → Bool
l : List α
c : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p c = true
h₃ : l = l₁ ++ c :: l₂
h₄ : eraseP p l = l₁ ++ l₂
⊢ l₁ ++ l₂ <+ l₁ ++ c :: l₂

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem continuous_sub_right (a : ℝ≥0∞) : Continuous fun x : ℝ≥0∞ => x - a

Proof state:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous fun x => x - a

Tactic:
rw [show (fun x => x - a) = (fun p : ℝ≥0∞ × ℝ≥0∞ => p.fst - p.snd) ∘ fun x => ⟨x, a⟩ by rfl]

Result:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous ((fun p => p.1 - p.2) ∘ fun x => (x, a))

Proof state:
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous fun x => (x, a)

Tactic:
fun_prop

Result:
no goals

Proof state:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ ∀ (x : ℝ≥0∞), (x, a) ∈ {p | p ≠ (⊤, ⊤)}

Tactic:
intro x

Result:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
x : ℝ≥0∞
⊢ (x, a) ∈ {p | p ≠ (⊤, ⊤)}

Proof state:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous ((fun p => p.1 - p.2) ∘ fun x => (x, a))

Tactic:
apply continuousOn_sub.comp_continuous (by fun_prop)

Result:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ ∀ (x : ℝ≥0∞), (x, a) ∈ {p | p ≠ (⊤, ⊤)}

Proof state:
case pos
a : ℝ≥0∞
a_infty : a = ⊤
⊢ Continuous fun x => x - a

Tactic:
simp [a_infty, continuous_const, tsub_eq_zero_of_le]

Result:
no goals

Proof state:
case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
x : ℝ≥0∞
⊢ (x, a) ∈ {p | p ≠ (⊤, ⊤)}

Tactic:
simp only [a_infty, Ne, mem_setOf_eq, Prod.mk.inj_iff, and_false, not_false_iff]

Result:
no goals

Proof state:
a : ℝ≥0∞
⊢ Continuous fun x => x - a

Tactic:
by_cases a_infty : a = ∞

Result:
case pos
a : ℝ≥0∞
a_infty : a = ⊤
⊢ Continuous fun x => x - a

case neg
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ Continuous fun x => x - a

Proof state:
a : ℝ≥0∞
a_infty : ¬a = ⊤
⊢ (fun x => x - a) = (fun p => p.1 - p.2) ∘ fun x => (x, a)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/ZModChar.lean
theorem χ₈'_eq_χ₄_mul_χ₈ : ∀ a : ZMod 8, χ₈' a = χ₄ (cast a) * χ₈ a

Proof state:
⊢ ∀ (a : ZMod 8), χ₈' a = χ₄ a.cast * χ₈ a

Tactic:
decide

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H2Map_id : H2Map (MonoidHom.id _) (𝟙 A) = 𝟙 _

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ H2Map (MonoidHom.id H) (𝟙 A) = 𝟙 (H2 A)

Tactic:
simp only [H2Map, shortComplexH2, mapShortComplexH2_id, leftHomologyMap'_id]

Result:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ 𝟙 (moduleCatMk (dOne A) (dTwo A) ⋯).moduleCatLeftHomologyData.H = 𝟙 (H2 A)

Proof state:
k H : Type u
inst✝¹ : CommRing k
inst✝ : Group H
A : Rep k H
⊢ 𝟙 (moduleCatMk (dOne A) (dTwo A) ⋯).moduleCatLeftHomologyData.H = 𝟙 (H2 A)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem iInf_toSubalgebra {ι : Sort*} (S : ι → StarSubalgebra R A) :
    (⨅ i, S i).toSubalgebra = ⨅ i, (S i).toSubalgebra :=
  SetLike.coe_injective <| by simp

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i).toSubalgebra = ↑(⨅ i, (S i).toSubalgebra)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem indep_iff_not_dep : M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ ¬M.Dep I ∧ I ⊆ M.E

Tactic:
rw [dep_iff, not_and, not_imp_not]

Result:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I : Set α
⊢ M.Indep I ↔ (I ⊆ M.E → M.Indep I) ∧ I ⊆ M.E

Tactic:
exact ⟨fun h ↦ ⟨fun _ ↦ h, h.subset_ground⟩, fun h ↦ h.1 h.2⟩

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma one_lt_div_of_mem_properDivisors {m n : ℕ} (h : m ∈ n.properDivisors) :
    1 < n / m

Proof state:
m n : ℕ
h : m ∈ n.properDivisors
⊢ 1 < n / m

Tactic:
obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h

Result:
case intro
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ 1 < n / m

Proof state:
case intro
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ 1 < n / m

Tactic:
rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_int_lt_one_iff_dvd (k : ℤ) : ‖(k : ℚ_[p])‖ < 1 ↔ ↑p ∣ k

Proof state:
case mp.hab
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = 1

Tactic:
calc
  ‖(k : ℚ_[p])‖ = ‖((k : ℚ) : ℚ_[p])‖ := by norm_cast
  _ = padicNorm p k := padicNormE.eq_padicNorm _
  _ = 1 := mod_cast (int_eq_one_iff k).mpr h

Result:
no goals

Proof state:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * ‖↑x‖ < 1

Tactic:
calc
  _ ≤ ‖(p : ℚ_[p])‖ * 1 :=
    mul_le_mul le_rfl (by simpa using norm_int_le_one _) (norm_nonneg _) (norm_nonneg _)
  _ < 1 := by
    rw [mul_one, padicNormE.norm_p]
    exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑x‖ ≤ 1

Tactic:
simpa using norm_int_le_one _

Result:
no goals

Proof state:
case mp.hab
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 = ‖↑k‖

Tactic:
rw [eq_comm]

Result:
case mp.hab
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = 1

Proof state:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p * ↑x‖ < 1

Tactic:
rw [padicNormE.mul]

Result:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * ‖↑x‖ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 ↔ ↑p ∣ k

Tactic:
constructor

Result:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 → ↑p ∣ k

case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1

Proof state:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ‖↑k‖ < 1 → ↑p ∣ k

Tactic:
intro h

Result:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ‖↑k‖ < 1
⊢ ↑p ∣ k

Proof state:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 ≤ ‖↑k‖

Tactic:
apply le_of_eq

Result:
case mp.hab
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 = ‖↑k‖

Proof state:
case mpr
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
⊢ ↑p ∣ k → ‖↑k‖ < 1

Tactic:
rintro ⟨x, rfl⟩

Result:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑(↑p * x)‖ < 1

Proof state:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ‖↑k‖ < 1
⊢ ↑p ∣ k

Tactic:
contrapose! h

Result:
case mp
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ 1 ≤ ‖↑k‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℤ
h : ¬↑p ∣ k
⊢ ‖↑k‖ = ‖↑↑k‖

Tactic:
norm_cast

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p‖ * 1 < 1

Tactic:
rw [mul_one, padicNormE.norm_p]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ (↑p)⁻¹ < 1

Proof state:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑(↑p * x)‖ < 1

Tactic:
push_cast

Result:
case mpr.intro
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ ‖↑p * ↑x‖ < 1

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ
⊢ (↑p)⁻¹ < 1

Tactic:
exact inv_lt_one_of_one_lt₀ <| mod_cast hp.1.one_lt

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthonormal.lean
theorem Orthonormal.linearIndependent {v : ι → E} (hv : Orthonormal 𝕜 v) :
    LinearIndependent 𝕜 v

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
⊢ l i = 0 i

Tactic:
have key : ⟪v i, Finsupp.linearCombination 𝕜 v l⟫ = ⟪v i, 0⟫ := by rw [hl]

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
key : inner (v i) ((linearCombination 𝕜 v) l) = inner (v i) 0
⊢ l i = 0 i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (l : ι →₀ 𝕜), (linearCombination 𝕜 v) l = 0 → l = 0

Tactic:
intro l hl

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
⊢ l = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
⊢ l = 0

Tactic:
ext i

Result:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
⊢ l i = 0 i

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ LinearIndependent 𝕜 v

Tactic:
rw [linearIndependent_iff]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
⊢ ∀ (l : ι →₀ 𝕜), (linearCombination 𝕜 v) l = 0 → l = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
⊢ inner (v i) ((linearCombination 𝕜 v) l) = inner (v i) 0

Tactic:
rw [hl]

Result:
no goals

Proof state:
case h
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_4
v : ι → E
hv : Orthonormal 𝕜 v
l : ι →₀ 𝕜
hl : (linearCombination 𝕜 v) l = 0
i : ι
key : inner (v i) ((linearCombination 𝕜 v) l) = inner (v i) 0
⊢ l i = 0 i

Tactic:
simpa only [hv.inner_right_finsupp, inner_zero_right] using key

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSpace_min_const (hτ : IsStoppingTime f τ) {i : ι} :
    (hτ.min_const i).measurableSpace = hτ.measurableSpace ⊓ f i

Proof state:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → ι
hτ : IsStoppingTime f τ
i : ι
⊢ ⋯.measurableSpace = hτ.measurableSpace ⊓ ↑f i

Tactic:
rw [hτ.measurableSpace_min (isStoppingTime_const _ i), measurableSpace_const]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Field.lean
theorem Polynomial.lift_of_splits {F K L : Type*} [Field F] [Field K] [Field L] [Algebra F K]
    [Algebra F L] (s : Finset K) : (∀ x ∈ s, IsIntegral F x ∧
      Splits (algebraMap F L) (minpoly F x)) → Nonempty (Algebra.adjoin F (s : Set K) →ₐ[F] L)

Proof state:
case refine_2.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : Splits (algebraMap (↥Ks) L) (minpoly (↥Ks) a)
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)

Tactic:
obtain ⟨y, hy⟩ := Polynomial.exists_root_of_splits _ H6 (minpoly.degree_pos H5).ne'

Result:
case refine_2.intro.intro.intro.intro
F : Type u_2
K : Type u_3
L : Type u_4
inst✝⁴ : Field F
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra F K
inst✝ : Algebra F L
s✝ : Finset K
a : K
s : Finset K
x✝ : a ∉ s
H1 : IsIntegral F a
H2 : Splits (algebraMap F L) (minpoly F a)
H3 : ∀ x ∈ s, IsIntegral F x
a✝ : ∀ x ∈ s, Splits (algebraMap F L) (minpoly F x)
Ks : Subalgebra F K := Algebra.adjoin F ↑s
ih : (∀ x ∈ s, IsIntegral F x ∧ Splits (algebraMap F L) (minpoly F x)) → Nonempty (↥Ks →ₐ[F] L)
f : ↥Ks →ₐ[F] L
this✝¹ : FiniteDimensional F ↥Ks
this✝ : Field ↥Ks := fieldOfFiniteDimensional F ↥Ks
this : Algebra (↥Ks) L := (↑f).toAlgebra
H5 : IsIntegral (↥Ks) a
H6 : Splits (algebraMap (↥Ks) L) (minpoly (↥Ks) a)
y : L
hy : eval₂ (algebraMap (↥Ks) L) y (minpoly (↥Ks) a) = 0
⊢ Nonempty (↥(Subalgebra.restrictScalars F (Algebra.adjoin ↥Ks {a})) →ₐ[F] L)
-- Mathlib/Data/PFunctor/Univariate/M.lean
theorem agree_children {n : ℕ} (x : CofixA F (succ n)) (y : CofixA F (succ n + 1)) {i j}
    (h₀ : HEq i j) (h₁ : Agree x y) : Agree (children' x i) (children' y j)

Proof state:
F : PFunctor.{u}
n : ℕ
x : CofixA F n.succ
y : CofixA F (n.succ + 1)
i : F.B (head' x)
j : F.B (head' y)
h₀ : HEq i j
h₁ : Agree x y
⊢ Agree (children' x i) (children' y j)

Tactic:
obtain - | ⟨_, _, hagree⟩ := h₁

Result:
case intro
F : PFunctor.{u}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
j : F.B (head' (CofixA.intro a✝ x'✝))
h₀ : HEq i j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)

Proof state:
case intro.refl
F : PFunctor.{u}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)

Tactic:
apply hagree

Result:
no goals

Proof state:
case intro
F : PFunctor.{u}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
j : F.B (head' (CofixA.intro a✝ x'✝))
h₀ : HEq i j
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) j)

Tactic:
cases h₀

Result:
case intro.refl
F : PFunctor.{u}
n✝ n : ℕ
a✝ : F.A
x✝ : F.B a✝ → CofixA F n✝
x'✝ : F.B a✝ → CofixA F (n✝ + 1)
hagree : ∀ (i : F.B a✝), Agree (x✝ i) (x'✝ i)
i : F.B (head' (CofixA.intro a✝ x✝))
⊢ Agree (children' (CofixA.intro a✝ x✝) i) (children' (CofixA.intro a✝ x'✝) i)
-- Mathlib/Algebra/Regular/SMul.lean
theorem of_mul [Mul R] [IsScalarTower R R M] (ab : IsSMulRegular M (a * b)) :
    IsSMulRegular M b

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b

Tactic:
exact ab.of_smul _

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M b

Tactic:
rw [← smul_eq_mul] at ab

Result:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp)]
lemma mulConst_empty_left (B : Finset G) : σₘ[∅, B] = 0

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
B : Finset G
⊢ σₘ[∅, B] = 0

Tactic:
simp [mulConst]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_right (n : Nat) {m : Nat} (H : 0 < m) : m * n / m = n

Proof state:
n m : Nat
H : 0 < m
⊢ m * n / m = n

Tactic:
induction n <;> simp_all [mul_succ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_eq_eraseP [LawfulBEq α] (a : α) (l : Array α) : l.erase a = l.eraseP (a == ·)

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : Array α
⊢ l.erase a = l.eraseP fun x => a == x

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.erase a = { toList := l }.eraseP fun x => a == x

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
⊢ { toList := l }.erase a = { toList := l }.eraseP fun x => a == x

Tactic:
simp [List.erase_eq_eraseP]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem measurable_tProd_elim [DecidableEq δ] :
    ∀ {l : List δ} {i : δ} (hi : i ∈ l), Measurable fun v : TProd π l => v.elim hi
  | i::is, j, hj => by
    by_cases hji : j = i
    · subst hji
      simpa using measurable_fst
    · simp only [TProd.elim_of_ne _ hji]
      rw [mem_cons] at hj
      exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

Proof state:
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
⊢ Measurable fun v => v.elim hj

Tactic:
by_cases hji : j = i

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v => v.elim hj

case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => v.elim hj

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.2 ⋯

Tactic:
rw [mem_cons] at hj

Result:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj✝ : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.2 ⋯

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj✝ : j ∈ i :: is
hj : j = i ∨ j ∈ is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.2 ⋯

Tactic:
exact (measurable_tProd_elim (hj.resolve_left hji)).comp measurable_snd

Result:
no goals

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v => v.elim hj

Tactic:
simpa using measurable_fst

Result:
no goals

Proof state:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : j = i
⊢ Measurable fun v => v.elim hj

Tactic:
subst hji

Result:
case pos
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
is : List δ
j : δ
hj : j ∈ j :: is
⊢ Measurable fun v => v.elim hj

Proof state:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => v.elim hj

Tactic:
simp only [TProd.elim_of_ne _ hji]

Result:
case neg
δ : Type u_4
π : δ → Type u_6
inst✝¹ : (x : δ) → MeasurableSpace (π x)
inst✝ : DecidableEq δ
i : δ
is : List δ
j : δ
hj : j ∈ i :: is
hji : ¬j = i
⊢ Measurable fun v => TProd.elim v.2 ⋯