harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma isoOfIsAffine_hom_appTop [IsAffine S] :
    (isoOfIsAffine n S).hom.appTop =
      (Scheme.ΓSpecIso _).hom ≫ CommRingCat.ofHom
        (eval₂Hom ((𝔸(n; S) ↘ S).appTop).hom (coord S))

Proof state:
n : Type v
S : Scheme
inst✝ : IsAffine S
⊢ Scheme.Hom.appTop (isoOfIsAffine n S).hom =
    (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑Γ(S, ⊤)))).hom ≫
      CommRingCat.ofHom (eval₂Hom (CommRingCat.Hom.hom (Scheme.Hom.appTop (𝔸(n; S) ↘ S))) (coord S))

Tactic:
simp [isoOfIsAffine_hom]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem SeminormFamily.withSeminorms_iff_uniformSpace_eq_iInf [u : UniformSpace E]
    [UniformAddGroup E] (p : SeminormFamily 𝕜 E ι) :
    WithSeminorms p ↔ u = ⨅ i, (p i).toSeminormedAddCommGroup.toUniformSpace

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0

Tactic:
congrm _ = ⨅ i, ?_

Result:
case a
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0

Proof state:
case a
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
i : ι
⊢ comap (⇑(p i)) (𝓝 0) = 𝓝 0

Tactic:
exact @comap_norm_nhds_zero _ (p i).toAddGroupSeminorm.toSeminormedAddGroup

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ WithSeminorms p ↔ u = ⨅ i, PseudoMetricSpace.toUniformSpace

Tactic:
rw [p.withSeminorms_iff_nhds_eq_iInf,
  UniformAddGroup.ext_iff inferInstance (uniformAddGroup_iInf fun i => inferInstance),
  UniformSpace.toTopologicalSpace_iInf, nhds_iInf]

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝⁴ : NormedField 𝕜
inst✝³ : AddCommGroup E
inst✝² : Module 𝕜 E
inst✝¹ : Nonempty ι
u : UniformSpace E
inst✝ : UniformAddGroup E
p : SeminormFamily 𝕜 E ι
⊢ 𝓝 0 = ⨅ i, comap (⇑(p i)) (𝓝 0) ↔ 𝓝 0 = ⨅ i, 𝓝 0
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_eq_neg_pi_div_two_iff {z : ℂ} : arg z = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Proof state:
case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Tactic:
obtain ⟨x, y⟩ := z

Result:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → { re := x, im := y }.arg = -(π / 2)

Proof state:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
simp [h₀, lt_irrefl, Real.pi_ne_zero]

Result:
no goals

Proof state:
z : ℂ
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
by_cases h₀ : z = 0

Result:
case pos
z : ℂ
h₀ : z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0

Tactic:
intro h

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0

Proof state:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg

Tactic:
simp

Result:
no goals

Proof state:
case neg
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) ↔ z.re = 0 ∧ z.im < 0

Tactic:
constructor

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
⊢ z.arg = -(π / 2) → z.re = 0 ∧ z.im < 0

case neg.mpr
z : ℂ
h₀ : ¬z = 0
⊢ z.re = 0 ∧ z.im < 0 → z.arg = -(π / 2)

Proof state:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = -(π / 2)

Tactic:
rw [← arg_neg_I, ← arg_real_mul (-I) (neg_pos.2 hy), mk_eq_add_mul_I]

Result:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ (↑0 + ↑y * I).arg = (↑(-y) * -I).arg

Proof state:
case neg.mpr.mk
x y : ℝ
h₀ : ¬{ re := x, im := y } = 0
⊢ { re := x, im := y }.re = 0 ∧ { re := x, im := y }.im < 0 → { re := x, im := y }.arg = -(π / 2)

Tactic:
rintro ⟨rfl : x = 0, hy : y < 0⟩

