harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem not_int_of_not_padic_int (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)]
    (H : 1 < padicNorm p a) : ¬ a.isInt

Proof state:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p a ≤ 1

Tactic:
rw [Rat.eq_num_of_isInt H]

Result:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p ↑a.num ≤ 1

Proof state:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : 1 < padicNorm p a
⊢ ¬a.isInt = true

Tactic:
contrapose! H

Result:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p a ≤ 1

Proof state:
p : ℕ
a : ℚ
hp : Fact (Nat.Prime p)
H : a.isInt = true
⊢ padicNorm p ↑a.num ≤ 1

Tactic:
apply padicNorm.of_int

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem triangle_assoc_comp_right (X Y : C) :
    (α_ X (𝟙_ C) Y).inv ≫ ((ρ_ X).hom ▷ Y) = X ◁ (λ_ Y).hom

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y : C
⊢ (α_ X (𝟙_ C) Y).inv ≫ (ρ_ X).hom ▷ Y = X ◁ (λ_ Y).hom

Tactic:
rw [← triangle, Iso.inv_hom_id_assoc]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_eq_top {φ : R⟦X⟧} : φ.order = ⊤ ↔ φ = 0

Proof state:
R : Type u_1
inst✝ : Semiring R
φ : R⟦X⟧
⊢ φ.order = ⊤ ↔ φ = 0

Tactic:
simpa using order_finite_iff_ne_zero.not_left

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem card_center_eq_prime_pow (hGpn : Nat.card G = p ^ n) (hn : 0 < n) :
    ∃ k > 0, Nat.card (center G) = p ^ k

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
have hcG := to_subgroup (of_card hGpn) (center G)

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup p ↥(center G)
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup p ↥(center G)
x✝ : ∃ n, Nat.card ↥(center G) = p ^ n
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
haveI : Nontrivial G := (nontrivial_iff_card <| of_card hGpn).2 ⟨n, hn, hGpn⟩

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this✝ : Finite G
hcG : IsPGroup p ↥(center G)
x✝ : ∃ n, Nat.card ↥(center G) = p ^ n
this : Nontrivial G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this✝ : Finite G
hcG : IsPGroup p ↥(center G)
x✝ : ∃ n, Nat.card ↥(center G) = p ^ n
this : Nontrivial G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
exact (nontrivial_iff_card hcG).mp (center_nontrivial (of_card hGpn))

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
have : Finite G := Nat.finite_of_card_ne_zero (hGpn ▸ pow_ne_zero n (NeZero.ne p))

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup p ↥(center G)
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k

Tactic:
rcases iff_card.1 hcG with _

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
inst✝ : Fact (Nat.Prime p)
n : ℕ
hGpn : Nat.card G = p ^ n
hn : 0 < n
this : Finite G
hcG : IsPGroup p ↥(center G)
x✝ : ∃ n, Nat.card ↥(center G) = p ^ n
⊢ ∃ k > 0, Nat.card ↥(center G) = p ^ k
-- Mathlib/Data/Rat/Cast/Lemmas.lean
theorem cast_zpow_of_ne_zero {K} [DivisionSemiring K] (q : ℚ≥0) (z : ℤ) (hq : (q.num : K) ≠ 0) :
    NNRat.cast (q ^ z) = (NNRat.cast q : K) ^ z

Proof state:
case intro.inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ = (↑q)⁻¹

Tactic:
rw [cast_inv_of_ne_zero hq]

Result:
no goals

Proof state:
case intro.inl
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ ↑n) = ↑q ^ ↑n

Tactic:
simp

Result:
no goals

Proof state:
case intro.inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)

Tactic:
simp_rw [zpow_neg, zpow_natCast, ← inv_pow, NNRat.cast_pow]

Result:
case intro.inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ ^ n = (↑q)⁻¹ ^ n

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
z : ℤ
hq : ↑q.num ≠ 0
⊢ ↑(q ^ z) = ↑q ^ z

Tactic:
obtain ⟨n, rfl | rfl⟩ := z.eq_nat_or_neg

Result:
case intro.inl
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ ↑n) = ↑q ^ ↑n

case intro.inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑(q ^ (-↑n)) = ↑q ^ (-↑n)

Proof state:
case intro.inr
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ ^ n = (↑q)⁻¹ ^ n

Tactic:
congr

Result:
case intro.inr.e_a
K : Type u_1
inst✝ : DivisionSemiring K
q : ℚ≥0
hq : ↑q.num ≠ 0
n : ℕ
⊢ ↑q⁻¹ = (↑q)⁻¹
-- Mathlib/Data/List/Basic.lean
theorem _root_.Function.Involutive.exists_mem_and_apply_eq_iff {f : α → α}
    (hf : Function.Involutive f) (x : α) (l : List α) : (∃ y : α, y ∈ l ∧ f y = x) ↔ f x ∈ l :=
  ⟨by rintro ⟨y, h, rfl⟩; rwa [hf y], fun h => ⟨f x, h, hf _⟩⟩

