harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.tendsto_nhds_atTop (hp : WithSeminorms p) (u : F → E) (y₀ : E) :
    Filter.Tendsto u Filter.atTop (𝓝 y₀) ↔
    ∀ i ε, 0 < ε → ∃ x₀, ∀ x, x₀ ≤ x → p i (u x - y₀) < ε

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ Tendsto u atTop (𝓝 y₀) ↔ ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Tactic:
rw [hp.tendsto_nhds u y₀]

Result:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Proof state:
𝕜 : Type u_1
E : Type u_5
F : Type u_6
ι : Type u_8
inst✝⁶ : NormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module 𝕜 E
inst✝³ : Nonempty ι
inst✝² : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
inst✝¹ : SemilatticeSup F
inst✝ : Nonempty F
hp : WithSeminorms p
u : F → E
y₀ : E
⊢ (∀ (i : ι) (ε : ℝ), 0 < ε → ∀ᶠ (x : F) in atTop, (p i) (u x - y₀) < ε) ↔
    ∀ (i : ι) (ε : ℝ), 0 < ε → ∃ x₀, ∀ (x : F), x₀ ≤ x → (p i) (u x - y₀) < ε

Tactic:
exact forall₃_congr fun _ _ _ => Filter.eventually_atTop

Result:
no goals
-- Mathlib/MeasureTheory/Function/StronglyMeasurable/AEStronglyMeasurable.lean
theorem aefinStronglyMeasurable_iff_aemeasurable {_m0 : MeasurableSpace α} (μ : Measure α)
    [SigmaFinite μ] : AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ

Proof state:
α : Type u_1
G : Type u_5
inst✝⁴ : SeminormedAddCommGroup G
inst✝³ : MeasurableSpace G
inst✝² : BorelSpace G
inst✝¹ : SecondCountableTopology G
f : α → G
_m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
⊢ AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ

Tactic:
simp_rw [AEFinStronglyMeasurable, AEMeasurable, finStronglyMeasurable_iff_measurable]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_one' (h : y + 1 ≠ 0) (x : ℝ≥0) : x ^ (y + 1) = x ^ y * x

Proof state:
y : ℝ
h : y + 1 ≠ 0
x : ℝ≥0
⊢ x ^ (y + 1) = x ^ y * x