Result:
case neg.mpr.mk.intro
y : ℝ
h₀ : ¬{ re := 0, im := y } = 0
hy : y < 0
⊢ { re := 0, im := y }.arg = -(π / 2)

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0

Tactic:
simp [h₀]

Result:
no goals

Proof state:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ z.re = 0 ∧ z.im < 0

Tactic:
rw [← norm_mul_cos_add_sin_mul_I z, h]

Result:
case neg.mp
z : ℂ
h₀ : ¬z = 0
h : z.arg = -(π / 2)
⊢ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).re = 0 ∧ (↑‖z‖ * (cos ↑(-(π / 2)) + sin ↑(-(π / 2)) * I)).im < 0
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem cycleType_eq_zero {σ : Perm α} : σ.cycleType = 0 ↔ σ = 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ σ.cycleType = 0 ↔ σ = 1

Tactic:
simp [cycleType_def, cycleFactorsFinset_eq_empty_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
    aig.decls.size ≤ (go aig input).aig.decls.size

Proof state:
case h_2.h_3
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝⁴ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝³ x✝² : Decl α
linv✝ rinv✝ : Bool
heq✝¹ : aig.decls[input.rhs.ref.gate] = Decl.const true
heq✝ : input.rhs.inv = true
x✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
⊢ aig.decls.size ≤ ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls.size

Tactic:
simp_arith [mkConstCached_le_size]

Result:
no goals

Proof state:
case h_2.h_1
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝² : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝¹ x✝ : Decl α
linv✝ rinv✝ : Bool
heq✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const true
heq✝ : input.lhs.inv = true
⊢ aig.decls.size ≤ ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls.size

Tactic:
simp_arith [mkConstCached_le_size]

Result:
no goals

Proof state:
case h_2.h_2
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝² : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝² : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝¹ x✝ : Decl α
linv✝ rinv✝ : Bool
heq✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false
heq✝ : input.lhs.inv = false
⊢ aig.decls.size ≤ ({ decls := aig.decls, cache := aig.cache, invariant := ⋯ }.mkConstCached false).aig.decls.size

Tactic:
simp_arith [mkConstCached_le_size]

Result:
no goals

Proof state:
case h_2.h_7
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝⁴ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝³ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝³ x✝² : Decl α
linv✝ rinv✝ : Bool
heq✝² : aig.decls[input.rhs.ref.gate] = Decl.const true
heq✝¹ : input.lhs.inv = false
heq✝ : input.rhs.inv = false
x✝¹ : aig.decls[input.lhs.ref.gate] = Decl.const false → False
x✝ : aig.decls[input.lhs.ref.gate] = Decl.const true → False
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ },
            ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }.aig.decls.size

Tactic:
simp_arith

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkGateCached.go_le_size (aig : AIG α) (input : GateInput aig) :
    aig.decls.size ≤ (go aig input).aig.decls.size

Proof state:
case h_2.h_9.isTrue
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
input : aig.GateInput
x✝¹⁰ : Option (CacheHit aig.decls (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv))
heq✝ : aig.cache.get? (Decl.gate input.lhs.ref.gate input.rhs.ref.gate input.lhs.inv input.rhs.inv) = none
x✝⁹ x✝⁸ : Decl α
linv✝ rinv✝ : Bool
x✝⁷ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = true → False
x✝⁶ : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = false → False
x✝⁵ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.rhs.inv = true → False
x✝⁴ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.rhs.inv = false → False
x✝³ : aig.decls[input.lhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝² : aig.decls[input.lhs.ref.gate] = Decl.const false → input.lhs.inv = true → input.rhs.inv = false → False
x✝¹ : aig.decls[input.rhs.ref.gate] = Decl.const true → input.lhs.inv = false → input.rhs.inv = false → False
x✝ : aig.decls[input.rhs.ref.gate] = Decl.const false → input.lhs.inv = false → input.rhs.inv = true → False
h✝ : (input.lhs.ref.gate == input.rhs.ref.gate && input.lhs.inv == false && input.rhs.inv == false) = true
⊢ aig.decls.size ≤
    { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ },
            ref := { gate := input.lhs.ref.gate, hgate := ⋯ } }.aig.decls.size