Proof state:
case intro.intro
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l

Tactic:
rwa [hf y]

Result:
no goals

Proof state:
α : Type u
f : α → α
hf : Involutive f
x : α
l : List α
⊢ (∃ y, y ∈ l ∧ f y = x) → f x ∈ l

Tactic:
rintro ⟨y, h, rfl⟩

Result:
case intro.intro
α : Type u
f : α → α
hf : Involutive f
l : List α
y : α
h : y ∈ l
⊢ f (f y) ∈ l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem head_filterMap (f : α → Option β) (l : List α) (h) :
    (l.filterMap f).head h = (l.findSome? f).get (by simp_all [Option.isSome_iff_ne_none])

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
l : List α
h : filterMap f l ≠ []
⊢ (filterMap f l).head h = (findSome? f l).get ⋯

Tactic:
simp [head_eq_iff_head?_eq_some]

Result:
no goals

Proof state:
α : Type ?u.20339
β : Type ?u.20336
f : α → Option β
l : List α
h : filterMap f l ≠ []
⊢ (findSome? f l).isSome = true

Tactic:
simp_all [Option.isSome_iff_ne_none]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem add : @Primrec' 2 fun v => v.head + v.tail.head :=
  (prec head (succ.comp₁ _ (tail head))).of_eq fun v => by
    simp; induction v.head <;> simp [*, Nat.succ_add]

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => IH + 1) v.head = v.head + v.tail.head

Tactic:
induction v.head <;> simp [*, Nat.succ_add]

Result:
no goals

Proof state:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => (y ::ᵥ IH ::ᵥ v.tail).tail.head.succ) v.head = v.head + v.tail.head

Tactic:
simp

Result:
v : List.Vector ℕ (Nat.succ 0 + 1)
⊢ Nat.rec v.tail.head (fun y IH => IH + 1) v.head = v.head + v.tail.head
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_erase [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β} {a : α}
    (h : Raw.WFImp m.1) : Raw.WFImp (m.erase a).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.eraseₘ a).val

Tactic:
exact wfImp_eraseₘ h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.erase a).val

Tactic:
rw [erase_eq_eraseₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
a : α
h : Raw.WFImp m.val
⊢ Raw.WFImp (m.eraseₘ a).val
-- Mathlib/Probability/Process/Stopping.lean
theorem measurableSet_ge_of_countable_range {ι} [LinearOrder ι] {τ : Ω → ι}
    {f : Filtration ι m} (hτ : IsStoppingTime f τ) (h_countable : (Set.range τ).Countable) (i : ι) :
    MeasurableSet[f i] {ω | i ≤ τ ω}

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω < i}ᶜ

Tactic:
simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
rw [this]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | τ ω < i}ᶜ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | i ≤ τ ω}

Tactic:
have : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ := by
  ext1 ω; simp only [Set.mem_setOf_eq, Set.mem_compl_iff, not_lt]

