harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem _root_.IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul_field {K : Type*}
    [Field K] {ζ : K} (x y : K) (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
    x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

Proof state:
case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n = x ^ #(nthRootsFinset n K)

Tactic:
congr

Result:
case pos.e_a
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ n = #(nthRootsFinset n K)

Proof state:
case h.e'_2
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = eval (x / y) (X ^ n - 1) * y ^ #(nthRootsFinset n K)

Tactic:
simp [sub_mul, div_pow, hy, h.card_nthRootsFinset]

Result:
no goals

Proof state:
case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

Tactic:
simp only [hy, zero_pow (Nat.not_eq_zero_of_lt hpos), sub_zero, mul_zero, prod_const]

Result:
case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n = x ^ #(nthRootsFinset n K)

Proof state:
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

Tactic:
by_cases hy : y = 0

Result:
case pos
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

case neg
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y)

Proof state:
case pos.e_a
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : y = 0
⊢ n = #(nthRootsFinset n K)

Tactic:
rw [h.card_nthRootsFinset]

Result:
no goals

Proof state:
case h.e'_3
n : ℕ
K : Type u_2
inst✝ : Field K
ζ x y : K
hpos : 0 < n
h : IsPrimitiveRoot ζ n
hy : ¬y = 0
⊢ ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y) = eval (x / y) (∏ ζ ∈ nthRootsFinset n K, (X - C ζ)) * y ^ #(nthRootsFinset n K)

Tactic:
simp [eval_prod, prod_mul_pow_card, sub_mul, hy]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_of_splits_id {f : K[X]} : Splits (RingHom.id K) f → Splits i f :=
  UniqueFactorizationMonoid.induction_on_prime f (fun _ => splits_zero _)
    (fun _ hu _ => splits_of_degree_le_one _ ((isUnit_iff_degree_eq_zero.1 hu).symm ▸ by decide))
    fun _ p ha0 hp ih hfi =>
    splits_mul _
      (splits_of_degree_eq_one _
        ((splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).1.def.resolve_left hp.1 hp.irreducible
          (by rw [map_id])))
      (ih (splits_of_splits_mul _ (mul_ne_zero hp.1 ha0) hfi).2)

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f x✝¹ : K[X]
hu : IsUnit x✝¹
x✝ : Splits (RingHom.id K) x✝¹
⊢ 0 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
K : Type v
L : Type w
inst✝¹ : Field K
inst✝ : Field L
i : K →+* L
f x✝ p : K[X]
ha0 : x✝ ≠ 0
hp : Prime p
ih : Splits (RingHom.id K) x✝ → Splits i x✝
hfi : Splits (RingHom.id K) (p * x✝)
⊢ p ∣ map (RingHom.id K) p

Tactic:
rw [map_id]

Result:
no goals
-- Mathlib/Order/Disjointed.lean
lemma disjointed_eq_self {f : ι → α} {i : ι} (hf : ∀ j < i, Disjoint (f j) (f i)) :
    disjointed f i = f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ disjointed f i = f i

Tactic:
rw [disjointed_apply, sdiff_eq_left, disjoint_iff, sup_inf_distrib_left,
  sup_congr rfl <| fun j hj ↦ disjoint_iff.mp <| (hf _ (mem_Iio.mp hj)).symm]

Result:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j => ⊥) = ⊥

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : Preorder ι
inst✝ : LocallyFiniteOrderBot ι
f : ι → α
i : ι
hf : ∀ j < i, Disjoint (f j) (f i)
⊢ ((Iio i).sup fun j => ⊥) = ⊥

Tactic:
exact sup_bot _

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma shift_smul (a : ℤ) (x : R) :
    (x • γ).shift a = x • (γ.shift a)

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq

Tactic:
simp only [shift_v', smul_v]

Result:
no goals

Proof state:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = x • (γ.shift a).v p q hpq

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
⊢ (x • γ).shift a = x • γ.shift a

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n : ℤ
γ : Cochain K L n
a : ℤ
x : R
p q : ℤ
hpq : p + n = q
⊢ ((x • γ).shift a).v p q hpq = (x • γ.shift a).v p q hpq
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma map_δ :
    (G.mapHomologicalComplex (ComplexShape.up ℤ)).map (triangle φ).mor₃ ≫
      NatTrans.app ((Functor.mapHomologicalComplex G (ComplexShape.up ℤ)).commShiftIso  1).hom K =
    (mapHomologicalComplexIso φ G).hom ≫
      (triangle ((G.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).mor₃

Proof state:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map ((triangle φ).mor₃.f n) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)

Tactic:
dsimp [triangle]

Result:
case h
C : Type u_1
D : Type u_2
inst✝⁶ : Category.{u_4, u_1} C
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive C
inst✝³ : HasBinaryBiproducts C
inst✝² : Preadditive D
inst✝¹ : HasBinaryBiproducts D
K L : CochainComplex C ℤ
φ : K ⟶ L
G : C ⥤ D
inst✝ : G.Additive
n : ℤ
⊢ G.map (((-↑(fst φ)).rightShift 1 0 triangle.proof_3).v n n ⋯) = -G.map ((↑(fst φ)).v n (n + 1) ⋯)
-- Mathlib/Data/Nat/WithBot.lean
theorem add_eq_zero_iff {n m : WithBot ℕ} : n + m = 0 ↔ n = 0 ∧ m = 0

Proof state:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ ⊥ = 0 ∧ m = 0

Tactic:
simp [WithBot.bot_add]

Result:
no goals

Proof state:
n m : WithBot ℕ
⊢ n + m = 0 ↔ n = 0 ∧ m = 0

Tactic:
cases n

Result:
case bot
m : WithBot ℕ
⊢ ⊥ + m = 0 ↔ ⊥ = 0 ∧ m = 0

case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0

Proof state:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

Tactic:
simp [WithBot.add_bot]

Result:
no goals

Proof state:
case coe
m : WithBot ℕ
a✝ : ℕ
⊢ ↑a✝ + m = 0 ↔ ↑a✝ = 0 ∧ m = 0

Tactic:
cases m

Result:
case coe.bot
a✝ : ℕ
⊢ ↑a✝ + ⊥ = 0 ↔ ↑a✝ = 0 ∧ ⊥ = 0

case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0

Proof state:
case coe.coe
a✝¹ a✝ : ℕ
⊢ ↑a✝¹ + ↑a✝ = 0 ↔ ↑a✝¹ = 0 ∧ ↑a✝ = 0

Tactic:
simp [← WithBot.coe_add, add_eq_zero_iff_of_nonneg]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem sizeof_of_step : ∀ {L₁ L₂ : List (α × Bool)},
    Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
  | _, _, @Step.not _ L1 L2 x b => by
    induction L1 with
    | nil =>
      dsimp
      omega
    | cons hd tl ih =>
      dsimp
      exact Nat.add_lt_add_left ih _

Proof state:
case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
exact Nat.add_lt_add_left ih _

Result:
no goals

Proof state:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf ([] ++ L2) < sizeOf ([] ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp

Result:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)

Proof state:
case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ sizeOf (hd :: tl ++ L2) < sizeOf (hd :: tl ++ (x, b) :: (x, !b) :: L2)

Tactic:
dsimp

Result:
case cons
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
hd : α × Bool
tl : List (α × Bool)
ih : sizeOf (tl ++ L2) < sizeOf (tl ++ (x, b) :: (x, !b) :: L2)
⊢ 1 + sizeOf hd + sizeOf (tl ++ L2) < 1 + sizeOf hd + sizeOf (tl ++ (x, b) :: (x, !b) :: L2)

Proof state:
case nil
α : Type u
L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf L2 < 1 + (1 + sizeOf b) + (1 + (1 + sizeOf !b) + sizeOf L2)

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ sizeOf (L1 ++ L2) < sizeOf (L1 ++ (x, b) :: (x, !b) :: L2)

Tactic:
induction L1 with
| nil =>
  dsimp
  omega
| cons hd tl ih =>
  dsimp
  exact Nat.add_lt_add_left ih _

Result:
no goals
-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
lemma ContinuousMultilinearMap.iteratedFDeriv_comp_diagonal
    {n : ℕ} (f : E [×n]→L[𝕜] F) (x : E) (v : Fin n → E) :
    iteratedFDeriv 𝕜 n (fun x ↦ f (fun _ ↦ x)) x v = ∑ σ : Perm (Fin n), f (fun i ↦ v (σ i))

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

Tactic:
let g : E →L[𝕜] (Fin n → E) := ContinuousLinearMap.pi (fun i ↦ ContinuousLinearMap.id 𝕜 E)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
g : E →L[𝕜] Fin n → E := ContinuousLinearMap.pi fun i => ContinuousLinearMap.id 𝕜 E
⊢ (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v = ∑ σ : Perm (Fin n), f fun i => v (σ i)

Tactic:
rw [← sum_comp (Equiv.inv (Perm (Fin n)))]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : ContinuousMultilinearMap 𝕜 (fun i => E) F
x : E
v : Fin n → E
⊢ (iteratedFDeriv 𝕜 n (fun x => f fun x_1 => x) x) v =
    ∑ i : Perm (Fin n), f fun i_1 => v (((Equiv.inv (Perm (Fin n))) i) i_1)
-- Mathlib/Data/Finite/Prod.lean
theorem infinite_prod :
    (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False

Tactic:
exact h ((this.1 h.nonempty.snd).prod <| this.2 h.nonempty.fst)

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Tactic:
rintro (h | h)

Result:
case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ (s ×ˢ t).Infinite ↔ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
refine ⟨fun h => ?_, ?_⟩

Result:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

case refine_2
α : Type u_1
β : Type u_2
s : Set α
t : Set β
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty → (s ×ˢ t).Infinite

Proof state:
case refine_2.inl
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : s.Infinite ∧ t.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.1.prod_left h.2

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)

Tactic:
by_contra!

Result:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
this : (t.Nonempty → s.Finite) ∧ (s.Nonempty → t.Finite)
⊢ False

Proof state:
case refine_2.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : t.Infinite ∧ s.Nonempty
⊢ (s ×ˢ t).Infinite

Tactic:
exact h.1.prod_right h.2

Result:
no goals

Proof state:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ s.Infinite ∧ t.Nonempty ∨ t.Infinite ∧ s.Nonempty

Tactic:
simp_rw [Set.Infinite, @and_comm ¬_, ← Classical.not_imp]

Result:
case refine_1
α : Type u_1
β : Type u_2
s : Set α
t : Set β
h : (s ×ˢ t).Infinite
⊢ ¬(t.Nonempty → s.Finite) ∨ ¬(s.Nonempty → t.Finite)
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Basic.lean
theorem sections_eq_nil_of_isEmpty : ∀ {L}, L.any isEmpty → @sections α L = []
  | l :: L, h => by
    simp only [any, foldr, Bool.or_eq_true] at h
    match l, h with
    | [], .inl rfl => simp
    | l, .inr h => simp [sections, sections_eq_nil_of_isEmpty h]

Proof state:
α : Type u_1
l✝ : List α
L : List (List α)
h✝ : l✝.isEmpty = true ∨ L.any isEmpty = true
l : List α
h : L.any isEmpty = true
⊢ (l :: L).sections = []

Tactic:
simp [sections, sections_eq_nil_of_isEmpty h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
L : List (List α)
h : l.isEmpty = true ∨ L.any isEmpty = true
⊢ ([] :: L).sections = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
L : List (List α)
h : l.isEmpty = true ∨ L.any isEmpty = true
⊢ (l :: L).sections = []

Tactic:
match l, h with
| [], .inl rfl => simp
| l, .inr h => simp [sections, sections_eq_nil_of_isEmpty h]

Result:
no goals

Proof state:
α : Type u_1
l : List α
L : List (List α)
h : (l :: L).any isEmpty = true
⊢ (l :: L).sections = []

Tactic:
simp only [any, foldr, Bool.or_eq_true] at h

Result:
α : Type u_1
l : List α
L : List (List α)
h : l.isEmpty = true ∨ L.any isEmpty = true
⊢ (l :: L).sections = []
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem rat_dense' (q : ℚ_[p]) {ε : ℚ} (hε : 0 < ε) : ∃ r : ℚ, padicNormE (q - r : ℚ_[p]) < ε :=
  Quotient.inductionOn q fun q' ↦
    have : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (q' m - q' n) < ε := cauchy₂ _ hε
    let ⟨N, hN⟩ := this
    ⟨q' N, by
      classical
      dsimp [padicNormE]
      -- Porting note: `change` → `convert_to` (`change` times out!)
      -- and add `PadicSeq p` type annotation
      convert_to PadicSeq.norm (q' - const _ (q' N) : PadicSeq p) < ε
      rcases Decidable.em (q' - const (padicNorm p) (q' N) ≈ 0) with heq | hne'
      · simpa only [heq, PadicSeq.norm, dif_pos]
      · simp only [PadicSeq.norm, dif_neg hne']
        change padicNorm p (q' _ - q' _) < ε
        rcases Decidable.em (stationaryPoint hne' ≤ N) with hle | hle
        · -- Porting note: inlined `stationaryPoint_spec` invocation.
          have := (stationaryPoint_spec hne' le_rfl hle).symm
          simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this
          simpa only [this]
        · exact hN _ (lt_of_not_ge hle).le _ le_rfl⟩

Proof state:
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this :
  padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) (stationaryPoint hne')) =
    padicNorm p (↑(q' - const (padicNorm p) (↑q' N)) N)
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

Tactic:
simp only [const_apply, sub_apply, padicNorm.zero, sub_self] at this

Result:
case inr.inl
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this✝ : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
hne' : ¬q' - const (padicNorm p) (↑q' N) ≈ 0
hle : stationaryPoint hne' ≤ N
this : padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) = 0
⊢ padicNorm p (↑q' (stationaryPoint hne') - ↑q' N) < ε

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ padicNormE (⟦q'⟧ - ↑(↑q' N)) < ε

Tactic:
dsimp [padicNormE]

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
q : ℚ_[p]
ε : ℚ
hε : 0 < ε
q' : CauSeq ℚ (padicNorm p)
this : ∃ N, ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
N : ℕ
hN : ∀ m ≥ N, ∀ n ≥ N, padicNorm p (↑q' m - ↑q' n) < ε
⊢ Quotient.lift PadicSeq.norm ⋯ (Completion.mk q' - ↑(↑q' N)) < ε
-- Mathlib/Combinatorics/SetFamily/Compression/Down.lean
theorem mem_compression : s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝓓 a 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s ∉ 𝒜 ∧ insert a s ∈ 𝒜

Tactic:
simp_rw [compression, mem_disjUnion, mem_filter, mem_image, and_comm (a := (¬ s ∈ 𝒜))]

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜

Proof state:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : t.erase a ∉ 𝒜
⊢ insert a (t.erase a) ∈ 𝒜

Tactic:
rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem ht hs).symm)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
⊢ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ (∃ a_1 ∈ 𝒜, a_1.erase a = s) ∧ s ∉ 𝒜 ↔ s ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ insert a s ∈ 𝒜 ∧ s ∉ 𝒜

