harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem filter_append_perm (p : α → Bool) (l : List α) :
    filter p l ++ filter (fun x => !p x) l ~ l

Proof state:
case neg
α : Type u_1
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => !p x) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => !p x) l ~ x :: l

Tactic:
exact Perm.trans (perm_append_comm.trans (perm_append_comm.cons _)) (ih.cons x)

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Bool
⊢ filter p [] ++ filter (fun x => !p x) [] ~ []

Tactic:
rfl

Result:
no goals

Proof state:
case pos
α : Type u_1
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => !p x) l ~ l
h : p x = true
⊢ x :: (filter p l ++ filter (fun x => !p x) l) ~ x :: l

Tactic:
exact ih.cons x

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => !p x) l ~ l
⊢ filter p (x :: l) ++ filter (fun x => !p x) (x :: l) ~ x :: l

Tactic:
by_cases h : p x <;> simp [h]

Result:
case pos
α : Type u_1
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => !p x) l ~ l
h : p x = true
⊢ x :: (filter p l ++ filter (fun x => !p x) l) ~ x :: l

case neg
α : Type u_1
p : α → Bool
x : α
l : List α
ih : filter p l ++ filter (fun x => !p x) l ~ l
h : ¬p x = true
⊢ filter p l ++ x :: filter (fun x => !p x) l ~ x :: l
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_pi_div_two_iff {z : ℂ} : arg z = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ z.re = 0 ∧ 0 < z.im

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im

Proof state:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Tactic:
obtain ⟨x, y⟩ := z

Result:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → { re := x, im := y }.arg = π / 2

Proof state:
z : ℂ
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
by_cases h₀ : z = 0

Result:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).re = 0 ∧ 0 < (↑‖z‖ * (cos ↑(π / 2) + sin ↑(π / 2) * I)).im

Tactic:
simp [h₀]

Result:
no goals

Proof state:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ 0 < { re := x, im := y }.im → { re := x, im := y }.arg = π / 2

Tactic:
rintro ⟨rfl : x = 0, hy : 0 < y⟩

Result:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = π / 2

Proof state:
case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
constructor

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 → z.re = 0 ∧ 0 < z.im

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ 0 < z.im → z.arg = π / 2

Proof state:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : 0 < y
⊢ { re := 0, im := y }.arg = π / 2

Tactic:
rw [← arg_I, ← arg_real_mul I hy, ofReal_mul', I_re, I_im, mul_zero, mul_one]

Result:
no goals

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = π / 2 → z.re = 0 ∧ 0 < z.im

Tactic:
intro h

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = π / 2
⊢ z.re = 0 ∧ 0 < z.im

Proof state:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = π / 2 ↔ z.re = 0 ∧ 0 < z.im

Tactic:
simp [h₀, lt_irrefl, Real.pi_div_two_pos.ne]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem head_filter (p : α → Bool) (l : List α) (h) :
    (l.filter p).head h = (l.find? p).get (by simp_all [Option.isSome_iff_ne_none])

Proof state:
α : Type ?u.60002
p : α → Bool
l : List α
h : filter p l ≠ []
⊢ (find? p l).isSome = true

Tactic:
simp_all [Option.isSome_iff_ne_none]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : List α
h : filter p l ≠ []
⊢ (filter p l).head h = (find? p l).get ⋯

Tactic:
simp [head_eq_iff_head?_eq_some]

Result:
no goals
-- Mathlib/Order/Category/PartOrd.lean
lemma id_apply (X : PartOrd) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : PartOrd
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem adj_congr_of_sym2 {H : G.Subgraph} {u v w x : V} (h2 : s(u, v) = s(w, x)) :
    H.Adj u v ↔ H.Adj w x

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rcases h2 with hl | hr

Result:
case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj u v ↔ H.Adj w x

case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Proof state:
case inl
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hl : u = w ∧ v = x
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rw [hl.1, hl.2]

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : s(u, v) = s(w, x)
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h2

Result:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Proof state:
case inr
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
hr : u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
rw [hr.1, hr.2, Subgraph.adj_comm]

Result:
no goals
-- Mathlib/Order/Booleanisation.lean
@[simp] lemma comp_lt_comp : comp a < comp b ↔ b < a := ⟨by rintro ⟨_⟩; assumption, LT.comp⟩

Proof state:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b < a
⊢ b < a

Tactic:
assumption

Result:
no goals

Proof state:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
⊢ comp a < comp b → b < a

Tactic:
rintro ⟨_⟩

Result:
case comp
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
a b : α
a✝ : b < a
⊢ b < a
-- Mathlib/MeasureTheory/Integral/Periodic.lean
theorem isAddFundamentalDomain_Ioc' {T : ℝ} (hT : 0 < T) (t : ℝ) (μ : Measure ℝ

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Tactic:
refine (AddSubgroup.equivOp _).bijective.comp this |>.existsUnique_iff.2 ?_

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! x_1, (⇑(zmultiples T).equivOp ∘ codRestrict (fun n => n • T) ↑(zmultiples T) ⋯) x_1 +ᵥ x ∈ Ioc t (t + T)

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! x_1, (⇑(zmultiples T).equivOp ∘ codRestrict (fun n => n • T) ↑(zmultiples T) ⋯) x_1 +ᵥ x ∈ Ioc t (t + T)

Tactic:
simpa using existsUnique_add_zsmul_mem_Ioc hT x t

Result:
no goals

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Tactic:
have : Bijective (codRestrict (fun n : ℤ => n • T) (AddSubgroup.zmultiples T) _) :=
  (Equiv.ofInjective (fun n : ℤ => n • T) (zsmul_left_strictMono hT).injective).bijective

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
this : Bijective (codRestrict (fun n => n • T) ↑(zmultiples T) ⋯)
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)