Tactic:
simp_arith

Result:
no goals
-- Mathlib/Data/Complex/ExponentialBounds.lean
theorem exp_neg_one_lt_d9 : exp (-1) < 0.3678794412

Proof state:
⊢ 0.3678794412⁻¹ < rexp 1

Tactic:
exact lt_of_lt_of_le (by norm_num) (sub_le_comm.1 (abs_sub_le_iff.1 exp_one_near_10).2)

Result:
no goals

Proof state:
⊢ 0 < 0.3678794412

Tactic:
norm_num

Result:
no goals

Proof state:
⊢ rexp (-1) < 0.3678794412

Tactic:
rw [exp_neg, inv_lt_comm₀ (exp_pos _) (by norm_num)]

Result:
⊢ 0.3678794412⁻¹ < rexp 1

Proof state:
⊢ 0.3678794412⁻¹ < 2244083 / 825552 - 1 / 10 ^ 10

Tactic:
norm_num

Result:
no goals
-- Mathlib/Analysis/Analytic/ChangeOrigin.lean
theorem changeOriginSeries_summable_aux₁ {r r' : ℝ≥0} (hr : (r + r' : ℝ≥0∞) < p.radius) :
    Summable fun s : Σk l : ℕ, { s : Finset (Fin (k + l)) // s.card = l } =>
      ‖p (s.1 + s.2.1)‖₊ * r ^ s.2.1 * r' ^ s.1

Proof state:
case h.e'_5.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
s : Finset (Fin n)
⊢ ‖p (n - s.card + s.card)‖₊ * r ^ s.card * r' ^ (n - s.card) = ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))

Tactic:
rw [tsub_add_cancel_of_le (card_finset_fin_le _), mul_assoc]

Result:
no goals

Proof state:
case convert_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card))) (‖p n‖₊ * (r + r') ^ n)

Tactic:
rw [← Fin.sum_pow_mul_eq_add_pow]

Result:
case convert_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r r' : ℝ≥0
hr : ↑r + ↑r' < p.radius
n : ℕ
⊢ HasSum (fun s => ‖p n‖₊ * (r ^ s.card * r' ^ (n - s.card)))
    (‖p n‖₊ * ∑ s : Finset (Fin n), r ^ s.card * r' ^ (n - s.card))
-- Mathlib/Algebra/Algebra/Bilinear.lean
theorem pow_mulLeft (a : A) (n : ℕ) : mulLeft R a ^ n = mulLeft R (a ^ n) :=
  match n with
  | 0 => by rw [pow_zero, pow_zero, mulLeft_one, LinearMap.one_eq_id]
  | (n + 1) => by rw [pow_succ, pow_succ, mulLeft_mul, LinearMap.mul_eq_comp, pow_mulLeft]

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n✝ n : ℕ
⊢ mulLeft R a ^ (n + 1) = mulLeft R (a ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, mulLeft_mul, LinearMap.mul_eq_comp, pow_mulLeft]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : Semiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : SMulCommClass R A A
a : A
n : ℕ
⊢ mulLeft R a ^ 0 = mulLeft R (a ^ 0)

Tactic:
rw [pow_zero, pow_zero, mulLeft_one, LinearMap.one_eq_id]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/StoneWeierstrass.lean
theorem ContinuousMap.starAlgHom_ext_map_X {𝕜 A : Type*} [RCLike 𝕜] [Ring A] [StarRing A]
    [Algebra 𝕜 A] [TopologicalSpace A] [T2Space A] {s : Set 𝕜} [CompactSpace s]
    {φ ψ : C(s, 𝕜) →⋆ₐ[𝕜] A} (hφ : Continuous φ) (hψ : Continuous ψ)
    (h : φ (toContinuousMapOnAlgHom s X) = ψ (toContinuousMapOnAlgHom s X)) : φ = ψ

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set 𝕜
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ ⊤ ≤ StarAlgHom.equalizer φ ψ

Tactic:
rw [← polynomialFunctions.starClosure_topologicalClosure s]

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set 𝕜
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).starClosure.topologicalClosure ≤ StarAlgHom.equalizer φ ψ

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set 𝕜
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ φ = ψ

Tactic:
suffices (⊤ : StarSubalgebra 𝕜 C(s, 𝕜)) ≤ StarAlgHom.equalizer φ ψ from
  StarAlgHom.ext fun x => this mem_top

Result:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set 𝕜
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ ⊤ ≤ StarAlgHom.equalizer φ ψ

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝⁶ : RCLike 𝕜
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : Algebra 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : T2Space A
s : Set 𝕜
inst✝ : CompactSpace ↑s
φ ψ : C(↑s, 𝕜) →⋆ₐ[𝕜] A
hφ : Continuous ⇑φ
hψ : Continuous ⇑ψ
h : φ ((toContinuousMapOnAlgHom s) X) = ψ ((toContinuousMapOnAlgHom s) X)
⊢ (polynomialFunctions s).starClosure.topologicalClosure ≤ StarAlgHom.equalizer φ ψ

Tactic:
exact StarSubalgebra.topologicalClosure_minimal
  (polynomialFunctions.starClosure_le_equalizer s φ ψ h) (isClosed_eq hφ hψ)

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
/-- Powers of analytic functions (into a normed `𝕜`-algebra) are analytic. -/
lemma AnalyticWithinAt.pow {f : E → A} {z : E} {s : Set E} (hf : AnalyticWithinAt 𝕜 f s z) (n : ℕ) :
    AnalyticWithinAt 𝕜 (fun x ↦ f x ^ n) s z

Proof state:
case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (fun x => f x ^ m) s z
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ m * f x) s z

Tactic:
exact hm.mul hf

Result:
no goals

Proof state:
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
n : ℕ
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ n) s z

Tactic:
induction n with
| zero =>
  simp only [pow_zero]
  apply analyticWithinAt_const
| succ m hm =>
  simp only [pow_succ]
  exact hm.mul hf

Result:
no goals

Proof state:
case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (fun x => f x ^ m) s z
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ (m + 1)) s z

Tactic:
simp only [pow_succ]

Result:
case succ
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
m : ℕ
hm : AnalyticWithinAt 𝕜 (fun x => f x ^ m) s z
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ m * f x) s z

