harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/FLT/Three.lean
/-- Given `S' : Solution'`, then there is `S₁ : Solution` such that
`S₁.multiplicity = S'.multiplicity`. -/
lemma exists_Solution_of_Solution' : ∃ (S₁ : Solution hζ), S₁.multiplicity = S'.multiplicity

Proof state:
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
⊢ ∃ S₁, S₁.multiplicity = S'.multiplicity

Tactic:
obtain ⟨a, b, H, coprime, ha, hb, hab⟩ := ex_cube_add_cube_eq_and_isCoprime_and_not_dvd_and_dvd S'

Result:
case intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
a b : 𝓞 K
H : a ^ 3 + b ^ 3 = ↑S'.u * S'.c ^ 3
coprime : IsCoprime a b
ha : ¬λ ∣ a
hb : ¬λ ∣ b
hab : λ ^ 2 ∣ a + b
⊢ ∃ S₁, S₁.multiplicity = S'.multiplicity

Proof state:
case intro.intro.intro.intro.intro.intro
K : Type u_1
inst✝³ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ ↑3
S' : Solution' hζ
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {3} ℚ K
inst✝ : DecidableRel fun a b => a ∣ b
a b : 𝓞 K
H : a ^ 3 + b ^ 3 = ↑S'.u * S'.c ^ 3
coprime : IsCoprime a b
ha : ¬λ ∣ a
hb : ¬λ ∣ b
hab : λ ^ 2 ∣ a + b
⊢ ∃ S₁, S₁.multiplicity = S'.multiplicity

Tactic:
exact ⟨
{ a := a
  b := b
  c := S'.c
  u := S'.u
  ha := ha
  hb := hb
  hc := S'.hc
  coprime := coprime
  hcdvd := S'.hcdvd
  H := H
  hab := hab }, rfl⟩

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem setIntegral_comp {f : γ → E} {s : Set γ} (hs : MeasurableSet s)
    (hf : IntegrableOn f s ((η ∘ₖ κ) a)) :
    ∫ z in s, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y in s, f y ∂η x ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ Integrable f ((η.restrict hs ∘ₖ κ) a)

Tactic:
rwa [comp_restrict, restrict_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (x : β), ∫ (y : γ), f y ∂(η.restrict hs) x ∂κ a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a

Tactic:
simp_rw [restrict_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (z : γ) in s, f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a

Tactic:
rw [← restrict_apply (η ∘ₖ κ) hs, ← comp_restrict hs, integral_comp]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ ∫ (x : β), ∫ (y : γ), f y ∂(η.restrict hs) x ∂κ a = ∫ (x : β), ∫ (y : γ) in s, f y ∂η x ∂κ a

α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f : γ → E
s : Set γ
hs : MeasurableSet s
hf : IntegrableOn f s ((η ∘ₖ κ) a)
⊢ Integrable f ((η.restrict hs ∘ₖ κ) a)
-- Mathlib/Data/List/ToFinsupp.lean
theorem toFinsupp_cons_eq_single_add_embDomain {R : Type*} [AddZeroClass R] (x : R) (xs : List R)
    [DecidablePred (getD (x::xs) · 0 ≠ 0)] [DecidablePred (getD xs · 0 ≠ 0)] :
    toFinsupp (x::xs) =
      Finsupp.single 0 x + (toFinsupp xs).embDomain ⟨Nat.succ, Nat.succ_injective⟩

Proof state:
case h.e'_3.h.e'_6.h.e'_5.h
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
n : ℕ
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } n = (addLeftEmbedding [x].length) n

Tactic:
exact add_comm n 1

Result:
no goals

Proof state:
case h.e'_3.h.e'_6.h.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } = addLeftEmbedding [x].length

Tactic:
ext n

Result:
case h.e'_3.h.e'_6.h.e'_5.h
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
n : ℕ
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } n = (addLeftEmbedding [x].length) n