Proof state:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
⊢ IsAddFundamentalDomain (↥(zmultiples T).op) (Ioc t (t + T)) μ

Tactic:
refine IsAddFundamentalDomain.mk' nullMeasurableSet_Ioc fun x => ?_

Result:
T : ℝ
hT : 0 < T
t : ℝ
μ : autoParam (Measure ℝ) _auto✝
x : ℝ
⊢ ∃! g, g +ᵥ x ∈ Ioc t (t + T)
-- Mathlib/Data/List/Chain.lean
theorem Chain'.infix (h : Chain' R l) (h' : l₁ <:+: l) : Chain' R l₁

Proof state:
α : Type u
R : α → α → Prop
l l₁ : List α
h : Chain' R l
h' : l₁ <:+: l
⊢ Chain' R l₁

Tactic:
rcases h' with ⟨l₂, l₃, rfl⟩

Result:
case intro.intro
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h : Chain' R (l₂ ++ l₁ ++ l₃)
⊢ Chain' R l₁

Proof state:
case intro.intro
α : Type u
R : α → α → Prop
l₁ l₂ l₃ : List α
h : Chain' R (l₂ ++ l₁ ++ l₃)
⊢ Chain' R l₁

Tactic:
exact h.left_of_append.right_of_append

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Dart.lean
theorem Dart.ext_iff (d₁ d₂ : G.Dart) : d₁ = d₂ ↔ d₁.toProd = d₂.toProd

Proof state:
V : Type u_1
G : SimpleGraph V
d₁ d₂ : G.Dart
⊢ d₁ = d₂ ↔ d₁.toProd = d₂.toProd

Tactic:
cases d₁

Result:
case mk
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝, adj := adj✝ } = d₂ ↔ { toProd := toProd✝, adj := adj✝ }.toProd = d₂.toProd

Proof state:
case mk.mk
V : Type u_1
G : SimpleGraph V
toProd✝¹ : V × V
adj✝¹ : G.Adj toProd✝¹.1 toProd✝¹.2
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝¹, adj := adj✝¹ } = { toProd := toProd✝, adj := adj✝ } ↔
    { toProd := toProd✝¹, adj := adj✝¹ }.toProd = { toProd := toProd✝, adj := adj✝ }.toProd

Tactic:
simp

Result:
no goals

Proof state:
case mk
V : Type u_1
G : SimpleGraph V
d₂ : G.Dart
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝, adj := adj✝ } = d₂ ↔ { toProd := toProd✝, adj := adj✝ }.toProd = d₂.toProd

Tactic:
cases d₂