Tactic:
refine
  or_congr_right
    (and_congr_left fun hs =>
      ⟨?_, fun h => ⟨_, h, erase_insert <| insert_ne_self.1 <| ne_of_mem_of_not_mem h hs⟩⟩)

Result:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∉ 𝒜
⊢ (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜

Proof state:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∉ 𝒜
⊢ (∃ a_1 ∈ 𝒜, a_1.erase a = s) → insert a s ∈ 𝒜

Tactic:
rintro ⟨t, ht, rfl⟩

Result:
case intro.intro
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
t : Finset α
ht : t ∈ 𝒜
hs : t.erase a ∉ 𝒜
⊢ insert a (t.erase a) ∈ 𝒜
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma cast_card [Finite α] : (Nat.card α : Cardinal) = Cardinal.mk α

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ #α < ℵ₀

Tactic:
exact Cardinal.lt_aleph0_of_finite _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Finite α
⊢ ↑(Nat.card α) = #α

Tactic:
rw [Nat.card, Cardinal.cast_toNat_of_lt_aleph0]

Result:
α : Type u_1
inst✝ : Finite α
⊢ #α < ℵ₀
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycle.pow_eq_pow_iff [Finite β] {f : Perm β} (hf : IsCycle f) {a b : ℕ} :
    f ^ a = f ^ b ↔ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Proof state:
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
by_cases hfa : (f ^ a) x ∈ f.support

Result:
case pos
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∈ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : (f ^ a) x ∉ f.support
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Proof state:
case neg
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
val✝ : Fintype β
x : β
hx : f x ≠ x
a b : ℕ
hx' : (f ^ a) x = (f ^ b) x
hab : a ≤ b
hfa : f x = x
h : f ((f ^ a) x) = (f ^ a) (f x)
⊢ ∃ x, f x ≠ x ∧ (f ^ (b - a)) x = x

Tactic:
contradiction

Result:
no goals

Proof state:
case intro.mp.intro.intro
β : Type u_3
inst✝ : Finite β
f : Perm β
hf : f.IsCycle
a b : ℕ
val✝ : Fintype β
h : f ^ a = f ^ b
x : β
hx : f x ≠ x
⊢ ∃ x, f x ≠ x ∧ (f ^ a) x = (f ^ b) x

Tactic:
exact ⟨x, hx, by simp [h]⟩

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Polynomial.lean
theorem adjoin_X : Algebra.adjoin R ({X} : Set R[X]) = ⊤

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (p.sum fun n a => (monomial n) a) ∈ S

Tactic:
simp only [← smul_X_eq_monomial, Sum]

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (p.sum fun n a => a • X ^ n) ∈ S

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ Algebra.adjoin R {X} = ⊤

Tactic:
refine top_unique fun p _hp => ?_

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ Algebra.adjoin R {X}

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (p.sum fun n a => a • X ^ n) ∈ S

Tactic:
exact S.sum_mem fun n _hn => S.smul_mem (S.pow_mem (Algebra.subset_adjoin rfl) _) _

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
⊢ p ∈ Algebra.adjoin R {X}

Tactic:
set S := Algebra.adjoin R ({X} : Set R[X])

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ p ∈ S

Proof state:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ p ∈ S

Tactic:
rw [← sum_monomial_eq p]

Result:
R : Type u
inst✝ : CommSemiring R
p : R[X]
_hp : p ∈ ⊤
S : Subalgebra R R[X] := Algebra.adjoin R {X}
⊢ (p.sum fun n a => (monomial n) a) ∈ S