Proof state:
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
⊢ (x :: xs).toFinsupp =
    Finsupp.single 0 x + Finsupp.embDomain { toFun := Nat.succ, inj' := Nat.succ_injective } xs.toFinsupp

Tactic:
convert toFinsupp_append [x] xs using 3

Result:
case h.e'_3.h.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
⊢ Finsupp.single 0 x = [x].toFinsupp

case h.e'_3.h.e'_6.h.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
⊢ { toFun := Nat.succ, inj' := Nat.succ_injective } = addLeftEmbedding [x].length

Proof state:
case h.e'_3.h.e'_5
R : Type u_2
inst✝² : AddZeroClass R
x : R
xs : List R
inst✝¹ : DecidablePred fun x_1 => (x :: xs).getD x_1 0 ≠ 0
inst✝ : DecidablePred fun x => xs.getD x 0 ≠ 0
⊢ Finsupp.single 0 x = [x].toFinsupp

Tactic:
exact (toFinsupp_singleton x).symm

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Colimits.lean
lemma Quot.desc_quotQuotUliftAddEquiv [DecidableEq J] (c : Cocone F) :
    (Quot.desc (F ⋙ uliftFunctor.{u'}) (uliftFunctor.{u'}.mapCocone c)).comp
    (quotQuotUliftAddEquiv F).toAddMonoidHom =
    AddEquiv.ulift.symm.toAddMonoidHom.comp (Quot.desc F c)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((ι (F ⋙ uliftFunctor) j) { down := a }) =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Tactic:
erw [Quot.ι_desc]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)) { down := a } =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (ConcreteCategory.hom ((uliftFunctor.mapCocone c).ι.app j)) { down := a } =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Tactic:
rfl

Result:
no goals

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((quotToQuotUlift F) ((ι F j) a)) =
    AddEquiv.ulift.symm ((desc F c) ((ι F j) a))

Tactic:
simp only [quotToQuotUlift_ι, Functor.comp_obj, uliftFunctor_obj, ι_desc,
  Functor.const_obj_obj, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe, Function.comp_apply, ι_desc]

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((ι (F ⋙ uliftFunctor) j) { down := a }) =
    AddEquiv.ulift.symm ((ConcreteCategory.hom (c.ι.app j)) a)

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ ((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom) ((ι F j) a) =
    (AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)) ((ι F j) a)

Tactic:
dsimp

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)) ((quotToQuotUlift F) ((ι F j) a)) =
    AddEquiv.ulift.symm ((desc F c) ((ι F j) a))

Proof state:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
⊢ (desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom =
    AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)

Tactic:
refine Quot.addMonoidHom_ext _ (fun j a ↦ ?_)

Result:
J : Type u
inst✝¹ : Category.{v, u} J
F : J ⥤ AddCommGrp
inst✝ : DecidableEq J
c : Cocone F
j : J
a : ↑(F.obj j)
⊢ ((desc (F ⋙ uliftFunctor) (uliftFunctor.mapCocone c)).comp (quotQuotUliftAddEquiv F).toAddMonoidHom) ((ι F j) a) =
    (AddEquiv.ulift.symm.toAddMonoidHom.comp (desc F c)) ((ι F j) a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_and {x y : BitVec w} : (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)

Proof state:
w i : Nat
x y : BitVec w
⊢ (x &&& y).getMsbD i = (x.getMsbD i && y.getMsbD i)

Tactic:
simp only [getMsbD]

Result:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x &&& y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) && (decide (i < w) && y.getLsbD (w - 1 - i)))

Proof state:
w i : Nat
x y : BitVec w
⊢ (decide (i < w) && (x &&& y).getLsbD (w - 1 - i)) =
    (decide (i < w) && x.getLsbD (w - 1 - i) && (decide (i < w) && y.getLsbD (w - 1 - i)))

Tactic:
by_cases h : i < w <;> simp [h]

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Shadow.lean
/-- `t` is in the upper shadow of `𝒜` iff `t` is exactly `k` elements less than something from `𝒜`.