Proof state:
case zero
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt 𝕜 (fun x => f x ^ 0) s z

Tactic:
simp only [pow_zero]

Result:
case zero
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt 𝕜 (fun x => 1) s z

Proof state:
case zero
𝕜 : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
A : Type u_8
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra 𝕜 A
f : E → A
z : E
s : Set E
hf : AnalyticWithinAt 𝕜 f s z
⊢ AnalyticWithinAt 𝕜 (fun x => 1) s z

Tactic:
apply analyticWithinAt_const

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
theorem modByMonic_X (p : R[X]) : p %ₘ X = C (p.eval 0)

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
⊢ p %ₘ X = C (eval 0 p)

Tactic:
rw [← modByMonic_X_sub_C_eq_C_eval, C_0, sub_zero]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem isAdjointPair_inner (A : E →L[𝕜] F) :
    LinearMap.IsAdjointPair (sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜)
      (sesqFormOfInner : F →ₗ[𝕜] F →ₗ⋆[𝕜] 𝕜) A (A†)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
y : F
⊢ (sesqFormOfInner (A x)) y = (sesqFormOfInner x) ((adjoint A) y)

Tactic:
simp only [sesqFormOfInner_apply_apply, adjoint_inner_left, coe_coe]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
⊢ sesqFormOfInner.IsAdjointPair sesqFormOfInner ⇑A ⇑(adjoint A)

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
x : E
y : F
⊢ (sesqFormOfInner (A x)) y = (sesqFormOfInner x) ((adjoint A) y)
-- Mathlib/NumberTheory/LSeries/PrimesInAP.lean
theorem forall_exists_prime_gt_and_eq_mod (ha : IsUnit a) (n : ℕ) :
    ∃ p > n, p.Prime ∧ (p : ZMod q) = a