Result:
case mk.mk
V : Type u_1
G : SimpleGraph V
toProd✝¹ : V × V
adj✝¹ : G.Adj toProd✝¹.1 toProd✝¹.2
toProd✝ : V × V
adj✝ : G.Adj toProd✝.1 toProd✝.2
⊢ { toProd := toProd✝¹, adj := adj✝¹ } = { toProd := toProd✝, adj := adj✝ } ↔
    { toProd := toProd✝¹, adj := adj✝¹ }.toProd = { toProd := toProd✝, adj := adj✝ }.toProd
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem closure_of_rat_image_lt {q : ℚ} :
    closure (((↑) : ℚ → ℝ) '' { x | q < x }) = { r | ↑q ≤ r } :=
  Subset.antisymm
    (isClosed_Ici.closure_subset_iff.2
      (image_subset_iff.2 fun p (h : q < p) => by simpa using h.le))
    fun x hx => mem_closure_iff_nhds.2 fun _ ht =>
      let ⟨ε, ε0, hε⟩ := Metric.mem_nhds_iff.1 ht
      let ⟨p, h₁, h₂⟩ := exists_rat_btwn ((lt_add_iff_pos_right x).2 ε0)
      ⟨p, hε <| by rwa [mem_ball, Real.dist_eq, abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add'],
        mem_image_of_mem _ <| Rat.cast_lt.1 <| lt_of_le_of_lt hx.out h₁⟩

Proof state:
q : ℚ
x : ℝ
hx : x ∈ {r | ↑q ≤ r}
x✝ : Set ℝ
ht : x✝ ∈ 𝓝 x
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ x✝
p : ℚ
h₁ : x < ↑p
h₂ : ↑p < x + ε
⊢ ↑p ∈ ball x ε

Tactic:
rwa [mem_ball, Real.dist_eq, abs_of_pos (sub_pos.2 h₁), sub_lt_iff_lt_add']

Result:
no goals

Proof state:
q p : ℚ
h : q < p
⊢ p ∈ Rat.cast ⁻¹' Ici ↑q

Tactic:
simpa using h.le

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Associated.prime [CommMonoidWithZero M] {p q : M} (h : p ~ᵤ q) (hp : Prime p) :
    Prime q :=
  ⟨h.ne_zero_iff.1 hp.ne_zero,
    let ⟨u, hu⟩ := h
    ⟨fun ⟨v, hv⟩ => hp.not_unit ⟨v * u⁻¹, by simp [hv, hu.symm]⟩,
      hu ▸ by
        simp only [IsUnit.mul_iff, Units.isUnit, and_true, IsUnit.mul_right_dvd]
        intro a b
        exact hp.dvd_or_dvd⟩⟩

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
a b : M
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
exact hp.dvd_or_dvd

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
x✝ : IsUnit q
v : Mˣ
hv : ↑v = q
⊢ ↑(v * u⁻¹) = p

Tactic:
simp [hv, hu.symm]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
intro a b

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
a b : M
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

Proof state:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p * ↑u ∣ a * b → p * ↑u ∣ a ∨ p * ↑u ∣ b

Tactic:
simp only [IsUnit.mul_iff, Units.isUnit, and_true, IsUnit.mul_right_dvd]

Result:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
⊢ ∀ (a b : M), p ∣ a * b → p ∣ a ∨ p ∣ b
-- Mathlib/CategoryTheory/Shift/Basic.lean
@[reassoc]
lemma assoc_inv_app (h : ShiftMkCore C A) (m₁ m₂ m₃ : A) (X : C) :
    (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫
      eqToHom (by rw [add_assoc])

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F m₃).map ((h.add m₁ m₂).inv.app X) ≫ (h.add (m₁ + m₂) m₃).inv.app X =
    (h.add m₂ m₃).inv.app ((h.F m₁).obj X) ≫ (h.add m₁ (m₂ + m₃)).inv.app X ≫ eqToHom ⋯

Tactic:
rw [← cancel_mono ((h.add (m₁ + m₂) m₃).hom.app X ≫ (h.F m₃).map ((h.add m₁ m₂).hom.app X)),
  Category.assoc, Category.assoc, Category.assoc, Iso.inv_hom_id_app_assoc, ← Functor.map_comp,
  Iso.inv_hom_id_app, Functor.map_id, h.assoc_hom_app, eqToHom_trans_assoc, eqToHom_refl,
  Category.id_comp, Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]

Result:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) = 𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X))

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ 𝟙 ((h.F m₃).obj ((h.F m₁ ⋙ h.F m₂).obj X)) = 𝟙 ((h.F m₂ ⋙ h.F m₃).obj ((h.F m₁).obj X))

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
A : Type u_1
inst✝¹ : Category.{v, u} C
inst✝ : AddMonoid A
h : ShiftMkCore C A
m₁ m₂ m₃ : A
X : C
⊢ (h.F (m₁ + (m₂ + m₃))).obj X = (h.F (m₁ + m₂ + m₃)).obj X

