harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Floor.lean
theorem floor_congr (h : ∀ n : ℕ, (n : α) ≤ a ↔ (n : β) ≤ b) : ⌊a⌋₊ = ⌊b⌋₊

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ 0 ≤ a ↔ 0 ≤ b

Tactic:
simpa only [cast_zero] using h 0

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
obtain ha | ha := lt_or_le a 0

Result:
case inl
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

case inr
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊

Proof state:
case inr
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : 0 ≤ a
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
exact (le_floor <| (h _).1 <| floor_le ha).antisymm (le_floor <| (h _).2 <| floor_le <| h₀.1 ha)

Result:
no goals

Proof state:
case inl
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
ha : a < 0
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
rw [floor_of_nonpos ha.le, floor_of_nonpos (le_of_not_le <| h₀.not.mp ha.not_le)]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊

Tactic:
have h₀ : 0 ≤ a ↔ 0 ≤ b := by simpa only [cast_zero] using h 0

Result:
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedSemiring α
inst✝² : LinearOrderedSemiring β
inst✝¹ : FloorSemiring α
inst✝ : FloorSemiring β
a : α
b : β
h : ∀ (n : ℕ), ↑n ≤ a ↔ ↑n ≤ b
h₀ : 0 ≤ a ↔ 0 ≤ b
⊢ ⌊a⌋₊ = ⌊b⌋₊
-- Mathlib/FieldTheory/CardinalEmb.lean
theorem cardinal_eq [Algebra.IsAlgebraic F E] :
    #(Field.Emb F E) = (fun c ↦ if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ #(Emb F E) = (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E)

Tactic:
rw [← cardinal_separableClosure, cardinal_eq_of_isSeparable]

Result:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F ↥(separableClosure F E)) =
    (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E)

