harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem exp_eq_one_iff {x : ℂ} : exp x = 1 ↔ ∃ n : ℤ, x = n * (2 * π * I)

Proof state:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0

Tactic:
have : (x + n * (2 * π * I)).im ∈ Set.Ioc (-π) π := by simpa [two_mul, mul_add] using hn

Result:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0

Proof state:
case mp
x : ℂ
h : cexp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
rcases existsUnique_add_zsmul_mem_Ioc Real.two_pi_pos x.im (-π) with ⟨n, hn, -⟩

Result:
case mp.intro.intro
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Proof state:
case mp.intro.intro
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
use -n

Result:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)

Proof state:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
this : (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π
⊢ x + ↑n * (2 * ↑π * I) = 0

Tactic:
rw [← log_exp this.1 this.2, exp_periodic.int_mul n, h, log_one]

Result:
no goals

Proof state:
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ (x + ↑n * (2 * ↑π * I)).im ∈ Set.Ioc (-π) π

Tactic:
simpa [two_mul, mul_add] using hn

Result:
no goals

Proof state:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x = ↑(-n) * (2 * ↑π * I)

Tactic:
rw [Int.cast_neg, neg_mul, eq_neg_iff_add_eq_zero]

Result:
case h
x : ℂ
h : cexp x = 1
n : ℤ
hn : x.im + n • (2 * π) ∈ Set.Ioc (-π) (-π + 2 * π)
⊢ x + ↑n * (2 * ↑π * I) = 0

Proof state:
case mpr.intro
n : ℤ
⊢ cexp (↑n * (2 * ↑π * I)) = 1

Tactic:
exact (exp_periodic.int_mul n).eq.trans exp_zero

Result:
no goals

Proof state:
case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → cexp x = 1

Tactic:
rintro ⟨n, rfl⟩

Result:
case mpr.intro
n : ℤ
⊢ cexp (↑n * (2 * ↑π * I)) = 1

Proof state:
x : ℂ
⊢ cexp x = 1 ↔ ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
constructor

Result:
case mp
x : ℂ
⊢ cexp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)

case mpr
x : ℂ
⊢ (∃ n, x = ↑n * (2 * ↑π * I)) → cexp x = 1

Proof state:
case mp
x : ℂ
⊢ cexp x = 1 → ∃ n, x = ↑n * (2 * ↑π * I)

Tactic:
intro h