Result:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | i ≤ τ ω}

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
this : {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ
⊢ MeasurableSet {ω | τ ω < i}ᶜ

Tactic:
exact (hτ.measurableSet_lt_of_countable_range h_countable i).compl

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ {ω | i ≤ τ ω} = {ω | τ ω < i}ᶜ

Tactic:
ext1 ω

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
ι : Type u_4
inst✝ : LinearOrder ι
τ : Ω → ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
ω : Ω
⊢ ω ∈ {ω | i ≤ τ ω} ↔ ω ∈ {ω | τ ω < i}ᶜ
-- Mathlib/Algebra/Polynomial/Eval/Degree.lean
theorem eval₂_eq_sum_range' (f : R →+* S) {p : R[X]} {n : ℕ} (hn : p.natDegree < n) (x : S) :
    eval₂ f x p = ∑ i ∈ Finset.range n, f (p.coeff i) * x ^ i

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ eval₂ f x p = ∑ i ∈ range n, f (p.coeff i) * x ^ i

Tactic:
rw [eval₂_eq_sum, p.sum_over_range' _ _ hn]

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∀ (n : ℕ), f 0 * x ^ n = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
⊢ ∀ (n : ℕ), f 0 * x ^ n = 0

Tactic:
intro i

Result:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
i : ℕ
⊢ f 0 * x ^ i = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
n : ℕ
hn : p.natDegree < n
x : S
i : ℕ
⊢ f 0 * x ^ i = 0

Tactic:
rw [f.map_zero, zero_mul]

Result:
no goals
-- Mathlib/Topology/Connected/Clopen.lean
theorem isPreconnected_iff_subset_of_disjoint {s : Set α} :
    IsPreconnected s ↔
      ∀ u v, IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v

Proof state:
case mp.intro.intro.intro.intro.intro
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
h : (s ∩ u).Nonempty → (s ∩ v).Nonempty → (s ∩ (u ∩ v)).Nonempty
x : α
hxs : x ∈ s
hxu : x ∉ u
y : α
hys : y ∈ s
hyv : y ∉ v
hxv : x ∈ v
hyu : y ∈ u
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
exact h ⟨y, hys, hyu⟩ ⟨x, hxs, hxv⟩

Result:
no goals

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
⊢ (s ∩ (u ∩ v)).Nonempty

Tactic:
by_contra H

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Proof state:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s : Set α
h : ∀ (u v : Set α), IsOpen u → IsOpen v → s ⊆ u ∪ v → s ∩ (u ∩ v) = ∅ → s ⊆ u ∨ s ⊆ v
u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
⊢ False

Tactic:
specialize h u v hu hv hs (Set.not_nonempty_iff_eq_empty.mp H)

Result:
case mpr
α : Type u
inst✝ : TopologicalSpace α
s u v : Set α
hu : IsOpen u
hv : IsOpen v
hs : s ⊆ u ∪ v
hsu : (s ∩ u).Nonempty
hsv : (s ∩ v).Nonempty
H : ¬(s ∩ (u ∩ v)).Nonempty
h : s ⊆ u ∨ s ⊆ v
⊢ False
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem truncateFun_add (x y : 𝕎 R) :
    truncateFun n (x + y) = truncateFun n x + truncateFun n y

Proof state:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ truncateFun n (x + y) = truncateFun n x + truncateFun n y

Tactic:
witt_truncateFun_tac

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem splitting_field_cyclotomic : IsSplittingField K L (cyclotomic n K) :=
  { splits' := splits_cyclotomic K L (mem_singleton n)
    adjoin_rootSet'

Proof state:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
letI := Classical.decEq L

Result:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
obtain ⟨ζ : L, hζ⟩ := IsCyclotomicExtension.exists_prim_root K (B := L) (mem_singleton n)

Result:
case intro
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = ⊤

Tactic:
rw [← ((iff_adjoin_eq_top {n} K L).1 inferInstance).2]

Result:
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Proof state:
case intro
n : ℕ+
K : Type w
L : Type z
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
this : DecidableEq L := Classical.decEq L
ζ : L
hζ : IsPrimitiveRoot ζ ↑n
⊢ adjoin K ((cyclotomic (↑n) K).rootSet L) = adjoin K {b | ∃ n_1 ∈ {n}, b ^ ↑n_1 = 1}

Tactic:
exact adjoin_roots_cyclotomic_eq_adjoin_nth_roots hζ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findFinIdx?_subtype {p : α → Prop} {l : List { x // p x }}
    {f : { x // p x } → Bool} {g : α → Bool} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    l.findFinIdx? f = (l.unattach.findFinIdx? g).map (fun i => i.cast (by simp))

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) l))

Tactic:
induction l with
| nil => simp
| cons a l ih =>
  simp [hf, findFinIdx?_cons]
  split <;> simp [ih, Function.comp_def]

Result:
no goals

Proof state:
case nil
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f [] = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) []))

Tactic:
simp

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) l))
⊢ findFinIdx? f (a :: l) = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) (a :: l)))

Tactic:
simp [hf, findFinIdx?_cons]

Result:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) l))
⊢ (if g a.val = true then some 0 else Option.map Fin.succ (findFinIdx? f l)) =
    Option.map (fun i => Fin.cast ⋯ i)
      (if g a.val = true then some 0 else Option.map Fin.succ (findFinIdx? g (map (fun x => x.val) l)))

Proof state:
α : Type ?u.111352
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
i : Fin l.unattach.length
⊢ l.unattach.length = l.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g l.unattach)

Tactic:
unfold unattach

Result:
α : Type u_1
p : α → Prop
l : List { x // p x }
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) l))