Proof state:
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
n : ℕ
⊢ ∃ p > n, Prime p ∧ ↑p = a

Tactic:
obtain ⟨p, hp₁, hp₂⟩ := Set.infinite_iff_exists_gt.mp (setOf_prime_and_eq_mod_infinite ha) n

Result:
case intro.intro
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
n p : ℕ
hp₁ : p ∈ {p | Prime p ∧ ↑p = a}
hp₂ : n < p
⊢ ∃ p > n, Prime p ∧ ↑p = a

Proof state:
case intro.intro
q : ℕ
inst✝ : NeZero q
a : ZMod q
ha : IsUnit a
n p : ℕ
hp₁ : p ∈ {p | Prime p ∧ ↑p = a}
hp₂ : n < p
⊢ ∃ p > n, Prime p ∧ ↑p = a

Tactic:
exact ⟨p, hp₂.gt, Set.mem_setOf.mp hp₁⟩

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_X_pow {n : ℕ} : (X ^ n : F[X]).natSepDegree = if n = 0 then 0 else 1

Proof state:
F : Type u
inst✝ : Field F
n : ℕ
⊢ (X ^ n).natSepDegree = if n = 0 then 0 else 1

Tactic:
simp only [natSepDegree_pow, natSepDegree_X]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem findFinIdx?_cons {p : α → Bool} {x : α} {xs : List α} :
    findFinIdx? p (x :: xs) = if p x then some 0 else (findFinIdx? p xs).map Fin.succ

Proof state:
case isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) = Option.map Fin.val (Option.map Fin.succ (findFinIdx? p xs))

Tactic:
rw [findIdx?_eq_map_findFinIdx?_val]

Result:
case isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (Option.map (fun x => ↑x) (findFinIdx? p xs)) =
    Option.map Fin.val (Option.map Fin.succ (findFinIdx? p xs))

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ Option.map Fin.val (findFinIdx? p (x :: xs)) =
    Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))

Tactic:
rw [← findIdx?_eq_map_findFinIdx?_val]

Result:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ findIdx? p (x :: xs) = Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ findIdx? p (x :: xs) = Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))

Tactic:
rw [findIdx?_cons]

Result:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) =
    Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))

Proof state:
case isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : p x = true
⊢ some 0 = Option.map Fin.val (some 0)

Tactic:
simp

Result:
no goals

Proof state:
case isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (Option.map (fun x => ↑x) (findFinIdx? p xs)) =
    Option.map Fin.val (Option.map Fin.succ (findFinIdx? p xs))

Tactic:
simp [Function.comp_def]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ (if p x = true then some 0 else Option.map (fun i => i + 1) (findIdx? p xs)) =
    Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))

Tactic:
split

Result:
case isTrue
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : p x = true
⊢ some 0 = Option.map Fin.val (some 0)

case isFalse
α : Type u_1
p : α → Bool
x : α
xs : List α
h✝ : ¬p x = true
⊢ Option.map (fun i => i + 1) (findIdx? p xs) = Option.map Fin.val (Option.map Fin.succ (findFinIdx? p xs))

Proof state:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ findFinIdx? p (x :: xs) = if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs)

Tactic:
rw [← Option.map_inj_right (f := Fin.val) (fun a b => Fin.eq_of_val_eq)]

Result:
α : Type u_1
p : α → Bool
x : α
xs : List α
⊢ Option.map Fin.val (findFinIdx? p (x :: xs)) =
    Option.map Fin.val (if p x = true then some 0 else Option.map Fin.succ (findFinIdx? p xs))