Tactic:
rw [rpow_add' h, rpow_one]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/SuccPred.lean
lemma Ioi_sub_one_eq_Ici_of_not_isMin (ha : ¬ IsMin a) : Ioi (a - 1) = Ici a

Proof state:
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : One α
inst✝¹ : Sub α
inst✝ : PredSubOrder α
a : α
ha : ¬IsMin a
⊢ Ioi (a - 1) = Ici a

Tactic:
simpa [pred_eq_sub_one] using Ioi_pred_eq_Ici_of_not_isMin ha

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioi_eq_empty : Ioi a = ∅ ↔ IsMax a

Proof state:
α : Type u_2
a : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Ioi a = ∅ ↔ IsMax a

Tactic:
rw [← coe_eq_empty, coe_Ioi, Set.Ioi_eq_empty_iff]

Result:
no goals
-- Mathlib/Data/List/Perm/Lattice.lean
theorem Perm.bagInter_left (l : List α) {t₁ t₂ : List α} (p : t₁ ~ t₂) :
    l.bagInter t₁ = l.bagInter t₂

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∉ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
simp [h, mt p.mem_iff.2 h, IH p]

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ [].bagInter t₁ = [].bagInter t₂

Tactic:
simp

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
simp [h, p.subset h, IH (p.erase _)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l t₁ t₂ : List α
p : t₁ ~ t₂
⊢ l.bagInter t₁ = l.bagInter t₂

Tactic:
induction' l with a l IH generalizing t₁ t₂ p

Result:
case nil
α : Type u_1
inst✝ : DecidableEq α
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ [].bagInter t₁ = [].bagInter t₂

case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Proof state:
case cons
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

Tactic:
by_cases h : a ∈ t₁

Result:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∈ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂

case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
l : List α
IH : ∀ {t₁ t₂ : List α}, t₁ ~ t₂ → l.bagInter t₁ = l.bagInter t₂
t₁ t₂ : List α
p : t₁ ~ t₂
h : a ∉ t₁
⊢ (a :: l).bagInter t₁ = (a :: l).bagInter t₂
-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_insertLeft_neg (x x' : PGame.{u}) : (-x).insertLeft (-x') = -x.insertRight x'

Proof state:
x x' : PGame
⊢ (-x).insertLeft (-x') = -x.insertRight x'

Tactic:
rw [← neg_eq_iff_eq_neg, ← neg_insertRight_neg, neg_neg, neg_neg]

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem toMeasureOfLEZero_toSignedMeasure (hs : s ≤[Set.univ] 0) :
    (s.toMeasureOfLEZero Set.univ MeasurableSet.univ hs).toSignedMeasure = -s

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
i : Set α
hi : MeasurableSet i
⊢ ↑(s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure i = ↑(-s) i

Tactic:
simp [hi, toMeasureOfLEZero_apply _ _ _ hi]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
⊢ (s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure = -s

Tactic:
ext i hi

Result:
case h
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
hs : s ≤[univ] 0
i : Set α
hi : MeasurableSet i
⊢ ↑(s.toMeasureOfLEZero univ ⋯ hs).toSignedMeasure i = ↑(-s) i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem push_toArray_fun (l : List α) : l.toArray.push = fun a => (l ++ [a]).toArray

Proof state:
α : Type u_1
l : List α
⊢ l.toArray.push = fun a => (l ++ [a]).toArray

Tactic:
funext a

Result:
case h
α : Type u_1
l : List α
a : α
⊢ l.toArray.push a = (l ++ [a]).toArray

Proof state:
case h
α : Type u_1
l : List α
a : α
⊢ l.toArray.push a = (l ++ [a]).toArray

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `div_lt_iff₀'` for a version with multiplication on the other side. -/
lemma div_lt_iff₀ (hc : 0 < c) : b / c < a ↔ b < a * c

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : MulPosStrictMono G₀
hc : 0 < c
⊢ b / c < a ↔ b < a * c

Tactic:
rw [div_eq_mul_inv, mul_inv_lt_iff₀ hc]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive (attr := simp)]
lemma map_comp_mul [MulHomClass F M N] (f : F) (g h : ι → M) : f ∘ (g * h) = f ∘ g * f ∘ h

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
⊢ ⇑f ∘ (g * h) = ⇑f ∘ g * ⇑f ∘ h

Tactic:
ext

Result:
case h
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
x✝ : ι
⊢ (⇑f ∘ (g * h)) x✝ = (⇑f ∘ g * ⇑f ∘ h) x✝

Proof state:
case h
ι : Type u_1
M : Type u_4
N : Type u_5
F : Type u_9
inst✝³ : Mul M
inst✝² : Mul N
inst✝¹ : FunLike F M N
inst✝ : MulHomClass F M N
f : F
g h : ι → M
x✝ : ι
⊢ (⇑f ∘ (g * h)) x✝ = (⇑f ∘ g * ⇑f ∘ h) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_T_le (n : ℤ) : (T n : R[T;T⁻¹]).degree ≤ n :=
  (le_of_eq (by rw [map_one, one_mul])).trans (degree_C_mul_T_le n (1 : R))

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℤ
⊢ (T n).degree = (C 1 * T n).degree

Tactic:
rw [map_one, one_mul]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem subset_product_image_fst [DecidableEq α] : (s ×ˢ t).image Prod.fst ⊆ s := fun i => by
  simp +contextual [mem_image]

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
inst✝ : DecidableEq α
i : α
⊢ i ∈ image Prod.fst (s ×ˢ t) → i ∈ s

Tactic:
simp +contextual [mem_image]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/CochainComplex.lean
@[reassoc (attr := simp)]
lemma ιTruncLE_naturality (n : ℤ) :
    truncLEMap φ n ≫ L.ιTruncLE n = K.ιTruncLE n ≫ φ

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_2, u_1} C
inst✝³ : HasZeroMorphisms C
K L : CochainComplex C ℤ
φ : K ⟶ L
inst✝² : HasZeroObject C
inst✝¹ : ∀ (i : ℤ), HasHomology K i
inst✝ : ∀ (i : ℤ), HasHomology L i
n : ℤ
⊢ truncLEMap φ n ≫ L.ιTruncLE n = K.ιTruncLE n ≫ φ

Tactic:
apply HomologicalComplex.ιTruncLE_naturality

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_div_right (a b c : EReal) : a / b * c = a * c / b

Proof state:
a b c : EReal
⊢ a / b * c = a * c / b

Tactic:
rw [mul_comm, EReal.mul_div, mul_comm]

Result:
no goals
-- Mathlib/GroupTheory/Congruence/BigOperators.lean
theorem list_prod {ι M : Type*} [Monoid M] (c : Con M) {l : List ι} {f g : ι → M}
    (h : ∀ x ∈ l, c (f x) (g x)) :
    c (l.map f).prod (l.map g).prod

Proof state:
ι : Type u_1
M : Type u_2
inst✝ : Monoid M
c : Con M
l : List ι
f g : ι → M
h : ∀ x ∈ l, c (f x) (g x)
⊢ c (List.map f l).prod (List.map g l).prod

Tactic:
induction l with
| nil =>
  simpa only [List.map_nil, List.prod_nil] using c.refl 1
| cons x xs ih =>
  rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]
  exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

Result:
no goals

Proof state:
case nil
ι : Type u_1
M : Type u_2
inst✝ : Monoid M
c : Con M
f g : ι → M
h : ∀ x ∈ [], c (f x) (g x)
⊢ c (List.map f []).prod (List.map g []).prod

Tactic:
simpa only [List.map_nil, List.prod_nil] using c.refl 1

Result:
no goals

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝ : Monoid M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (List.map f (x :: xs)).prod (List.map g (x :: xs)).prod

Tactic:
rw [List.map_cons, List.map_cons, List.prod_cons, List.prod_cons]

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝ : Monoid M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝ : Monoid M
c : Con M
f g : ι → M
x : ι
xs : List ι
ih : (∀ x ∈ xs, c (f x) (g x)) → c (List.map f xs).prod (List.map g xs).prod
h : ∀ x_1 ∈ x :: xs, c (f x_1) (g x_1)
⊢ c (f x * (List.map f xs).prod) (g x * (List.map g xs).prod)

Tactic:
exact c.mul (h _ <| .head _) <| ih fun k hk ↦ h _ (.tail _ hk)

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
theorem add_one_lt_of_even (hn : Even n) (hm : Even m) (hnm : n < m) :
    n + 1 < m

Proof state:
m n : ℕ
hn : Even n
hm : Even m
hnm : n < m
⊢ n + 1 < m

Tactic:
rcases hn with ⟨n, rfl⟩

Result:
case intro
m : ℕ
hm : Even m
n : ℕ
hnm : n + n < m
⊢ n + n + 1 < m

Proof state:
case intro.intro
n m : ℕ
hnm : n + n < m + m
⊢ n + n + 1 < m + m

Tactic:
omega

Result:
no goals

Proof state:
case intro
m : ℕ
hm : Even m
n : ℕ
hnm : n + n < m
⊢ n + n + 1 < m

Tactic:
rcases hm with ⟨m, rfl⟩

Result:
case intro.intro
n m : ℕ
hnm : n + n < m + m
⊢ n + n + 1 < m + m
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem exists_fixed_point_of_prime' {p n : ℕ} [hp : Fact p.Prime] (hα : p ∣ Fintype.card α)
    {σ : Perm α} (hσ : σ ^ p ^ n = 1) {a : α} (ha : σ a = a) : ∃ b : α, σ b = b ∧ b ≠ a

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
classical
  have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
    rw [Finset.mem_compl, mem_support, Classical.not_not]
  obtain ⟨b, hb1, hb2⟩ := Finset.exists_ne_of_one_lt_card (hp.out.one_lt.trans_le
    (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
      ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a
  exact ⟨b, (h b).mp hb1, hb2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
have h : ∀ b : α, b ∈ σ.supportᶜ ↔ σ b = b := fun b => by
  rw [Finset.mem_compl, mem_support, Classical.not_not]

Result:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
⊢ ∃ b, σ b = b ∧ b ≠ a

Proof state:
case intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
b : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
exact ⟨b, (h b).mp hb1, hb2⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
b : α
⊢ b ∈ σ.supportᶜ ↔ σ b = b

Tactic:
rw [Finset.mem_compl, mem_support, Classical.not_not]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
⊢ ∃ b, σ b = b ∧ b ≠ a

Tactic:
obtain ⟨b, hb1, hb2⟩ := Finset.exists_ne_of_one_lt_card (hp.out.one_lt.trans_le
  (Nat.le_of_dvd (Finset.card_pos.mpr ⟨a, (h a).mpr ha⟩) (Nat.modEq_zero_iff_dvd.mp
    ((card_compl_support_modEq hσ).trans (Nat.modEq_zero_iff_dvd.mpr hα))))) a

Result:
case intro.intro
α : Type u_1
inst✝ : Fintype α
p n : ℕ
hp : Fact (Nat.Prime p)
hα : p ∣ Fintype.card α
σ : Perm α
hσ : σ ^ p ^ n = 1
a : α
ha : σ a = a
h : ∀ (b : α), b ∈ σ.supportᶜ ↔ σ b = b
b : α
hb1 : b ∈ σ.supportᶜ
hb2 : b ≠ a
⊢ ∃ b, σ b = b ∧ b ≠ a
-- Mathlib/GroupTheory/FreeGroup/Reduce.lean
theorem norm_surjective [Nonempty α] : Function.Surjective (norm (α := α))

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
a : α
⊢ Function.Surjective norm

Tactic:
exact Function.RightInverse.surjective <| norm_of_pow a

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
⊢ Function.Surjective norm

Tactic:
let ⟨a⟩ := ‹Nonempty α›

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Nonempty α
a : α
⊢ Function.Surjective norm
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_adjoin_simple_eq_natSepDegree {α : E} (halg : IsAlgebraic F α) :
    finSepDegree F F⟮α⟯ = (minpoly F α).natSepDegree

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
have : finSepDegree F F⟮α⟯ = _ := Nat.card_congr
  (algHomAdjoinIntegralEquiv F (K := AlgebraicClosure F⟮α⟯) halg.isIntegral)

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } =
    Fintype.card { x // x ∈ ((minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯)).toFinset }

Tactic:
simp_rw [Multiset.mem_toFinset]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
classical
rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
  ← Fintype.card_coe]
simp_rw [Multiset.mem_toFinset]

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ finSepDegree F ↥F⟮α⟯ = (minpoly F α).natSepDegree

Tactic:
rw [this, Nat.card_eq_fintype_card, natSepDegree_eq_of_isAlgClosed (E := AlgebraicClosure F⟮α⟯),
  ← Fintype.card_coe]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
this : finSepDegree F ↥F⟮α⟯ = Nat.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) }
⊢ Fintype.card { x // x ∈ (minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯) } =
    Fintype.card { x // x ∈ ((minpoly F α).aroots (AlgebraicClosure ↥F⟮α⟯)).toFinset }
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_ofNat (n : ℕ) [n.AtLeastTwo] :
    ((ofNat(n) : ℤ) : R) = ofNat(n)

Proof state:
R : Type u
inst✝¹ : AddGroupWithOne R
n : ℕ
inst✝ : n.AtLeastTwo
⊢ ↑(OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simpa only [OfNat.ofNat] using AddGroupWithOne.intCast_ofNat (R := R) n

Result:
no goals
-- Mathlib/Topology/Path.lean
theorem refl_reparam {f : I → I} (hfcont : Continuous f) (hf₀ : f 0 = 0) (hf₁ : f 1 = 1) :
    (refl x).reparam f hfcont hf₀ hf₁ = refl x

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
⊢ (refl x).reparam f hfcont hf₀ hf₁ = refl x

Tactic:
ext

Result:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ((refl x).reparam f hfcont hf₀ hf₁) x✝ = (refl x) x✝

Proof state:
case a.h
X : Type u_1
inst✝ : TopologicalSpace X
x : X
f : ↑I → ↑I
hfcont : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
x✝ : ↑I
⊢ ((refl x).reparam f hfcont hf₀ hf₁) x✝ = (refl x) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Midpoint.lean
theorem midpoint_add_self (x y : V) : midpoint R x y + midpoint R x y = x + y :=
  calc
    midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y +ᵥ midpoint R y x = x + y

Tactic:
rw [midpoint_vadd_midpoint, vadd_eq_add, vadd_eq_add, add_comm, midpoint_self]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
inst✝³ : Ring R
inst✝² : Invertible 2
inst✝¹ : AddCommGroup V
inst✝ : Module R V
x y : V
⊢ midpoint R x y +ᵥ midpoint R x y = midpoint R x y +ᵥ midpoint R y x

Tactic:
rw [midpoint_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_nil (h : m.WF) :
    insertMany m [] = m

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
⊢ insertMany m [] = m

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ []).val.val = m

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ []).val.val = m

Tactic:
rw [Raw₀.Const.insertMany_nil]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem eq_of_mem_uIcc_of_mem_uIcc' : b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simp_rw [mem_uIcc]

Result:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c

Proof state:
α : Type u_2
inst✝¹ : DistribLattice α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc'

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma asympBound_def' {α} [Fintype α] (a b : α → ℝ) {n : ℕ} :
    asympBound g a b n = n ^ p a b * (1 + (∑ u ∈ range n, g u / u ^ (p a b + 1)))

Proof state:
g : ℝ → ℝ
α : Type u_2
inst✝ : Fintype α
a b : α → ℝ
n : ℕ
⊢ asympBound g a b n = ↑n ^ p a b * (1 + ∑ u ∈ range n, g ↑u / ↑u ^ (p a b + 1))

Tactic:
simp [asympBound_def, sumTransform, mul_add, mul_one, Finset.sum_Ico_eq_sum_range]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem ContinuousAt.comp_lowerSemicontinuousAt {g : γ → δ} {f : α → γ} (hg : ContinuousAt g (f x))
    (hf : LowerSemicontinuousAt f x) (gmon : Monotone g) : LowerSemicontinuousAt (g ∘ f) x

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x

Tactic:
exact hg.comp_lowerSemicontinuousWithinAt hf gmon

Result:
no goals

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
hf : LowerSemicontinuousAt f x
gmon : Monotone g
⊢ LowerSemicontinuousAt (g ∘ f) x

Tactic:
simp only [← lowerSemicontinuousWithinAt_univ_iff] at hf ⊢

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
x : α
γ : Type u_3
inst✝⁵ : LinearOrder γ
inst✝⁴ : TopologicalSpace γ
inst✝³ : OrderTopology γ
δ : Type u_4
inst✝² : LinearOrder δ
inst✝¹ : TopologicalSpace δ
inst✝ : OrderTopology δ
g : γ → δ
f : α → γ
hg : ContinuousAt g (f x)
gmon : Monotone g
hf : LowerSemicontinuousWithinAt f univ x
⊢ LowerSemicontinuousWithinAt (g ∘ f) univ x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem and_le_left {n m : Nat} : n &&& m ≤ n :=
  le_of_testBit (by simpa using fun i x _ => x)

Proof state:
n m : Nat
⊢ ∀ (i : Nat), (n &&& m).testBit i = true → n.testBit i = true

Tactic:
simpa using fun i x _ => x

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/Basic.lean
theorem mod (a : ℤ) : legendreSym p a = legendreSym p (a % p)

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
⊢ legendreSym p a = legendreSym p (a % ↑p)

Tactic:
simp only [legendreSym, intCast_mod]

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Tagged.lean
theorem mem_filter {p : Box ι → Prop} : J ∈ π.filter p ↔ J ∈ π ∧ p J

Proof state:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
classical exact Finset.mem_filter

Result:
no goals

Proof state:
ι : Type u_1
I J : Box ι
π : TaggedPrepartition I
p : Box ι → Prop
⊢ J ∈ π.filter p ↔ J ∈ π ∧ p J

Tactic:
exact Finset.mem_filter

Result:
no goals