See also `Finset.mem_upShadow_iff_exists_mem_card_add`. -/
lemma mem_upShadow_iterate_iff_exists_sdiff : t ∈ ∂⁺^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ t \ (t \ s) ∈ 𝒜

Tactic:
rwa [sdiff_sdiff_eq_self hst]

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
rintro ⟨s, hs, hst, rfl⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ ∃ u, #u = #(t \ s) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
rw [mem_upShadow_iterate_iff_exists_card]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ #(t \ (t \ u)) = #u

Tactic:
rw [sdiff_sdiff_eq_self hut]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

case mpr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k) → ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Proof state:
case mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
k : ℕ
⊢ (∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜) → ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = k

Tactic:
rintro ⟨u, rfl, hut, htu⟩

Result:
case mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = #u

Proof state:
case mp.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ ∃ s ∈ 𝒜, s ⊆ t ∧ #(t \ s) = #u

Tactic:
exact ⟨_, htu, sdiff_subset, by rw [sdiff_sdiff_eq_self hut]⟩

Result:
no goals

Proof state:
case mpr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ ∃ u, #u = #(t \ s) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
exact ⟨_, rfl, sdiff_subset, by rwa [sdiff_sdiff_eq_self hst]⟩

Result:
no goals
-- Mathlib/Data/List/Basic.lean
lemma map_filter {f : α → β} (hf : Injective f) (l : List α)
    [DecidablePred fun b => ∃ a, p a ∧ f a = b] :
    (l.filter p).map f = (l.map f).filter fun b => ∃ a, p a ∧ f a = b

Proof state:
α : Type u
β : Type v
p : α → Bool
f : α → β
hf : Injective f
l : List α
inst✝ : DecidablePred fun b => ∃ a, p a = true ∧ f a = b
⊢ map f (filter p l) = filter (fun b => decide (∃ a, p a = true ∧ f a = b)) (map f l)

Tactic:
simp [comp_def, filter_map, hf.eq_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Independence.lean
theorem dependent_iff_not_independent : Dependent f ↔ ¬Independent f

Proof state:
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬Independent f

Tactic:
rw [dependent_iff, independent_iff]

Result:
no goals
-- Mathlib/NumberTheory/LucasLehmer.lean
theorem closed_form (i : ℕ) : (s i : X q) = (ω : X q) ^ 2 ^ i + (ωb : X q) ^ 2 ^ i

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2

Tactic:
rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]

Result:
no goals

Proof state:
q : ℕ+
i : ℕ
⊢ ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i

Tactic:
induction i with
| zero =>
  dsimp [s, ω, ωb]
  ext <;> norm_num
| succ i ih =>
  calc
    (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
    _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
    _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
    _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
    _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
      rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
    _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Result:
no goals

Proof state:
case zero
q : ℕ+
⊢ ↑(s 0) = ω ^ 2 ^ 0 + ωb ^ 2 ^ 0

Tactic:
dsimp [s, ω, ωb]

Result:
case zero
q : ℕ+
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1

Proof state:
case succ
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s (i + 1)) = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)

Tactic:
calc
  (s (i + 1) : X q) = (s i ^ 2 - 2 : ℤ) := rfl
  _ = (s i : X q) ^ 2 - 2 := by push_cast; rfl
  _ = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 := by rw [ih]
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2 := by ring
  _ = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 := by
    rw [← mul_pow ωb ω, ωb_mul_ω, one_pow, mul_one, add_sub_cancel_right]
  _ = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1) := by rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Result:
no goals

Proof state:
case zero
q : ℕ+
⊢ ↑4 = (2, 1) ^ 1 + (2, -1) ^ 1

Tactic:
ext <;> norm_num

Result:
no goals

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i ^ 2 - 2) = ↑(s i) ^ 2 - 2

Tactic:
push_cast