Proof state:
F : Type u
E : Type v
inst✝³ : Field F
inst✝² : Field E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsAlgebraic F E
⊢ (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (Module.rank F ↥(separableClosure F E)) =
    (fun c => if ℵ₀ ≤ c then 2 ^ c else c) (sepDegree F E)

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addX_neg {P : Fin 3 → R} (hP : W'.Equation P) : W'.addX P (W'.neg P) = W'.dblZ P ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P (W'.neg P) = W'.dblZ P ^ 2

Tactic:
linear_combination (norm := (rw [addX, neg_X, neg_Y, neg_Z, dblZ, negY]; ring1))
  -2 * P z ^ 2 * (equation_iff _).mp hP

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z +
                          P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      ((P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
ring1

Result:
no goals

Proof state:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ W'.addX P (W'.neg P) + -2 * P z ^ 2 * 0 -
      (W'.dblZ P ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0

Tactic:
rw [addX, neg_X, neg_Y, neg_Z, dblZ, negY]

Result:
case a.a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ P x * P x ^ 2 * P z ^ 2 - 2 * P y * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z * P z +
                          P x ^ 2 * P x * P z ^ 2 -
                        W'.a₁ * P x * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 2 * P z -
                      W'.a₁ * P y * P x * P z * P z ^ 2 +
                    2 * W'.a₂ * P x * P x * P z ^ 2 * P z ^ 2 -
                  W'.a₃ * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) * P z ^ 4 * P z -
                W'.a₃ * P y * P z * P z ^ 4 +
              W'.a₄ * P x * P z ^ 4 * P z ^ 2 +
            W'.a₄ * P x * P z ^ 2 * P z ^ 4 +
          2 * W'.a₆ * P z ^ 4 * P z ^ 4 +
        -2 * P z ^ 2 * 0 -
      ((P z * (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3))) ^ 2 +
        -2 * P z ^ 2 *
          (P y ^ 2 + W'.a₁ * P x * P y * P z + W'.a₃ * P y * P z ^ 3 -
            (P x ^ 3 + W'.a₂ * P x ^ 2 * P z ^ 2 + W'.a₄ * P x * P z ^ 4 + W'.a₆ * P z ^ 6))) =
    0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_inj {s₁ s₂ t₁ t₂ : Array α} (h : s₁ ++ t₁ = s₂ ++ t₂) (hl : s₁.size = s₂.size) :
    s₁ = s₂ ∧ t₁ = t₂

Proof state:
case mk.mk
α : Type u_1
t₁ t₂ : Array α
s₁ s₂ : List α
h : { toList := s₁ } ++ t₁ = { toList := s₂ } ++ t₂
hl : { toList := s₁ }.size = { toList := s₂ }.size
⊢ { toList := s₁ } = { toList := s₂ } ∧ t₁ = t₂

Tactic:
rcases t₁ with ⟨t₁⟩

Result:
case mk.mk.mk
α : Type u_1
t₂ : Array α
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ t₂
⊢ { toList := s₁ } = { toList := s₂ } ∧ { toList := t₁ } = t₂

Proof state:
α : Type u_1
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ t₂ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ { toList := t₂ }
⊢ s₁.length = s₂.length

Tactic:
simpa using hl

Result:
no goals

Proof state:
α : Type u_1
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ t₂ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ { toList := t₂ }
⊢ s₁ ++ t₁ = s₂ ++ t₂

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk.mk.mk.mk
α : Type u_1
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ t₂ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ { toList := t₂ }
⊢ { toList := s₁ } = { toList := s₂ } ∧ { toList := t₁ } = { toList := t₂ }

Tactic:
simpa using List.append_inj (by simpa using h) (by simpa using hl)

Result:
no goals

Proof state:
case mk.mk.mk
α : Type u_1
t₂ : Array α
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ t₂
⊢ { toList := s₁ } = { toList := s₂ } ∧ { toList := t₁ } = t₂

Tactic:
rcases t₂ with ⟨t₂⟩

Result:
case mk.mk.mk.mk
α : Type u_1
s₁ s₂ : List α
hl : { toList := s₁ }.size = { toList := s₂ }.size
t₁ t₂ : List α
h : { toList := s₁ } ++ { toList := t₁ } = { toList := s₂ } ++ { toList := t₂ }
⊢ { toList := s₁ } = { toList := s₂ } ∧ { toList := t₁ } = { toList := t₂ }

Proof state:
α : Type u_1
s₁ s₂ t₁ t₂ : Array α
h : s₁ ++ t₁ = s₂ ++ t₂
hl : s₁.size = s₂.size
⊢ s₁ = s₂ ∧ t₁ = t₂

Tactic:
rcases s₁ with ⟨s₁⟩

Result:
case mk
α : Type u_1
s₂ t₁ t₂ : Array α
s₁ : List α
h : { toList := s₁ } ++ t₁ = s₂ ++ t₂
hl : { toList := s₁ }.size = s₂.size
⊢ { toList := s₁ } = s₂ ∧ t₁ = t₂

Proof state:
case mk
α : Type u_1
s₂ t₁ t₂ : Array α
s₁ : List α
h : { toList := s₁ } ++ t₁ = s₂ ++ t₂
hl : { toList := s₁ }.size = s₂.size
⊢ { toList := s₁ } = s₂ ∧ t₁ = t₂

Tactic:
rcases s₂ with ⟨s₂⟩

Result:
case mk.mk
α : Type u_1
t₁ t₂ : Array α
s₁ s₂ : List α
h : { toList := s₁ } ++ t₁ = { toList := s₂ } ++ t₂
hl : { toList := s₁ }.size = { toList := s₂ }.size
⊢ { toList := s₁ } = { toList := s₂ } ∧ t₁ = t₂
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem lt_irrefl : ∀ (x : Bool), ¬ x < x

Proof state:
⊢ ∀ (x : Bool), ¬x < x

Tactic:
decide

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem StrictMonoOn.strictConvexOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : StrictMonoOn (deriv f) (interior D)) : StrictConvexOn ℝ D f :=
  strictConvexOn_of_slope_strict_mono_adjacent hD fun {x y z} hx hz hxy hyz => by
    -- First we prove some trivial inclusions
    have hxzD : Icc x z ⊆ D := hD.ordConnected.out hx hz
    have hxyD : Icc x y ⊆ D := (Icc_subset_Icc_right hyz.le).trans hxzD
    have hxyD' : Ioo x y ⊆ interior D :=
      subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hxyD⟩
    have hyzD : Icc y z ⊆ D := (Icc_subset_Icc_left hxy.le).trans hxzD
    have hyzD' : Ioo y z ⊆ interior D :=
      subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩
    -- Then we get points `a` and `b` in each interval `[x, y]` and `[y, z]` where the derivatives
    -- can be compared to the slopes between `x, y` and `y, z` respectively.
    obtain ⟨a, ⟨hxa, hay⟩, ha⟩ : ∃ a ∈ Ioo x y, (f y - f x) / (y - x) < deriv f a :=
      StrictMonoOn.exists_slope_lt_deriv (hf.mono hxyD) hxy (hf'.mono hxyD')
    obtain ⟨b, ⟨hyb, hbz⟩, hb⟩ : ∃ b ∈ Ioo y z, deriv f b < (f z - f y) / (z - y) :=
      StrictMonoOn.exists_deriv_lt_slope (hf.mono hyzD) hyz (hf'.mono hyzD')
    apply ha.trans (lt_trans _ hb)
    exact hf' (hxyD' ⟨hxa, hay⟩) (hyzD' ⟨hyb, hbz⟩) (hay.trans hyb)

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)

Tactic:
have hyzD' : Ioo y z ⊆ interior D :=
  subset_sUnion_of_mem ⟨isOpen_Ioo, Ioo_subset_Icc_self.trans hyzD⟩

Result:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : StrictMonoOn (deriv f) (interior D)
x y z : ℝ
hx : x ∈ D
hz : z ∈ D
hxy : x < y
hyz : y < z
hxzD : Icc x z ⊆ D
hxyD : Icc x y ⊆ D
hxyD' : Ioo x y ⊆ interior D
hyzD : Icc y z ⊆ D
hyzD' : Ioo y z ⊆ interior D
⊢ (f y - f x) / (y - x) < (f z - f y) / (z - y)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n) {a : α} :
    l.setIfInBounds n a = l

Proof state:
case mk
α : Type u_1
n : Nat
a : α
toList✝ : List α
h : { toList := toList✝ }.size ≤ n
⊢ { toList := toList✝ }.setIfInBounds n a = { toList := toList✝ }

Tactic:
simp [List.set_eq_of_length_le (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
l : Array α
n : Nat
h : l.size ≤ n
a : α
⊢ l.setIfInBounds n a = l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
a : α
toList✝ : List α
h : { toList := toList✝ }.size ≤ n
⊢ { toList := toList✝ }.setIfInBounds n a = { toList := toList✝ }

Proof state:
α : Type u_1
n : Nat
a : α
toList✝ : List α
h : { toList := toList✝ }.size ≤ n
⊢ List.length ?m.138198 ≤ ?m.138199

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma hasFPowerSeriesOnBall_inv_one_sub
    (𝕜 𝕝 : Type*) [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕝] [NormedAlgebra 𝕜 𝕝] :
    HasFPowerSeriesOnBall (fun x : 𝕝 ↦ (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Proof state:
𝕜 : Type u_9
𝕝 : Type u_10
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
⊢ HasFPowerSeriesOnBall (fun x => (1 - x)⁻¹) (formalMultilinearSeries_geometric 𝕜 𝕝) 0 1

Tactic:
convert hasFPowerSeriesOnBall_inverse_one_sub 𝕜 𝕝

Result:
case h.e'_9.h.h.e
𝕜 : Type u_9
𝕝 : Type u_10
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
x✝ : 𝕝
⊢ Inv.inv = Ring.inverse

Proof state:
case h.e'_9.h.h.e
𝕜 : Type u_9
𝕝 : Type u_10
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕝
inst✝ : NormedAlgebra 𝕜 𝕝
x✝ : 𝕝
⊢ Inv.inv = Ring.inverse

Tactic:
exact Ring.inverse_eq_inv'.symm

Result:
no goals
-- Mathlib/Data/NNRat/Defs.lean
lemma divNat_inj (h₁ : d₁ ≠ 0) (h₂ : d₂ ≠ 0) : divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Proof state:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ divNat n₁ d₁ = divNat n₂ d₂ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
rw [← coe_inj]

Result:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁

Proof state:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑(divNat n₁ d₁) = ↑(divNat n₂ d₂) ↔ n₁ * d₂ = n₂ * d₁

Tactic:
simp [Rat.mkRat_eq_iff, h₁, h₂]

Result:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁ ↔ n₁ * d₂ = n₂ * d₁

Proof state:
n₁ n₂ d₁ d₂ : ℕ
h₁ : d₁ ≠ 0
h₂ : d₂ ≠ 0
⊢ ↑n₁ * ↑d₂ = ↑n₂ * ↑d₁ ↔ n₁ * d₂ = n₂ * d₁

Tactic:
norm_cast

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma rootOfSplitsXPowSubC_pow [NeZero n] :
    (rootOfSplitsXPowSubC (NeZero.pos n) a L) ^ n = algebraMap K L a

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this : ∀ (hfd : (X ^ n - C a).degree ≠ 0), rootOfSplits (algebraMap K L) ⋯ hfd ^ n = (algebraMap K L) a
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Tactic:
exact this _

Result:
no goals

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this :
  ∀ (hfd : (X ^ n - C a).degree ≠ 0), eval₂ (algebraMap K L) (rootOfSplits (algebraMap K L) ⋯ hfd) (X ^ n - C a) = 0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Tactic:
simp only [eval₂_sub, eval₂_X_pow, eval₂_C, sub_eq_zero] at this

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this : ∀ (hfd : (X ^ n - C a).degree ≠ 0), rootOfSplits (algebraMap K L) ⋯ hfd ^ n = (algebraMap K L) a
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Proof state:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a

Tactic:
have := map_rootOfSplits _ (IsSplittingField.splits L (X ^ n - C a))

Result:
K : Type u
inst✝⁴ : Field K
n : ℕ
a : K
L : Type u_1
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : IsSplittingField K L (X ^ n - C a)
inst✝ : NeZero n
this :
  ∀ (hfd : (X ^ n - C a).degree ≠ 0), eval₂ (algebraMap K L) (rootOfSplits (algebraMap K L) ⋯ hfd) (X ^ n - C a) = 0
⊢ rootOfSplitsXPowSubC ⋯ a L ^ n = (algebraMap K L) a
-- Mathlib/Algebra/Symmetrized.lean
theorem mul_comm [Mul α] [AddCommSemigroup α] [One α] [OfNat α 2] [Invertible (2 : α)]
    (a b : αˢʸᵐ) :
    a * b = b * a

Proof state:
α : Type u_1
inst✝⁴ : Mul α
inst✝³ : AddCommSemigroup α
inst✝² : One α
inst✝¹ : OfNat α 2
inst✝ : Invertible 2
a b : αˢʸᵐ
⊢ a * b = b * a

Tactic:
rw [mul_def, mul_def, add_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem snd_eq_coprod : snd R M M₂ = coprod 0 LinearMap.id

Proof state:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (snd R M M₂) x✝ = (coprod 0 id) x✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
⊢ snd R M M₂ = coprod 0 id

Tactic:
ext

Result:
case h
R : Type u
M : Type v
M₂ : Type w
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
x✝ : M × M₂
⊢ (snd R M M₂) x✝ = (coprod 0 id) x✝
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_moveLeft_inl {x : PGame} (y : PGame) (i) :
    (x + y).moveLeft (toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesAdd (Sum.inl i)) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i + mk α✝ β✝ a✝¹ a✝

Tactic:
rfl

Result:
no goals

Proof state:
x y : PGame
i : x.LeftMoves
⊢ (x + y).moveLeft (toLeftMovesAdd (Sum.inl i)) = x.moveLeft i + y

Tactic:
cases x

Result:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveLeft (toLeftMovesAdd (Sum.inl i)) = (mk α✝ β✝ a✝¹ a✝).moveLeft i + y

Proof state:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).LeftMoves
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveLeft (toLeftMovesAdd (Sum.inl i)) = (mk α✝ β✝ a✝¹ a✝).moveLeft i + y

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).LeftMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveLeft (toLeftMovesAdd (Sum.inl i)) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveLeft i + mk α✝ β✝ a✝¹ a✝
-- Mathlib/Analysis/Polynomial/Basic.lean
theorem abs_tendsto_atTop (hdeg : 0 < P.degree) :
    Tendsto (fun x => abs <| eval x P) atTop atTop

Proof state:
case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (fun x => |eval x P|) atTop atTop

Tactic:
exact tendsto_abs_atBot_atTop.comp (P.tendsto_atBot_of_leadingCoeff_nonpos hdeg hP)

Result:
no goals

Proof state:
case inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : 0 ≤ P.leadingCoeff
⊢ Tendsto (fun x => |eval x P|) atTop atTop

Tactic:
exact tendsto_abs_atTop_atTop.comp (P.tendsto_atTop_of_leadingCoeff_nonneg hdeg hP)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
⊢ Tendsto (fun x => |eval x P|) atTop atTop

Tactic:
rcases le_total 0 P.leadingCoeff with hP | hP

Result:
case inl
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : 0 ≤ P.leadingCoeff
⊢ Tendsto (fun x => |eval x P|) atTop atTop

case inr
𝕜 : Type u_1
inst✝¹ : NormedLinearOrderedField 𝕜
P : 𝕜[X]
inst✝ : OrderTopology 𝕜
hdeg : 0 < P.degree
hP : P.leadingCoeff ≤ 0
⊢ Tendsto (fun x => |eval x P|) atTop atTop
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem monic_toSubring : Monic (toSubring p T hp) ↔ Monic p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).Monic ↔ p.Monic

Tactic:
simp_rw [Monic, leadingCoeff, natDegree_toSubring, ← coeff_toSubring p T hp]

Result:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
H : (p.toSubring T hp).coeff p.natDegree = 1
⊢ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Tactic:
rw [H, OneMemClass.coe_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
T : Subring R
hp : ↑p.coeffs ⊆ ↑T
⊢ (p.toSubring T hp).coeff p.natDegree = 1 ↔ ↑((p.toSubring T hp).coeff p.natDegree) = 1

Tactic:
exact ⟨fun H => by rw [H, OneMemClass.coe_one], fun H => Subtype.coe_injective H⟩

Result:
no goals
-- Mathlib/Order/Filter/Subsingleton.lean
theorem Subsingleton.exists_eq_pure [l.NeBot] (hl : l.Subsingleton) : ∃ a, l = pure a

Proof state:
α : Type u_1
l : Filter α
inst✝ : l.NeBot
hl : l.Subsingleton
⊢ ∃ a, l = pure a

Tactic:
rcases hl with ⟨s, hsl, hs⟩

Result:
case intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
s : Set α
hsl : s ∈ l
hs : s.Subsingleton
⊢ ∃ a, l = pure a

Proof state:
case intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
s : Set α
hsl : s ∈ l
hs : s.Subsingleton
⊢ ∃ a, l = pure a

Tactic:
rcases exists_eq_singleton_iff_nonempty_subsingleton.2 ⟨nonempty_of_mem hsl, hs⟩ with ⟨a, rfl⟩

Result:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
a : α
hsl : {a} ∈ l
hs : {a}.Subsingleton
⊢ ∃ a, l = pure a

Proof state:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
a : α
hsl : {a} ∈ l
hs : {a}.Subsingleton
⊢ ∃ a, l = pure a

Tactic:
refine ⟨a, (NeBot.le_pure_iff ‹_›).1 ?_⟩

Result:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
a : α
hsl : {a} ∈ l
hs : {a}.Subsingleton
⊢ l ≤ pure a

Proof state:
case intro.intro.intro
α : Type u_1
l : Filter α
inst✝ : l.NeBot
a : α
hsl : {a} ∈ l
hs : {a}.Subsingleton
⊢ l ≤ pure a

Tactic:
rwa [le_pure_iff]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem aleph_limit {o : Ordinal} (ho : o.IsLimit) : ℵ_ o = ⨆ a : Iio o, ℵ_ a

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ ⨆ a, preAleph ↑a = ⨆ a, ℵ_ ↑a

Tactic:
apply le_antisymm <;>
  apply ciSup_mono' (bddAbove_of_small _) <;>
  intro i

Result:
case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio (ω + o))
⊢ ∃ i', preAleph ↑i ≤ ℵ_ ↑i'

case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio o)
⊢ ∃ i', ℵ_ ↑i ≤ preAleph ↑i'

Proof state:
case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio (ω + o))
⊢ ∃ i', preAleph ↑i ≤ ℵ_ ↑i'

Tactic:
refine ⟨⟨_, sub_lt_of_lt_add i.2 ho.pos⟩, ?_⟩

Result:
case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio (ω + o))
⊢ preAleph ↑i ≤ ℵ_ ↑⟨↑i - ω, ⋯⟩

Proof state:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ ℵ_ o = ⨆ a, ℵ_ ↑a

Tactic:
rw [aleph_eq_preAleph, preAleph_limit (isLimit_add ω ho)]

Result:
o : Ordinal.{u_1}
ho : o.IsLimit
⊢ ⨆ a, preAleph ↑a = ⨆ a, ℵ_ ↑a

Proof state:
case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio o)
⊢ ∃ i', ℵ_ ↑i ≤ preAleph ↑i'

Tactic:
exact ⟨⟨_, add_lt_add_left i.2 ω⟩, le_rfl⟩

Result:
no goals

Proof state:
case a
o : Ordinal.{u_1}
ho : o.IsLimit
i : ↑(Iio (ω + o))
⊢ preAleph ↑i ≤ ℵ_ ↑⟨↑i - ω, ⋯⟩

Tactic:
simpa [aleph_eq_preAleph] using le_add_sub _ _

Result:
no goals