harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/EMetricSpace/BoundedVariation.lean
theorem lowerSemicontinuous_uniformOn (s : Set α) :
    LowerSemicontinuous fun f : α →ᵤ[{s}] E => eVariationOn f s := fun f ↦ by
  apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E {s}) id (𝓝 f) f s _
  have := @tendsto_id _ (𝓝 f)
  rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at this
  simp_rw [← tendstoUniformlyOn_singleton_iff_tendsto]
  exact fun x xs => (this s rfl).mono (singleton_subset_iff.mpr xs)

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Tactic:
simp_rw [← tendstoUniformlyOn_singleton_iff_tendsto]

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ LowerSemicontinuousAt (fun f => eVariationOn f s) f

Tactic:
apply @lowerSemicontinuous_aux _ _ _ _ (UniformOnFun α E {s}) id (𝓝 f) f s _

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, TendstoUniformlyOn id f (𝓝 f) {x}

Tactic:
exact fun x xs => (this s rfl).mono (singleton_subset_iff.mpr xs)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Tactic:
have := @tendsto_id _ (𝓝 f)

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : Tendsto id (𝓝 f) (𝓝 f)
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : Tendsto id (𝓝 f) (𝓝 f)
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))

Tactic:
rw [UniformOnFun.tendsto_iff_tendstoUniformlyOn] at this

Result:
α : Type u_1
inst✝¹ : LinearOrder α
E : Type u_2
inst✝ : PseudoEMetricSpace E
s : Set α
f : α →ᵤ[{s}] E
this : ∀ s_1 ∈ {s}, TendstoUniformlyOn (⇑(UniformOnFun.toFun {s}) ∘ id) ((UniformOnFun.toFun {s}) f) (𝓝 f) s_1
⊢ ∀ x ∈ s, Tendsto (fun i => id i x) (𝓝 f) (𝓝 (f x))
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem subOneIntegralPowerBasis_gen [IsCyclotomicExtension {p ^ k} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) :
    hζ.subOneIntegralPowerBasis.gen =
      ⟨ζ - 1, Subalgebra.sub_mem _ (hζ.isIntegral (p ^ k).pos) (Subalgebra.one_mem _)⟩

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝² : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ hζ.subOneIntegralPowerBasis.gen = ⟨ζ - 1, ⋯⟩

Tactic:
simp [subOneIntegralPowerBasis]

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/Proper.lean
lemma IsFinite.eq_isProper_inf_isAffineHom :
    @IsFinite = (@IsProper ⊓ @IsAffineHom : MorphismProperty _)

Proof state:
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom

Tactic:
have : (@IsAffineHom ⊓ @IsSeparated : MorphismProperty _) = @IsAffineHom :=
  inf_eq_left.mpr fun _ _ _ _ ↦ inferInstance

Result:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom

Proof state:
this : @IsAffineHom ⊓ @IsSeparated = @IsAffineHom
⊢ @IsFinite = @IsProper ⊓ @IsAffineHom