Result:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2

Tactic:
rw [ih]

Result:
no goals

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i + ωb ^ 2 ^ i) ^ 2 - 2 = (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 + 2 * (ωb ^ 2 ^ i * ω ^ 2 ^ i) - 2

Tactic:
ring

Result:
no goals

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ ↑(s i) ^ 2 - 2 = ↑(s i) ^ 2 - 2

Tactic:
rfl

Result:
no goals

Proof state:
q : ℕ+
i : ℕ
ih : ↑(s i) = ω ^ 2 ^ i + ωb ^ 2 ^ i
⊢ (ω ^ 2 ^ i) ^ 2 + (ωb ^ 2 ^ i) ^ 2 = ω ^ 2 ^ (i + 1) + ωb ^ 2 ^ (i + 1)

Tactic:
rw [← pow_mul, ← pow_mul, _root_.pow_succ]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem infDegree_withTop_some_comp {s : AddMonoidAlgebra R A} (hs : s.support.Nonempty) :
    infDegree (WithTop.some ∘ D) s = infDegree D s

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
⊢ s.support.inf (WithTop.some ∘ D) = ↑(s.support.inf D)

Tactic:
rw [← Finset.coe_inf' hs, Finset.inf'_eq_inf]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
⊢ infDegree (WithTop.some ∘ D) s = ↑(infDegree D s)

Tactic:
unfold AddMonoidAlgebra.infDegree

Result:
R : Type u_1
A : Type u_3
T : Type u_4
inst✝² : Semiring R
inst✝¹ : SemilatticeInf T
inst✝ : OrderTop T
D : A → T
s : R[A]
hs : s.support.Nonempty
⊢ s.support.inf (WithTop.some ∘ D) = ↑(s.support.inf D)
-- Mathlib/Data/List/NatAntidiagonal.lean
theorem antidiagonal_succ' {n : ℕ} :
    antidiagonal (n + 1) = (antidiagonal n).map (Prod.map id Nat.succ) ++ [(n + 1, 0)]

Proof state:
case e_a
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n)

Tactic:
apply map_congr_left

Result:
case e_a.h
n : ℕ
⊢ ∀ a ∈ range n, (a, n + 1 - a) = (Prod.map id succ ∘ fun i => (i, n - i)) a

Proof state:
n : ℕ
⊢ antidiagonal (n + 1) = map (Prod.map id succ) (antidiagonal n) ++ [(n + 1, 0)]

Tactic:
simp only [antidiagonal, range_succ, Nat.add_sub_cancel_left, map_append, append_assoc,
  Nat.sub_self, singleton_append, map_map, map]

Result:
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) ++ [(n, 1), (n + 1, 0)] =
    map (Prod.map id succ ∘ fun i => (i, n - i)) (range n) ++ [Prod.map id succ (n, 0), (n + 1, 0)]

Proof state:
case e_a.h
n : ℕ
⊢ ∀ a ∈ range n, (a, n + 1 - a) = (Prod.map id succ ∘ fun i => (i, n - i)) a

Tactic:
simp +contextual [le_of_lt, Nat.sub_add_comm]

Result:
no goals

Proof state:
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) ++ [(n, 1), (n + 1, 0)] =
    map (Prod.map id succ ∘ fun i => (i, n - i)) (range n) ++ [Prod.map id succ (n, 0), (n + 1, 0)]

Tactic:
congr 1

Result:
case e_a
n : ℕ
⊢ map (fun i => (i, n + 1 - i)) (range n) = map (Prod.map id succ ∘ fun i => (i, n - i)) (range n)
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_mem_commute' {g1 g2 : Perm α}
    (h1 : g1 ∈ f.cycleFactorsFinset) (h2 : g2 ∈ f.cycleFactorsFinset) :
    Commute g1 g2

Proof state:
case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Tactic:
exact Equiv.Perm.cycleFactorsFinset_mem_commute f h1 h2 h

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
⊢ Commute g1 g2