Result:
case mp
x : ℂ
h : cexp x = 1
⊢ ∃ n, x = ↑n * (2 * ↑π * I)
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_prod {ι : Type*} [DecidableEq σ] {s : Finset ι} (f : ι → MvPolynomial σ R) :
    (∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars

Tactic:
classical
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Result:
no goals

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i => (f i).vars
⊢ (f a✝).vars ∪ (∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i => (f i).vars

Tactic:
exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ s, f i).vars ⊆ s.biUnion fun i => (f i).vars

Tactic:
induction s using Finset.induction_on with
| empty => simp
| insert hs hsub =>
  simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
  apply Finset.Subset.trans (vars_mul _ _)
  exact Finset.union_subset_union (Finset.Subset.refl _) hsub

Result:
no goals

Proof state:
case empty
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
⊢ (∏ i ∈ ∅, f i).vars ⊆ ∅.biUnion fun i => (f i).vars

Tactic:
simp

Result:
no goals

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i => (f i).vars
⊢ (∏ i ∈ insert a✝ s✝, f i).vars ⊆ (insert a✝ s✝).biUnion fun i => (f i).vars

Tactic:
simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i => (f i).vars
⊢ (f a✝ * ∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i => (f i).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i => (f i).vars
⊢ (f a✝ * ∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i => (f i).vars

Tactic:
apply Finset.Subset.trans (vars_mul _ _)

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq σ
f : ι → MvPolynomial σ R
a✝ : ι
s✝ : Finset ι
hs : a✝ ∉ s✝
hsub : (∏ i ∈ s✝, f i).vars ⊆ s✝.biUnion fun i => (f i).vars
⊢ (f a✝).vars ∪ (∏ i ∈ s✝, f i).vars ⊆ (f a✝).vars ∪ s✝.biUnion fun i => (f i).vars
-- Mathlib/Data/Vector/Basic.lean
theorem eq_cons_iff (a : α) (v : Vector α n.succ) (v' : Vector α n) :
    v = a ::ᵥ v' ↔ v.head = a ∧ v.tail = v' :=
  ⟨fun h => h.symm ▸ ⟨head_cons a v', tail_cons a v'⟩, fun h =>
    _root_.trans (cons_head_tail v).symm (by rw [h.1, h.2])⟩

Proof state:
α : Type u_1
n : ℕ
a : α
v : Vector α n.succ
v' : Vector α n
h : v.head = a ∧ v.tail = v'
⊢ v.head ::ᵥ v.tail = a ::ᵥ v'

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

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_filter (p : α → Bool) (f : α → β → β) (l : List α) (init : β) :
    (l.filter p).foldr f init = l.foldr (fun x y => if p x then f x y else y) init

Proof state:
case nil
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
init : β
⊢ foldr f init (filter p []) = foldr (fun x y => if p x = true then f x y else y) init []

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
a : α
l : List α
ih : ∀ (init : β), foldr f init (filter p l) = foldr (fun x y => if p x = true then f x y else y) init l
init : β
⊢ foldr f init (if p a = true then a :: filter p l else filter p l) =
    if p a = true then f a (foldr (fun x y => if p x = true then f x y else y) init l)
    else foldr (fun x y => if p x = true then f x y else y) init l

Tactic:
split <;> simp [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
a : α
l : List α
ih : ∀ (init : β), foldr f init (filter p l) = foldr (fun x y => if p x = true then f x y else y) init l
init : β
⊢ foldr f init (filter p (a :: l)) = foldr (fun x y => if p x = true then f x y else y) init (a :: l)

Tactic:
simp only [filter_cons, foldr_cons]

Result:
case cons
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
a : α
l : List α
ih : ∀ (init : β), foldr f init (filter p l) = foldr (fun x y => if p x = true then f x y else y) init l
init : β
⊢ foldr f init (if p a = true then a :: filter p l else filter p l) =
    if p a = true then f a (foldr (fun x y => if p x = true then f x y else y) init l)
    else foldr (fun x y => if p x = true then f x y else y) init l

Proof state:
α : Type u_1
β : Type u_2
p : α → Bool
f : α → β → β
l : List α
init : β
⊢ foldr f init (filter p l) = foldr (fun x y => if p x = true then f x y else y) init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filter_cons, foldr_cons]
  split <;> simp [ih]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem add : mapFun f (x + y) = mapFun f x + mapFun f y

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x + y) = mapFun (⇑f) x + mapFun (⇑f) y

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/Topology/NhdsSet.lean
theorem IsClosed.nhdsSet_le_sup (h : IsClosed t) : 𝓝ˢ s ≤ 𝓝ˢ (s ∩ t) ⊔ 𝓟 (tᶜ) :=
  calc
    𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ) = 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ (s ∩ tᶜ)

Tactic:
rw [nhdsSet_union]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ (s ∩ t) ⊔ 𝓝ˢ tᶜ = 𝓝ˢ (s ∩ t) ⊔ 𝓟 tᶜ

Tactic:
rw [h.isOpen_compl.nhdsSet_eq]

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s t : Set X
h : IsClosed t
⊢ 𝓝ˢ s = 𝓝ˢ (s ∩ t ∪ s ∩ tᶜ)

Tactic:
rw [Set.inter_union_compl s t]

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem product_inter [DecidableEq α] [DecidableEq β] : s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ s ×ˢ (t ∩ t') = s ×ˢ t ∩ s ×ˢ t'

Tactic:
ext ⟨x, y⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∩ t') ↔ (x, y) ∈ s ×ˢ t ∩ s ×ˢ t'

Proof state:
case h.mk
α : Type u_1
β : Type u_2
s : Finset α
t t' : Finset β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x : α
y : β
⊢ (x, y) ∈ s ×ˢ (t ∩ t') ↔ (x, y) ∈ s ×ˢ t ∩ s ×ˢ t'

Tactic:
simp only [← and_and_left, mem_inter, mem_product]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem has_fderiv_at_filter_real_equiv {L : Filter E} :
    Tendsto (fun x' : E => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
      Tendsto (fun x' : E => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
rw [tendsto_iff_norm_sub_tendsto_zero]

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun e => ‖‖e - x‖⁻¹ • (f e - f x - f' (e - x)) - 0‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
x' : E
⊢ ‖‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x)) - 0‖ = ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖

Tactic:
simp [norm_smul]

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun e => ‖‖e - x‖⁻¹ • (f e - f x - f' (e - x)) - 0‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)

Tactic:
refine tendsto_congr fun x' => ?_

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
x' : E
⊢ ‖‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x)) - 0‖ = ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0)

Tactic:
symm

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f : E → F
f' : E →L[ℝ] F
x : E
L : Filter E
⊢ Tendsto (fun x' => ‖x' - x‖⁻¹ • (f x' - f x - f' (x' - x))) L (𝓝 0) ↔
    Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - f' (x' - x)‖) L (𝓝 0)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getLsbD_eq_getMsbD (x : BitVec w) (i : Nat) : x.getLsbD i = (decide (i < w) && x.getMsbD (w - 1 - i))

Proof state:
case pos
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : w - 1 - i < w
⊢ x.getLsbD i = x.getLsbD (w - 1 - (w - 1 - i))

Tactic:
congr

Result:
case pos.e_i
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : w - 1 - i < w
⊢ i = w - 1 - (w - 1 - i)

Proof state:
case pos.e_i
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : w - 1 - i < w
⊢ i = w - 1 - (w - 1 - i)

Tactic:
omega

Result:
no goals

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

Tactic:
by_cases h₁ : i < w <;> by_cases h₂ : w - 1 - i < w <;>
  simp only [h₁, h₂] <;> simp only [decide_true, decide_false, Bool.false_and, Bool.and_false, Bool.true_and, Bool.and_true]

Result:
case pos
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : w - 1 - i < w
⊢ x.getLsbD i = x.getLsbD (w - 1 - (w - 1 - i))

case neg
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : ¬w - 1 - i < w
⊢ x.getLsbD i = false

case pos
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : w - 1 - i < w
⊢ x.getLsbD i = false

case neg
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : ¬w - 1 - i < w
⊢ x.getLsbD i = false

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
h₁ : i < w
h₂ : ¬w - 1 - i < w
⊢ x.getLsbD i = false

case pos
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : w - 1 - i < w
⊢ x.getLsbD i = false

case neg
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : ¬w - 1 - i < w
⊢ x.getLsbD i = false

Tactic:
all_goals
  apply getLsbD_ge
  omega

Result:
no goals

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

Tactic:
rw [getMsbD]

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

Proof state:
case neg
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : ¬w - 1 - i < w
⊢ x.getLsbD i = false

Tactic:
apply getLsbD_ge

Result:
case neg.ge
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : ¬w - 1 - i < w
⊢ w ≤ i

Proof state:
case neg.ge
w : Nat
x : BitVec w
i : Nat
h₁ : ¬i < w
h₂ : ¬w - 1 - i < w
⊢ w ≤ i

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Lattice.lean
theorem mem_closure_singleton {x y : G} : y ∈ closure ({x} : Set G) ↔ ∃ n : ℤ, x ^ n = y

Proof state:
case refine_3.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
m : ℤ
hy✝ : x ^ m ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = x ^ n * x ^ m

Tactic:
exact ⟨n + m, zpow_add x n m⟩

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x

Tactic:
exact ⟨1, zpow_one x⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x y : G
⊢ y ∈ closure {x} ↔ ∃ n, x ^ n = y

Tactic:
refine
  ⟨fun hy => closure_induction ?_ ?_ ?_ ?_ hy, fun ⟨n, hn⟩ =>
    hn ▸ zpow_mem (subset_closure <| mem_singleton x) n⟩

Result:
case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Proof state:
case refine_3
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ (x_1 y : G), x_1 ∈ closure {x} → y ∈ closure {x} → (∃ n, x ^ n = x_1) → (∃ n, x ^ n = y) → ∃ n, x ^ n = x_1 * y

Tactic:
rintro _ _ _ _ ⟨n, rfl⟩ ⟨m, rfl⟩

Result:
case refine_3.intro.intro
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
m : ℤ
hy✝ : x ^ m ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = x ^ n * x ^ m

Proof state:
case refine_4.intro
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹

Tactic:
exact ⟨-n, zpow_neg x n⟩

Result:
no goals

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ {x}, ∃ n, x ^ n = x_1

Tactic:
intro y hy

Result:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y

Proof state:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = y

Tactic:
rw [eq_of_mem_singleton hy]

Result:
case refine_1
G : Type u_1
inst✝ : Group G
x y✝ : G
hy✝ : y✝ ∈ closure {x}
y : G
hy : y ∈ {x}
⊢ ∃ n, x ^ n = x

Proof state:
case refine_4
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∀ x_1 ∈ closure {x}, (∃ n, x ^ n = x_1) → ∃ n, x ^ n = x_1⁻¹

Tactic:
rintro _ _ ⟨n, rfl⟩

Result:
case refine_4.intro
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
n : ℤ
hx✝ : x ^ n ∈ closure {x}
⊢ ∃ n_1, x ^ n_1 = (x ^ n)⁻¹

Proof state:
case refine_2
G : Type u_1
inst✝ : Group G
x y : G
hy : y ∈ closure {x}
⊢ ∃ n, x ^ n = 1

Tactic:
exact ⟨0, zpow_zero x⟩

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/QuadraticReciprocity.lean
theorem at_neg_two (hp : p ≠ 2) : legendreSym p (-2) = χ₈' p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ legendreSym p (-2) = χ₈' ↑p

Tactic:
have : (-2 : ZMod p) = (-2 : ℤ) := by norm_cast

Result:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = χ₈' ↑p

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
this : -2 = ↑(-2)
⊢ legendreSym p (-2) = χ₈' ↑p

Tactic:
rw [legendreSym, ← this, quadraticChar_neg_two ((ringChar_zmod_n p).substr hp), card p]

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
⊢ -2 = ↑(-2)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/DegreewiseSplit.lean
@[reassoc (attr := simp)]
lemma mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃ :
    (mappingConeHomOfDegreewiseSplitIso S σ).inv ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ = -S.g⟦(1 : ℤ)⟧'

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ ((mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃).f n =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g).f n

Tactic:
dsimp [mappingConeHomOfDegreewiseSplitXIso]

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ (S.g.f (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ -
        (σ (n + 1)).r ≫ 𝟙 (S.X₁.X (n + 1)) ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃.f n =
    -S.g.f (n + 1)

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
⊢ (mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃ =
    -(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ ((mappingConeHomOfDegreewiseSplitIso S σ).inv ≫ (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃).f n =
    (-(CategoryTheory.shiftFunctor (CochainComplex C ℤ) 1).map S.g).f n

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex (CochainComplex C ℤ)
σ : (n : ℤ) → (S.map (eval C (ComplexShape.up ℤ) n)).Splitting
inst✝ : HasBinaryBiproducts C
n : ℤ
⊢ (S.g.f (n + 1) ≫ (mappingCone.inl (homOfDegreewiseSplit S σ)).v (n + 1) n ⋯ -
        (σ (n + 1)).r ≫ 𝟙 (S.X₁.X (n + 1)) ≫ (mappingCone.inr (homOfDegreewiseSplit S σ)).f n) ≫
      (mappingCone.triangle (homOfDegreewiseSplit S σ)).mor₃.f n =
    -S.g.f (n + 1)

Tactic:
simp only [Int.reduceNeg, id_comp, sub_comp, assoc, mappingCone.inl_v_triangle_mor₃_f,
  shiftFunctor_obj_X, shiftFunctorObjXIso, XIsoOfEq_rfl, Iso.refl_inv, comp_neg, comp_id,
  mappingCone.inr_f_triangle_mor₃_f, comp_zero, sub_zero]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean
theorem d_eq (n : ℕ) : ((groupCohomology.resolution k G).d (n + 1) n).hom =
    ModuleCat.ofHom (d k G (n + 1))

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ ((-1) ^ ↑x✝¹ • lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Tactic:
erw [LinearMap.smul_apply]

Result:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ (-1) ^ ↑x✝¹ • (lmapDomain k k ((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom) (single x 1) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Proof state:
case hf
k G : Type u
inst✝¹ : CommRing k
inst✝ : Monoid G
n : ℕ
x : ((classifyingSpaceUniversalCover G).obj (Opposite.op (SimplexCategory.mk (n + 1)))).V
x✝¹ : Fin (n + 2)
x✝ : x✝¹ ∈ Finset.univ
⊢ single (((classifyingSpaceUniversalCover G).map (SimplexCategory.δ x✝¹).op).hom x) ((-1) ^ ↑x✝¹) =
    single (x ∘ x✝¹.succAbove) ((-1) ^ ↑x✝¹)

Tactic:
rfl

Result:
no goals