Tactic:
rw [inf_comm, isProper_eq, inf_assoc, ← inf_assoc, this, eq_inf,
  IsIntegralHom.eq_universallyClosed_inf_isAffineHom, inf_assoc, inf_left_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_one (n : Nat) : n / 1 = n

Proof state:
n : Nat
this : n % 1 + 1 * (n / 1) = n
⊢ n / 1 = n

Tactic:
rwa [mod_one, Nat.zero_add, Nat.one_mul] at this

Result:
no goals

Proof state:
n : Nat
⊢ n / 1 = n

Tactic:
have := mod_add_div n 1

Result:
n : Nat
this : n % 1 + 1 * (n / 1) = n
⊢ n / 1 = n
-- Mathlib/Data/Int/Init.lean
@[norm_cast] lemma natCast_pred_of_pos {n : ℕ} (h : 0 < n) : ((n - 1 : ℕ) : ℤ) = (n : ℤ) - 1

Proof state:
case zero
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1

case succ
n✝ : ℕ
h : 0 < n✝ + 1
⊢ ↑(n✝ + 1 - 1) = ↑(n✝ + 1) - 1

Tactic:
cases h

Result:
case succ
n✝ : ℕ
h : 0 < n✝ + 1
⊢ ↑(n✝ + 1 - 1) = ↑(n✝ + 1) - 1

Proof state:
n : ℕ
h : 0 < n
⊢ ↑(n - 1) = ↑n - 1

Tactic:
cases n

Result:
case zero
h : 0 < 0
⊢ ↑(0 - 1) = ↑0 - 1

case succ
n✝ : ℕ
h : 0 < n✝ + 1
⊢ ↑(n✝ + 1 - 1) = ↑(n✝ + 1) - 1

Proof state:
case succ
n✝ : ℕ
h : 0 < n✝ + 1
⊢ ↑(n✝ + 1 - 1) = ↑(n✝ + 1) - 1

Tactic:
simp [ofNat_succ]

Result:
no goals
-- Mathlib/Tactic/Abel.lean
theorem term_add_constg {α} [AddCommGroup α] (n x a k a') (h : a + k = a') :
    @termg α _ n x a + k = termg n x a'

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a k a' : α
h : a + k = a'
⊢ termg n x a + k = termg n x a'

Tactic:
simp [h.symm, termg, add_assoc]

Result:
no goals
-- Mathlib/Data/Nat/Cast/Order/Basic.lean
theorem cast_add_one_pos (n : ℕ) : 0 < (n : α) + 1

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ ↑n + 1

Tactic:
convert (@mono_cast α _).imp (?_ : 1 ≤ n + 1)
<;> simp

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 0 < ↑n + 1

Tactic:
apply zero_lt_one.trans_le

Result:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : AddLeftMono α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
n : ℕ
⊢ 1 ≤ ↑n + 1
-- Mathlib/NumberTheory/RamificationInertia/Basic.lean
theorem finrank_prime_pow_ramificationIdx [IsDedekindDomain S] (hP0 : P ≠ ⊥)
    [p.IsMaximal] [P.IsPrime] (he : e ≠ 0) :
    finrank (R ⧸ p) (S ⧸ P ^ e) =
      e *
        @finrank (R ⧸ p) (S ⧸ P) _ _
          (@Algebra.toModule _ _ _ _ <|
            @Quotient.algebraQuotientOfRamificationIdxNeZero _ _ _ _ _ _ _ ⟨he⟩)

Proof state:
case neg
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : ¬FiniteDimensional (R ⧸ p) (S ⧸ P)
hPe : ¬FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
simp only [finrank_of_infinite_dimensional hP, finrank_of_infinite_dimensional hPe,
  mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
have hdim := rank_prime_pow_ramificationIdx _ _ hP0 he

Result:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Proof state:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
haveI := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP

Result:
case pos
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
p : Ideal R
P : Ideal S
inst✝³ : Algebra R S
inst✝² : IsDedekindDomain S
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝² : NeZero e := { out := he }
this✝¹ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP this✝ : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)
-- Mathlib/ModelTheory/Definability.lean
theorem definable_finset_biInter {ι : Type*} {f : ι → Set (α → M)}
    (hf : ∀ i, A.Definable L (f i)) (s : Finset ι) : A.Definable L (⋂ i ∈ s, f i)

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)

Tactic:
exact definable_finset_inf hf s

Result:
no goals

Proof state:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (⋂ i ∈ s, f i)

Tactic:
rw [← Finset.inf_set_eq_iInter]

Result:
M : Type w
A : Set M
L : Language
inst✝ : L.Structure M
α : Type u₁
ι : Type u_2
f : ι → Set (α → M)
hf : ∀ (i : ι), A.Definable L (f i)
s : Finset ι
⊢ A.Definable L (s.inf f)
-- Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean
theorem _root_.HasCompactSupport.integral_Ioi_deriv_eq (hf : ContDiff ℝ 1 f)
    (h2f : HasCompactSupport f) (b : ℝ) : ∫ x in Ioi b, deriv f x = - f b

Proof state:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
⊢ ∫ (x : ℝ) in Ioi b, deriv f x = -f b

Tactic:
have := fun x (_ : x ∈ Ioi b) ↦ hf.differentiable le_rfl x |>.hasDerivAt

Result:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ ∫ (x : ℝ) in Ioi b, deriv f x = -f b

Proof state:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [hasCompactSupport_iff_eventuallyEq, Filter.coclosedCompact_eq_cocompact] at h2f

Result:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Proof state:
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ ∫ (x : ℝ) in Ioi b, deriv f x = -f b

Tactic:
rw [integral_Ioi_of_hasDerivAt_of_tendsto hf.continuous.continuousWithinAt this, zero_sub]

Result:
case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Ioi b) volume

case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Proof state:
case f'int
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : HasCompactSupport f
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ IntegrableOn (deriv f) (Ioi b) volume

Tactic:
refine hf.continuous_deriv le_rfl |>.integrable_of_hasCompactSupport h2f.deriv |>.integrableOn

Result:
no goals

Proof state:
case hf
E : Type u_1
f : ℝ → E
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
hf : ContDiff ℝ 1 f
h2f : f =ᶠ[cocompact ℝ] 0
b : ℝ
this : ∀ x ∈ Ioi b, HasDerivAt f (deriv f x) x
⊢ Tendsto f atTop (𝓝 0)

Tactic:
exact h2f.filter_mono _root_.atTop_le_cocompact |>.tendsto

