harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/PSeries.lean
theorem tsum_schlomilch_le {C : ℕ} (hf : ∀ ⦃m n⦄, 1 < m → m ≤ n → f n ≤ f m) (h_pos : ∀ n, 0 < u n)
    (h_nonneg : ∀ n, 0 ≤ f n) (hu : Monotone u) (h_succ_diff : SuccDiffBounded C u) :
    ∑' k : ℕ, (u (k + 1) - u k) * f (u k) ≤ (u 1 - u 0) * f (u 0) + C * ∑' k, f k

Proof state:
case refine_2
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ 0 ≤ ↑C

Tactic:
exact zero_le _

Result:
no goals

Proof state:
case refine_1
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ a ∈ range n.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤
    (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑ x ∈ Ico (u 0 + 1) (u n + 1), f x

Tactic:
simpa using Finset.sum_schlomilch_le hf h_pos h_nonneg hu h_succ_diff n

Result:
no goals

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ⨆ i, ∑ a ∈ range i.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

Tactic:
refine
  iSup_le fun n =>
    le_trans ?_
      (add_le_add_left
        (mul_le_mul_of_nonneg_left (ENNReal.sum_le_tsum <| Finset.Ico (u 0 + 1) (u n + 1)) ?_) _)

Result:
case refine_1
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ ∑ a ∈ range n.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤
    (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑ x ∈ Ico (u 0 + 1) (u n + 1), f x

case refine_2
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
n : ℕ
⊢ 0 ≤ ↑C

Proof state:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ∑' (k : ℕ), (↑(u (k + 1)) - ↑(u k)) * f (u k) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k

Tactic:
rw [ENNReal.tsum_eq_iSup_nat' (tendsto_atTop_mono Nat.le_succ tendsto_id)]

Result:
u : ℕ → ℕ
f : ℕ → ℝ≥0∞
C : ℕ
hf : ∀ ⦃m n : ℕ⦄, 1 < m → m ≤ n → f n ≤ f m
h_pos : ∀ (n : ℕ), 0 < u n
h_nonneg : ∀ (n : ℕ), 0 ≤ f n
hu : Monotone u
h_succ_diff : SuccDiffBounded C u
⊢ ⨆ i, ∑ a ∈ range i.succ, (↑(u (a + 1)) - ↑(u a)) * f (u a) ≤ (↑(u 1) - ↑(u 0)) * f (u 0) + ↑C * ∑' (k : ℕ), f k
-- Mathlib/RingTheory/FiniteType.lean
theorem freeAlgebra_lift_of_surjective_of_closure [CommSemiring R] {S : Set M}
    (hS : closure S = ⊤) :
    Function.Surjective
      (FreeAlgebra.lift R fun s : S => of R M ↑s : FreeAlgebra R S → MonoidAlgebra R M)

Proof state:
case hadd.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
g : MonoidAlgebra R M
ihg : ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = g
P : FreeAlgebra R ↑S
⊢ ∃ a, ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a = ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P + g

Tactic:
rcases ihg with ⟨Q, rfl⟩

Result:
case hadd.intro.intro
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
P Q : FreeAlgebra R ↑S
⊢ ∃ a,
    ((FreeAlgebra.lift R) fun s => (of R M) ↑s) a =
      ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P + ((FreeAlgebra.lift R) fun s => (of R M) ↑s) Q

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : CommSemiring R
S : Set M
hS : closure S = ⊤
m : M
this : m ∈ closure S
m₁ m₂ : M
hx✝ : m₁ ∈ closure S
hy✝ : m₂ ∈ closure S
P₁ : FreeAlgebra R ↑S
hP₁ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₁ = (of R M) m₁
P₂ : FreeAlgebra R ↑S
hP₂ : ((FreeAlgebra.lift R) fun s => (of R M) ↑s) P₂ = (of R M) m₂
⊢ ((FreeAlgebra.lift R) fun s => (of R M) ↑s) (P₁ * P₂) = (of R M) (m₁ * m₂)

Tactic:
rw [map_mul, hP₁, hP₂, of_apply, of_apply, of_apply, single_mul_single, one_mul]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem or_left_comm  : a ∨ (b ∨ c) ↔ b ∨ (a ∨ c)

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

Tactic:
rw [← or_assoc, ← or_assoc, @or_comm a b]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Multiset.lean
lemma map_add_left_Ico (a b c : α) : (Ico a b).map (c + ·) = Ico (c + a) (c + b)

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedCancelAddCommMonoid α
inst✝¹ : ExistsAddOfLE α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ map (fun x => c + x) (Ico a b) = Ico (c + a) (c + b)

Tactic:
classical rw [Ico, Ico, ← Finset.image_add_left_Ico, Finset.image_val,
    ((Finset.nodup _).map <| add_right_injective c).dedup]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
lemma ediam_eq_zero_of_subsingleton [Subsingleton α] : G.ediam = 0

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ G.ediam = 0

Tactic:
rw [ediam_def, ENat.iSup_eq_zero]

Result:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ ∀ (i : α × α), G.edist i.1 i.2 = 0

Proof state:
α : Type u_1
G : SimpleGraph α
inst✝ : Subsingleton α
⊢ ∀ (i : α × α), G.edist i.1 i.2 = 0

Tactic:
simpa [edist_eq_zero_iff, Prod.forall] using subsingleton_iff.mp ‹_›

Result:
no goals
-- Mathlib/Data/Finsupp/Single.lean
theorem equivFunOnFinite_single [DecidableEq α] [Finite α] (x : α) (m : M) :
    Finsupp.equivFunOnFinite (Finsupp.single x m) = Pi.single x m

Proof state:
α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
⊢ equivFunOnFinite (single x m) = Pi.single x m

Tactic:
ext

Result:
case h
α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
x✝ : α
⊢ equivFunOnFinite (single x m) x✝ = Pi.single x m x✝

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝² : Zero M
inst✝¹ : DecidableEq α
inst✝ : Finite α
x : α
m : M
x✝ : α
⊢ equivFunOnFinite (single x m) x✝ = Pi.single x m x✝

Tactic:
simp [Finsupp.single_eq_pi_single, equivFunOnFinite]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem of_card_lt [Finite Y] [IsPretransitive H Y] [IsPreprimitive G X]
    (hf' : Nat.card Y < 2 * (Set.range f).ncard) :
    IsPreprimitive H Y :=  by
  refine ⟨fun {B} hB ↦ ?_⟩
  rcases B.eq_empty_or_nonempty with hB' | hB'; · simp [IsTrivialBlock, hB']
  rw [IsTrivialBlock, or_iff_not_imp_right]
  intro hB_ne_top
  -- we need Set.Subsingleton B ↔ Set.ncard B ≤ 1
  suffices Set.ncard B < 2 by simpa [Nat.lt_succ] using this
  -- We reduce to proving that (Set.range f).ncard ≤ (orbit N B).ncard
  apply lt_of_mul_lt_mul_right (lt_of_le_of_lt _ hf') (zero_le _)
  simp only [← Nat.card_eq_fintype_card, ← hB.ncard_block_mul_ncard_orbit_eq hB']
  apply Nat.mul_le_mul_left
  -- We reduce to proving that (Set.range f ∩ g • B).ncard ≤ 1 for every g
  have hfin := Fintype.ofFinite (Set.range fun g : H ↦ g • B)
  rw [(hB.isBlockSystem hB').left.ncard_eq_finsum, finsum_eq_sum_of_fintype]
  apply le_trans (Finset.sum_le_card_nsmul _ _ 1 _)
  · rw [nsmul_one, Finset.card_univ, ← Set.toFinset_card, ← Set.ncard_eq_toFinset_card',
      orbit, Nat.cast_id]
  · rintro ⟨x, ⟨g, rfl⟩⟩ -
    suffices Set.Subsingleton (Set.range f ∩ g • B) by simpa
    -- It suffices to prove that the preimage is subsingleton
    rw [← Set.image_preimage_eq_range_inter]
    apply Set.Subsingleton.image
    -- Since the action of M on α is primitive, it suffices to prove that
    -- the preimage is a block which is not ⊤
    apply Or.resolve_right (isTrivialBlock_of_isBlock ((hB.translate g).preimage f))
    intro h
    simp only [Set.top_eq_univ, Set.preimage_eq_univ_iff] at h
    -- We will prove that B is large, which will contradict the assumption that it is not ⊤
    apply hB_ne_top
    apply hB.eq_univ_of_card_lt
    -- It remains to show that Nat.card β < Set.ncard B * 2
    apply lt_of_lt_of_le hf'
    rw [mul_comm, mul_le_mul_right Nat.succ_pos']
    apply le_trans (Set.ncard_le_ncard h) (Set.ncard_image_le B.toFinite)

Proof state:
case inr
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
⊢ ¬B = Set.univ → B.Subsingleton

Tactic:
intro hB_ne_top

Result:
case inr
G : Type u_1
X : Type u_2
inst✝⁶ : Group G
inst✝⁵ : MulAction G X
H : Type u_3
Y : Type u_4
inst✝⁴ : Group H
inst✝³ : MulAction H Y
φ : G → H
f : X →ₑ[φ] Y
inst✝² : Finite Y
inst✝¹ : IsPretransitive H Y
inst✝ : IsPreprimitive G X
hf' : Nat.card Y < 2 * (Set.range ⇑f).ncard
B : Set Y
hB : IsBlock H B
hB' : B.Nonempty
hB_ne_top : ¬B = Set.univ
⊢ B.Subsingleton
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
/-- If `X` is affine, the image of the zero locus of global sections of `X` under `X.isoSpec`
is the zero locus in terms of the prime spectrum of `Γ(X, ⊤)`. -/
lemma isoSpec_image_zeroLocus [IsAffine X]
    (s : Set Γ(X, ⊤)) :
    X.isoSpec.hom.base '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom X.isoSpec.hom.base) '' X.zeroLocus s = PrimeSpectrum.zeroLocus s

Tactic:
rw [← X.toSpecΓ_preimage_zeroLocus]

Result:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom X.isoSpec.hom.base) '' (⇑(hom X.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s) = PrimeSpectrum.zeroLocus s

Proof state:
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ ⇑(hom X.isoSpec.hom.base) '' (⇑(hom X.toSpecΓ.base) ⁻¹' PrimeSpectrum.zeroLocus s) = PrimeSpectrum.zeroLocus s

Tactic:
erw [Set.image_preimage_eq]

Result:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑(hom X.isoSpec.hom.base)

Proof state:
case h
X : Scheme
inst✝ : IsAffine X
s : Set ↑Γ(X, ⊤)
⊢ Function.Surjective ⇑(hom X.isoSpec.hom.base)

Tactic:
exact (bijective_of_isIso X.isoSpec.hom.base).surjective

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/IsOpenComapC.lean
theorem isOpenMap_comap_C : IsOpenMap (PrimeSpectrum.comap (C : R →+* R[X]))

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ IsOpenMap ⇑(PrimeSpectrum.comap C)

Tactic:
rintro U ⟨s, z⟩

Result:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⇑(PrimeSpectrum.comap C) '' U)

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, ⇑(PrimeSpectrum.comap C) '' (zeroLocus {↑i})ᶜ)

Tactic:
simp_rw [← imageOfDf_eq_comap_C_compl_zeroLocus]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, imageOfDf ↑i)

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, imageOfDf ↑i)

Tactic:
exact isOpen_iUnion fun f => isOpen_imageOfDf

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⇑(PrimeSpectrum.comap C) '' U)

Tactic:
rw [← compl_compl U, ← z, ← iUnion_of_singleton_coe s, zeroLocus_iUnion, compl_iInter,
  image_iUnion]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (⋃ i, ⇑(PrimeSpectrum.comap C) '' (zeroLocus {↑i})ᶜ)
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem zero_morphism_ext {P Q : C} (f : P ⟶ Q) : (∀ a, f a = 0) → f = 0 := fun h => by
  rw [← Category.id_comp f]
  exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ f = 0

Tactic:
rw [← Category.id_comp f]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q : C
f : P ⟶ Q
h : ∀ (a : Pseudoelement P), pseudoApply f a = 0
⊢ 𝟙 P ≫ f = 0

Tactic:
exact (pseudoZero_iff (𝟙 P ≫ f : Over Q)).1 (h (𝟙 P))

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem zpow_pow_orderOf : (x ^ i) ^ orderOf x = 1

Proof state:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
rw [← zpow_natCast, ← zpow_mul, mul_comm, zpow_mul, zpow_natCast, pow_orderOf_eq_one, one_zpow]

Result:
no goals

Proof state:
case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
rw [orderOf_eq_zero h, _root_.pow_zero]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
⊢ (x ^ i) ^ orderOf x = 1

Tactic:
by_cases h : IsOfFinOrder x

Result:
case pos
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1

case neg
G : Type u_1
inst✝ : Group G
x : G
i : ℤ
h : ¬IsOfFinOrder x
⊢ (x ^ i) ^ orderOf x = 1
-- Mathlib/NumberTheory/Cyclotomic/Gal.lean
theorem autToPow_injective : Function.Injective <| hμ.autToPow K

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hfg : ↑⋯.choose = ↑⋯.choose
⊢ f = g

Tactic:
generalize_proofs hn₀ hf' hg' at hfg

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hn₀ : NeZero ↑n
hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hfg : ↑hf'.choose = ↑hg'.choose
⊢ f = g

Proof state:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hn₀ : NeZero ↑n
hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hfg : hf'.choose ≡ hg'.choose [MOD ↑n]
hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose
hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose
⊢ ↑↑hμ.toRootsOfUnity ^ hf'.choose = ↑↑hμ.toRootsOfUnity ^ hg'.choose

Tactic:
rw [← rootsOfUnity.coe_pow _ hf'.choose, ← rootsOfUnity.coe_pow _ hg'.choose]

Result:
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hn₀ : NeZero ↑n
hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hfg : hf'.choose ≡ hg'.choose [MOD ↑n]
hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose
hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose
⊢ ↑↑(hμ.toRootsOfUnity ^ hf'.choose) = ↑↑(hμ.toRootsOfUnity ^ hg'.choose)

Proof state:
case a.h
n : ℕ+
K : Type u_1
inst✝⁴ : Field K
L : Type u_2
μ : L
inst✝³ : CommRing L
inst✝² : IsDomain L
hμ : IsPrimitiveRoot μ ↑n
inst✝¹ : Algebra K L
inst✝ : IsCyclotomicExtension {n} K L
f g : L ≃ₐ[K] L
hn₀ : NeZero ↑n
hf' : ∃ m, f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hg' : ∃ m, g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ m
hfg : ↑hf'.choose = ↑hg'.choose
hf : f ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hf'.choose
hg : g ↑↑hμ.toRootsOfUnity = ↑↑hμ.toRootsOfUnity ^ hg'.choose
this : f ↑↑hμ.toRootsOfUnity = g ↑↑hμ.toRootsOfUnity
⊢ ↑f (IsPrimitiveRoot.powerBasis K hμ).gen = ↑g (IsPrimitiveRoot.powerBasis K hμ).gen

Tactic:
exact this

Result:
no goals
-- Mathlib/RingTheory/IsTensorProduct.lean
theorem IsTensorProduct.lift_eq (h : IsTensorProduct f) (f' : M₁ →ₗ[R] M₂ →ₗ[R] M') (x₁ : M₁)
    (x₂ : M₂) : h.lift f' (f x₁ x₂) = f' x₁ x₂

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ (TensorProduct.lift f' ∘ₗ ↑h.equiv.symm) ((f x₁) x₂) = (f' x₁) x₂

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁸ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ (h.lift f') ((f x₁) x₂) = (f' x₁) x₂

Tactic:
delta IsTensorProduct.lift

Result:
R : Type u_1
inst✝⁸ : CommSemiring R
M₁ : Type u_2
M₂ : Type u_3
M : Type u_4
M' : Type u_5
inst✝⁷ : AddCommMonoid M₁
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M'
inst✝³ : Module R M₁
inst✝² : Module R M₂
inst✝¹ : Module R M
inst✝ : Module R M'
f : M₁ →ₗ[R] M₂ →ₗ[R] M
h : IsTensorProduct f
f' : M₁ →ₗ[R] M₂ →ₗ[R] M'
x₁ : M₁
x₂ : M₂
⊢ (TensorProduct.lift f' ∘ₗ ↑h.equiv.symm) ((f x₁) x₂) = (f' x₁) x₂
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
/-- A locally compact manifold must be modelled on a locally compact space. -/
lemma LocallyCompactSpace.of_locallyCompact_manifold (I : ModelWithCorners 𝕜 E H)
    [h : Nonempty M] [LocallyCompactSpace M] :
    LocallyCompactSpace E

Proof state:
case intro
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
⊢ LocallyCompactSpace E

Tactic:
obtain ⟨y, hy⟩ := interior_extChartAt_target_nonempty I x

Result:
case intro.intro
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
⊢ LocallyCompactSpace E

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
h : Nonempty M
inst✝ : LocallyCompactSpace M
⊢ LocallyCompactSpace E

Tactic:
rcases h with ⟨x⟩

Result:
case intro
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
⊢ LocallyCompactSpace E

Proof state:
case intro.intro.intro.intro.intro
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 (↑(extChartAt I x).symm y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact (↑(extChartAt I x) '' s)
⊢ ↑(extChartAt I x) '' s ∈ 𝓝 (↑(extChartAt I x) (↑(extChartAt I x).symm y))

Tactic:
apply extChartAt_image_nhd_mem_nhds_of_mem_interior_range
  (PartialEquiv.map_target (extChartAt I x) h'y) _ hmem

Result:
E : Type u_8
𝕜 : Type u_9
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
H : Type u_10
inst✝³ : TopologicalSpace H
M : Type u_11
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
I : ModelWithCorners 𝕜 E H
inst✝ : LocallyCompactSpace M
x : M
y : E
hy : y ∈ interior (extChartAt I x).target
h'y : y ∈ (extChartAt I x).target
s : Set M
hmem : s ∈ 𝓝 (↑(extChartAt I x).symm y)
hss : s ⊆ (extChartAt I x).source
hcom : IsCompact s
this : IsCompact (↑(extChartAt I x) '' s)
⊢ ↑(extChartAt I x) (↑(extChartAt I x).symm y) ∈ interior (range ↑I)
-- Mathlib/Algebra/Group/Nat/Units.lean
@[simp] protected lemma isUnit_iff {n : ℕ} : IsUnit n ↔ n = 1 where
  mp

Proof state:
case intro

⊢ ↑1 = 1

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
⊢ IsUnit n → n = 1

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro
u : ℕˣ
⊢ ↑u = 1

Proof state:
case intro
u : ℕˣ
⊢ ↑u = 1

Tactic:
obtain rfl := Nat.units_eq_one u

Result:
case intro

⊢ ↑1 = 1
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem ascPochhammer_nat_eval_succ (r : ℕ) :
    ∀ n : ℕ, n * (ascPochhammer ℕ r).eval (n + 1) = (n + r) * (ascPochhammer ℕ r).eval n
  | 0 => by
    by_cases h : r = 0
    · simp only [h, zero_mul, zero_add]
    · simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]
  | k + 1 => by simp only [ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]

Proof state:
case neg
r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
simp only [ascPochhammer_eval_zero, zero_mul, if_neg h, mul_zero]

Result:
no goals

Proof state:
r k : ℕ
⊢ (k + 1) * eval (k + 1 + 1) (ascPochhammer ℕ r) = (k + 1 + r) * eval (k + 1) (ascPochhammer ℕ r)

Tactic:
simp only [ascPochhammer_nat_eq_ascFactorial, Nat.succ_ascFactorial, add_right_comm]

Result:
no goals

Proof state:
case pos
r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
simp only [h, zero_mul, zero_add]

Result:
no goals

Proof state:
r : ℕ
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

Tactic:
by_cases h : r = 0

Result:
case pos
r : ℕ
h : r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)

case neg
r : ℕ
h : ¬r = 0
⊢ 0 * eval (0 + 1) (ascPochhammer ℕ r) = (0 + r) * eval 0 (ascPochhammer ℕ r)