Tactic:
rw [add_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Norm.lean
theorem not_ite {_ : Decidable p} (q r : Prop) : (¬ite p q r) = ite p (¬q) (¬r)

Proof state:
p : Prop
x✝ : Decidable p
q r : Prop
⊢ (¬if p then q else r) = if p then ¬q else ¬r

Tactic:
by_cases p <;> simp [*]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem numberField [h : NumberField K] [Finite S] [IsCyclotomicExtension S K L] : NumberField L :=
  { to_charZero := charZero_of_injective_algebraMap (algebraMap K L).injective
    to_finiteDimensional

Proof state:
S : Set ℕ+
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this✝ : CharZero L
this : Module.Finite K L
⊢ FiniteDimensional ℚ L

Tactic:
exact Module.Finite.trans K _

Result:
no goals

Proof state:
S : Set ℕ+
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this : CharZero L
⊢ FiniteDimensional ℚ L

Tactic:
haveI := IsCyclotomicExtension.finite S K L

Result:
S : Set ℕ+
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this✝ : CharZero L
this : Module.Finite K L
⊢ FiniteDimensional ℚ L

Proof state:
S : Set ℕ+
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
⊢ FiniteDimensional ℚ L

Tactic:
haveI := charZero_of_injective_algebraMap (algebraMap K L).injective

Result:
S : Set ℕ+
K : Type w
L : Type z
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
h : NumberField K
inst✝¹ : Finite ↑S
inst✝ : IsCyclotomicExtension S K L
this : CharZero L
⊢ FiniteDimensional ℚ L
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_concat (f : α → β) (a : α) (l : List α) : map f (concat l a) = concat (map f l) (f a)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
a : α
l : List α
⊢ map f (l.concat a) = (map f l).concat (f a)

Tactic:
induction l with
| nil => rfl
| cons x xs ih => simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → β
a x : α
xs : List α
ih : map f (xs.concat a) = (map f xs).concat (f a)
⊢ map f ((x :: xs).concat a) = (map f (x :: xs)).concat (f a)

Tactic:
simp [ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f ([].concat a) = (map f []).concat (f a)

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma b₈_of_char_three :
    W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 =
    W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2

Tactic:
linear_combination W.a₂ * W.a₆ * CharP.cast_eq_zero R 3

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.b₈ = W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2

Tactic:
rw [b₈]

Result:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : CharP R 3
⊢ W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2 =
    W.a₁ ^ 2 * W.a₆ + W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_or_distrib_left : a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c

Proof state:
a b c : Prop
⊢ a ∨ b ∨ c ↔ (a ∨ b) ∨ a ∨ c

Tactic:
rw [or_or_or_comm, or_self]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma exists_pow_mem_of_relindex_ne_zero (h : H.relindex K ≠ 0) {a : G} (ha : a ∈ K) :
    ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K

Tactic:
refine ⟨n, hlt, hle, ?_⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Proof state:
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
⊢ ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K

Tactic:
rcases exists_pow_mem_of_index_ne_zero h ⟨a, ha⟩ with ⟨n, hlt, hle, he⟩

Result:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ ∃ n, 0 < n ∧ n ≤ H.relindex K ∧ a ^ n ∈ H ⊓ K

Proof state:
case intro.intro.intro
G : Type u_1
inst✝ : Group G
H K : Subgroup G
h : H.relindex K ≠ 0
a : G
ha : a ∈ K
n : ℕ
hlt : 0 < n
hle : n ≤ (H.subgroupOf K).index
he : ⟨a, ha⟩ ^ n ∈ H.subgroupOf K
⊢ a ^ n ∈ H ⊓ K

Tactic:
simpa [pow_mem ha, mem_subgroupOf] using he

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem hasFTaylorSeriesUpToOn_pi {n : WithTop ℕ∞} :
    HasFTaylorSeriesUpToOn n (fun x i => φ i x)
        (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s ↔
      ∀ i, HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Proof state:
case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
⊢ ∀ (m : ℕ),
    ↑m < n →
      ∀ x ∈ s,
        HasFDerivWithinAt (fun x => ContinuousMultilinearMap.pi fun i => p' i x m)
          (ContinuousMultilinearMap.pi fun i => p' i x m.succ).curryLeft s x

Tactic:
intro m hm x hx

Result:
case refine_3
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : ∀ (i : ι), HasFTaylorSeriesUpToOn n (φ i) (p' i) s
m : ℕ
hm : ↑m < n
x : E
hx : x ∈ s
⊢ HasFDerivWithinAt (fun x => ContinuousMultilinearMap.pi fun i => p' i x m)
    (ContinuousMultilinearMap.pi fun i => p' i x m.succ).curryLeft s x

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
s : Set E
ι : Type u_3
inst✝² : Fintype ι
F' : ι → Type u_5
inst✝¹ : (i : ι) → NormedAddCommGroup (F' i)
inst✝ : (i : ι) → NormedSpace 𝕜 (F' i)
φ : (i : ι) → E → F' i
p' : (i : ι) → E → FormalMultilinearSeries 𝕜 E (F' i)
n : WithTop ℕ∞
pr : (i : ι) → ((i : ι) → F' i) →L[𝕜] F' i := ContinuousLinearMap.proj
L : (m : ℕ) →
  ((i : ι) → ContinuousMultilinearMap 𝕜 (fun i => E) (F' i)) ≃ₗᵢ[𝕜]
    ContinuousMultilinearMap 𝕜 (fun i => E) ((i : ι) → F' i) :=
  fun m => ContinuousMultilinearMap.piₗᵢ 𝕜 fun i => E
h : HasFTaylorSeriesUpToOn n (fun x i => φ i x) (fun x m => ContinuousMultilinearMap.pi fun i => p' i x m) s
i : ι
⊢ HasFTaylorSeriesUpToOn n (φ i) (p' i) s

Tactic:
exact h.continuousLinearMap_comp (pr i)

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleOf_pow_apply_self (f : Perm α) [DecidableRel f.SameCycle] (x : α) :
    ∀ n : ℕ, (cycleOf f x ^ n) x = (f ^ n) x

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ ∀ (n : ℕ), (f.cycleOf x ^ n) x = (f ^ n) x

Tactic:
intro n

Result:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
⊢ (f.cycleOf x ^ n) x = (f ^ n) x

Proof state:
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
⊢ (f.cycleOf x ^ n) x = (f ^ n) x

Tactic:
induction n with
| zero => rfl
| succ n hn =>
  rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]
  exact ⟨n, rfl⟩

Result:
no goals

Proof state:
case zero
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
⊢ (f.cycleOf x ^ 0) x = (f ^ 0) x

Tactic:
rfl

Result:
no goals

Proof state:
case succ
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ (f.cycleOf x ^ (n + 1)) x = (f ^ (n + 1)) x

Tactic:
rw [pow_succ', mul_apply, cycleOf_apply, hn, if_pos, pow_succ', mul_apply]

Result:
case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)

Proof state:
case succ.hc
α : Type u_2
f : Perm α
inst✝ : DecidableRel f.SameCycle
x : α
n : ℕ
hn : (f.cycleOf x ^ n) x = (f ^ n) x
⊢ f.SameCycle x ((f ^ n) x)

Tactic:
exact ⟨n, rfl⟩

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_add {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

Proof state:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal (p + q) = ENNReal.ofReal p + ENNReal.ofReal q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, ENNReal.ofReal, ← coe_add, coe_inj,
  Real.toNNReal_add hp hq]

Result:
no goals