Result:
no goals
-- Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@[to_additive]
lemma IsCyclic.ext [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d}
    (hGcard : Nat.card G = d) (h : ∀ t : G, t ^ a.val = t ^ b.val) : a = b

Proof state:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b

Tactic:
simpa [ZMod.natCast_val, ZMod.cast_id'] using h

Result:
no goals

Proof state:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
⊢ a = b

Tactic:
have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩

Result:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
⊢ a = b

Proof state:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
h : g ^ a.val = g ^ b.val
⊢ a = b

Tactic:
subst hGcard

Result:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : g ^ a.val = g ^ b.val
⊢ a = b

Proof state:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
⊢ a = b

Tactic:
specialize h g

Result:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
h : g ^ a.val = g ^ b.val
⊢ a = b

Proof state:
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
⊢ a = b

Tactic:
obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)

Result:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
d : ℕ
a b : ZMod d
hGcard : Nat.card G = d
h : ∀ (t : G), t ^ a.val = t ^ b.val
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
⊢ a = b

Proof state:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : g ^ a.val = g ^ b.val
⊢ a = b

Tactic:
rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg,
  ← ZMod.natCast_eq_natCast_iff] at h

Result:
case intro
G : Type u_2
inst✝² : Group G
inst✝¹ : Finite G
inst✝ : IsCyclic G
this : NeZero (Nat.card G)
g : G
hg : ∀ (x : G), x ∈ zpowers g
a b : ZMod (Nat.card G)
h : ↑a.val = ↑b.val
⊢ a = b
-- Mathlib/Topology/Algebra/Group/Basic.lean
@[to_additive]
lemma IsCompact.mul_closure_one_eq_closure {K : Set G} (hK : IsCompact K) :
    K * (closure {1} : Set G) = closure K

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed (K * closure {1})
⊢ closure K ⊆ K * closure {1}

Tactic:
rw [IsClosed.closure_subset_iff this]

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed (K * closure {1})
⊢ K ⊆ K * closure {1}

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure {1} = closure K

Tactic:
apply Subset.antisymm ?_ ?_

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure {1} ⊆ closure K

G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure K ⊆ K * closure {1}

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed (K * closure {1})
⊢ K ⊆ K * closure {1}

Tactic:
exact subset_mul_closure_one K

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ K * closure {1} ⊆ closure K

Tactic:
calc
K * (closure {1} : Set G) ⊆ closure K * (closure {1} : Set G) :=
  smul_subset_smul_right subset_closure
_ ⊆ closure (K * ({1} : Set G)) := smul_set_closure_subset _ _
_ = closure K := by simp

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure (K * {1}) = closure K

Tactic:
simp

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
⊢ closure K ⊆ K * closure {1}

Tactic:
have : IsClosed (K * (closure {1} : Set G)) :=
  IsClosed.smul_left_of_isCompact isClosed_closure hK

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
K : Set G
hK : IsCompact K
this : IsClosed (K * closure {1})
⊢ closure K ⊆ K * closure {1}
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_top : withTopEquiv.symm ⊤ = ⊤

Proof state:
⊢ withTopEquiv.symm ⊤ = ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem insertMany_list_singleton {k : α} {v : β k} :
    m.insertMany [⟨k, v⟩] = m.insert k v

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝¹ : BEq α
inst✝ : Hashable α
k : α
v : β k
⊢ (m.insertMany [⟨k, v⟩]).val = m.insert k v