Tactic:
rcases eq_or_ne g1 g2 with rfl | h

Result:
case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 : Perm α
h1 h2 : g1 ∈ f.cycleFactorsFinset
⊢ Commute g1 g1

case inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 g2 : Perm α
h1 : g1 ∈ f.cycleFactorsFinset
h2 : g2 ∈ f.cycleFactorsFinset
h : g1 ≠ g2
⊢ Commute g1 g2

Proof state:
case inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g1 : Perm α
h1 h2 : g1 ∈ f.cycleFactorsFinset
⊢ Commute g1 g1

Tactic:
apply Commute.refl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.ro_eq_false_of_lo (u v k₁ k₂ : Nat) : isLt k₂ k₁ = true → u + k₁ ≤ v → (v ≤ u + k₂) = False

Proof state:
u v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ v → u + k₂ < v

Tactic:
omega

Result:
no goals

Proof state:
u v k₁ k₂ : Nat
⊢ isLt k₂ k₁ = true → u + k₁ ≤ v → (v ≤ u + k₂) = False

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ k₂ < k₁ → u + k₁ ≤ v → u + k₂ < v
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_eq_zero_iff_of_nonneg_ae (hf : 0 ≤ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] f)
    (hfi : IntervalIntegrable f μ a b) :
    ∫ x in a..b, f x ∂μ = 0 ↔ f =ᵐ[μ.restrict (Ioc a b ∪ Ioc b a)] 0

Proof state:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

Tactic:
exact integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi

Result:
no goals

Proof state:
case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0

Tactic:
rw [integral_symm, neg_eq_zero, integral_eq_zero_iff_of_le_of_nonneg_ae hab hf hfi.symm]

Result:
no goals

Proof state:
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] f
hfi : IntervalIntegrable f μ a b
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b ∪ Ioc b a))] 0

Tactic:
rcases le_total a b with hab | hab <;>
  simp only [Ioc_eq_empty hab.not_lt, empty_union, union_empty] at hf ⊢

Result:
case inl
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : a ≤ b
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc a b))] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc a b))] 0

case inr
f : ℝ → ℝ
a b : ℝ
μ : Measure ℝ
hfi : IntervalIntegrable f μ a b
hab : b ≤ a
hf : 0 ≤ᶠ[ae (μ.restrict (Ioc b a))] f
⊢ ∫ (x : ℝ) in a..b, f x ∂μ = 0 ↔ f =ᶠ[ae (μ.restrict (Ioc b a))] 0
-- Mathlib/Analysis/Normed/Operator/Compact.lean
theorem isCompactOperator_iff_exists_mem_nhds_isCompact_closure_image [T2Space M₂] (f : M₁ → M₂) :
    IsCompactOperator f ↔ ∃ V ∈ (𝓝 0 : Filter M₁), IsCompact (closure <| f '' V)

Proof state:
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ (∃ V ∈ 𝓝 0, ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))

Tactic:
exact
  ⟨fun ⟨V, hV, K, hK, hKV⟩ => ⟨V, hV, hK.closure_of_subset hKV⟩,
    fun ⟨V, hV, hVc⟩ => ⟨V, hV, closure (f '' V), hVc, subset_closure⟩⟩

Result:
no goals

Proof state:
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ IsCompactOperator f ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))

Tactic:
rw [isCompactOperator_iff_exists_mem_nhds_image_subset_compact]

Result:
M₁ : Type u_2
M₂ : Type u_3
inst✝³ : TopologicalSpace M₁
inst✝² : AddCommMonoid M₁
inst✝¹ : TopologicalSpace M₂
inst✝ : T2Space M₂
f : M₁ → M₂
⊢ (∃ V ∈ 𝓝 0, ∃ K, IsCompact K ∧ f '' V ⊆ K) ↔ ∃ V ∈ 𝓝 0, IsCompact (closure (f '' V))