Proof state:
case cons
α : Type u_1
p : α → Prop
f : { x // p x } → Bool
g : α → Bool
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
a : { x // p x }
l : List { x // p x }
ih : findFinIdx? f l = Option.map (fun i => Fin.cast ⋯ i) (findFinIdx? g (map (fun x => x.val) l))
⊢ (if g a.val = true then some 0 else Option.map Fin.succ (findFinIdx? f l)) =
    Option.map (fun i => Fin.cast ⋯ i)
      (if g a.val = true then some 0 else Option.map Fin.succ (findFinIdx? g (map (fun x => x.val) l)))

Tactic:
split <;> simp [ih, Function.comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_eq_map_add (l : Vector α n) (m : Nat) :
    l.zipIdx m = l.zipIdx.map (fun ⟨a, i⟩ => (a, m + i))

Proof state:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.zipIdx m =
    map
      (fun x =>
        match x with
        | (a, i) => (a, m + i))
      { toArray := l, size_toArray := ⋯ }.zipIdx

Tactic:
simp only [zipIdx_mk, map_mk, eq_mk]

Result:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ l.zipIdx m = Array.map (fun x => (x.fst, m + x.snd)) l.zipIdx

Proof state:
α : Type u_1
n : Nat
l : Vector α n
m : Nat
⊢ l.zipIdx m =
    map
      (fun x =>
        match x with
        | (a, i) => (a, m + i))
      l.zipIdx

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.zipIdx m =
    map
      (fun x =>
        match x with
        | (a, i) => (a, m + i))
      { toArray := l, size_toArray := ⋯ }.zipIdx

Proof state:
case mk
α : Type u_1
m : Nat
l : Array α
⊢ l.zipIdx m = Array.map (fun x => (x.fst, m + x.snd)) l.zipIdx

Tactic:
rw [Array.zipIdx_eq_map_add]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Defs.lean
theorem vsub_add_vsub_cancel (p₁ p₂ p₃ : P) : p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃

Tactic:
rw [add_vadd, vsub_vadd, vsub_vadd, vsub_vadd]

Result:
no goals

Proof state:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₁ -ᵥ p₂ + (p₂ -ᵥ p₃) = p₁ -ᵥ p₃

Tactic:
apply vadd_right_cancel p₃

Result:
G : Type u_1
P : Type u_2
inst✝ : AddGroup G
T : AddTorsor G P
p₁ p₂ p₃ : P
⊢ (p₁ -ᵥ p₂ + (p₂ -ᵥ p₃)) +ᵥ p₃ = (p₁ -ᵥ p₃) +ᵥ p₃
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem mkHom_f_succ_succ (n : ℕ) :
    (mkHom P Q zero one one_zero_comm succ).f (n + 2) =
      (succ n
          ⟨(mkHom P Q zero one one_zero_comm succ).f n,
            (mkHom P Q zero one one_zero_comm succ).f (n + 1),
            (mkHom P Q zero one one_zero_comm succ).comm n (n + 1)⟩).1

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
P Q : CochainComplex V ℕ
zero : P.X 0 ⟶ Q.X 0
one : P.X 1 ⟶ Q.X 1
one_zero_comm : zero ≫ Q.d 0 1 = P.d 0 1 ≫ one
succ :
  (n : ℕ) →
    (p : (f : P.X n ⟶ Q.X n) ×' (f' : P.X (n + 1) ⟶ Q.X (n + 1)) ×' f ≫ Q.d n (n + 1) = P.d n (n + 1) ≫ f') →
      (f'' : P.X (n + 2) ⟶ Q.X (n + 2)) ×' p.snd.fst ≫ Q.d (n + 1) (n + 2) = P.d (n + 1) (n + 2) ≫ f''
n : ℕ
⊢ (P.mkHom Q zero one one_zero_comm succ).f (n + 2) =
    (succ n ⟨(P.mkHom Q zero one one_zero_comm succ).f n, ⟨(P.mkHom Q zero one one_zero_comm succ).f (n + 1), ⋯⟩⟩).fst

Tactic:
dsimp [mkHom, mkHomAux]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem snd_eq (κ : Kernel α (β × γ)) : snd κ = map κ Prod.snd

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
⊢ κ.snd = κ.map Prod.snd

Tactic:
simp [snd]

Result:
no goals
-- Mathlib/NumberTheory/FLT/Three.lean
lemma a_add_eta_mul_b : S.a + η * S.b = (S.a + S.b) + λ * S.b

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + hζ.toInteger * S.b = S.a + S.b + λ * S.b

Tactic:
ring

Result:
no goals

Proof state:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + ↑η * S.b = S.a + S.b + λ * S.b

Tactic:
rw [coe_eta]

Result:
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S : Solution hζ
⊢ S.a + hζ.toInteger * S.b = S.a + S.b + λ * S.b
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_apply_ite_of_true {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β)
    (h : ∀ x ∈ s, p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (f x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (f x)

Tactic:
exact prod_ite_of_true h _ _

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

Tactic:
simp_rw [apply_ite k]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (f x)