Tactic:
simp [insertMany, Id.run]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma polynomialZ_eq : W'.polynomialZ = C W'.a₁ * X 0 * X 1 + C (3 * W'.a₃) * X 1 * X 2 ^ 2 -
    (C (2 * W'.a₂) * X 0 ^ 2 * X 2 + C (4 * W'.a₄) * X 0 * X 2 ^ 3 + C (6 * W'.a₆) * X 2 ^ 5)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 1) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 1)) -
      (↑3 * X x ^ (3 - 1) * 0 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 1)) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 1)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 1))) =
    C W'.a₁ * X x * X y + 3 * C W'.a₃ * X y * X z ^ 2 -
      (2 * C W'.a₂ * X x ^ 2 * X z + 4 * C W'.a₄ * X x * X z ^ 3 + 6 * C W'.a₆ * X z ^ 5)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv z)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 -
      (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ ↑2 * X y ^ (2 - 1) * 0 + (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 0) * X z + C W'.a₁ * X x * X y * 1) +
        ((0 * X y + C W'.a₃ * 0) * X z ^ 3 + C W'.a₃ * X y * (↑3 * X z ^ (3 - 1) * 1)) -
      (↑3 * X x ^ (3 - 1) * 0 +
            ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z ^ 2 +
              C W'.a₂ * X x ^ 2 * (↑2 * X z ^ (2 - 1) * 1)) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 4 + C W'.a₄ * X x * (↑4 * X z ^ (4 - 1) * 1)) +
        (0 * X z ^ 6 + C W'.a₆ * (↑6 * X z ^ (6 - 1) * 1))) =
    C W'.a₁ * X x * X y + 3 * C W'.a₃ * X y * X z ^ 2 -
      (2 * C W'.a₂ * X x ^ 2 * X z + 4 * C W'.a₄ * X x * X z ^ 3 + 6 * C W'.a₆ * X z ^ 5)

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ W'.polynomialZ =
    C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 -
      (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)

Tactic:
rw [polynomialZ, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
⊢ (pderiv z)
      (X y ^ 2 + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 3 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z ^ 2 + C W'.a₄ * X x * X z ^ 4 + C W'.a₆ * X z ^ 6)) =
    C W'.a₁ * X x * X y + C (3 * W'.a₃) * X y * X z ^ 2 -
      (C (2 * W'.a₂) * X x ^ 2 * X z + C (4 * W'.a₄) * X x * X z ^ 3 + C (6 * W'.a₆) * X z ^ 5)
-- Mathlib/Analysis/SpecialFunctions/OrdinaryHypergeometric.lean
theorem ordinaryHypergeometric_zero : ₂F₁ a b c (0 : 𝔸) = 1

Proof state:
𝕂 : Type u_1
𝔸 : Type u_2
inst✝⁴ : Field 𝕂
inst✝³ : Ring 𝔸
inst✝² : Algebra 𝕂 𝔸
inst✝¹ : TopologicalSpace 𝔸
inst✝ : IsTopologicalRing 𝔸
a b c : 𝕂
⊢ ₂F₁ a b c 0 = 1

Tactic:
simp [ordinaryHypergeometric_eq_tsum, ← ordinaryHypergeometricSeries_apply_eq,
  ordinaryHypergeometricSeries_apply_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsb?_eq_getLsb? (x : BitVec w) (i : Nat) :
    x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ (if h : i < w then some (x.getMsb' ⟨i, h⟩) else none) = if i < w then x[w - 1 - i]? else none

Tactic:
split <;> simp [getMsb'_eq_getLsb']

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Nat
⊢ x.getMsb? i = if i < w then x.getLsb? (w - 1 - i) else none

Tactic:
simp only [getMsb?, getLsb?_eq_getElem?]

Result:
w : Nat
x : BitVec w
i : Nat
⊢ (if h : i < w then some (x.getMsb' ⟨i, h⟩) else none) = if i < w then x[w - 1 - i]? else none
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
lemma hasSum_qExpansion [NeZero n] [ModularFormClass F Γ(n) k] (τ : ℍ) :
    HasSum (fun m : ℕ ↦ (qExpansion n f).coeff ℂ m • 𝕢 n τ ^ m) (f τ)

Proof state:
k : ℤ
F : Type u_1
inst✝² : FunLike F ℍ ℂ
n : ℕ
f : F
inst✝¹ : NeZero n
inst✝ : ModularFormClass F Γ(n) k
τ : ℍ
⊢ HasSum (fun m => (PowerSeries.coeff ℂ m) (qExpansion n f) • 𝕢 ↑n ↑τ ^ m) (f τ)

Tactic:
simpa only [eq_cuspFunction n f] using
  hasSum_qExpansion_of_abs_lt n f (τ.norm_qParam_lt_one n)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_getElem : ∀ (l : List α) (h : l ≠ []),
    getLast l h = l[l.length - 1]'(by
      match l with
      | [] => contradiction
      | a :: l => exact Nat.le_refl _)
  | [_], _ => rfl
  | _ :: _ :: _, _ => by
    simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]

Proof state:
α : Type ?u.92859
l : List α
h : l ≠ []
⊢ l.length - 1 < l.length

Tactic:
match l with
| [] => contradiction
| a :: l => exact Nat.le_refl _

Result:
no goals

Proof state:
α : Type ?u.92859
l✝ : List α
a : α
l : List α
h : a :: l ≠ []
⊢ (a :: l).length - 1 < (a :: l).length

Tactic:
exact Nat.le_refl _

Result:
no goals

Proof state:
α : Type ?u.92859
l : List α
h : [] ≠ []
⊢ [].length - 1 < [].length

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
head✝¹ head✝ : α
tail✝ : List α
x✝ : head✝¹ :: head✝ :: tail✝ ≠ []
⊢ (head✝¹ :: head✝ :: tail✝).getLast x✝ = (head✝¹ :: head✝ :: tail✝)[(head✝¹ :: head✝ :: tail✝).length - 1]

Tactic:
simp [getLast, get, Nat.succ_sub_succ, getLast_eq_getElem]

Result:
no goals