harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/Trunc.lean
theorem trunc'_C (n : σ →₀ ℕ) (a : R) :
    trunc' R n (C σ R a) = MvPolynomial.C a :=
  MvPolynomial.ext _ _ fun m ↦ by
    classical
    rw [coeff_trunc', coeff_C, MvPolynomial.coeff_C]
    split_ifs with H <;> first |rfl|try simp_all
    exfalso; apply H; subst m; exact orderBot.proof_1 n

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ False

Tactic:
apply H

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ m ≤ n

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
H : ¬0 ≤ n
⊢ 0 ≤ n

Tactic:
exact orderBot.proof_1 n

Result:
no goals

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a

Tactic:
exfalso

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ False

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ m ≤ n

Tactic:
subst m

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
H : ¬0 ≤ n
⊢ 0 ≤ n

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a

Tactic:
simp_all

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)

Tactic:
classical
rw [coeff_trunc', coeff_C, MvPolynomial.coeff_C]
split_ifs with H <;> first |rfl|try simp_all
exfalso; apply H; subst m; exact orderBot.proof_1 n

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ MvPolynomial.coeff m ((trunc' R n) ((C σ R) a)) = MvPolynomial.coeff m (MvPolynomial.C a)

Tactic:
rw [coeff_trunc', coeff_C, MvPolynomial.coeff_C]

Result:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : m ≤ n
h✝¹ : ¬m = 0
h✝ : 0 = m
⊢ 0 = a

Tactic:
try simp_all

Result:
no goals

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : ¬0 = m
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
⊢ (if m ≤ n then if m = 0 then a else 0 else 0) = if 0 = m then a else 0

Tactic:
split_ifs with H <;> first |rfl|try simp_all

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
n : σ →₀ ℕ
a : R
m : σ →₀ ℕ
H : ¬m ≤ n
h✝ : 0 = m
⊢ 0 = a
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
protected lemma add_comp {n₁ n₂ n₁₂ : ℤ} (z₁ z₁' : Cochain F G n₁) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂) : (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁ + z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h + z₁'.comp z₂ h).v p q hpq

Tactic:
simp only [comp_v _ _ h p _ q rfl (by omega), add_v, add_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ (z₁ + z₁').comp z₂ h = z₁.comp z₂ h + z₁'.comp z₂ h

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ ((z₁ + z₁').comp z₂ h).v p q hpq = (z₁.comp z₂ h + z₁'.comp z₂ h).v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ z₁' : Cochain F G n₁
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
p q : ℤ
hpq : p + n₁₂ = q
⊢ p + n₁ + n₂ = q

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Span.lean
theorem toSpanUnitSingleton_apply (x : E) (hx : ‖x‖ = 1) (r : 𝕜) :
    toSpanUnitSingleton x hx r = (⟨r • x, by aesop⟩ : 𝕜 ∙ x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
hx : ‖x‖ = 1
r : 𝕜
⊢ (toSpanUnitSingleton x hx) r = ⟨r • x, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : NormedDivisionRing 𝕜
inst✝² : SeminormedAddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
x : E
hx : ‖x‖ = 1
r : 𝕜
⊢ r • x ∈ Submodule.span 𝕜 {x}

Tactic:
aesop

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem round_eq_zero_iff {x : α} : round x = 0 ↔ x ∈ Ico (-(1 / 2)) ((1 : α) / 2)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ round x = 0 ↔ x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
rw [round_eq, floor_eq_zero_iff, add_mem_Ico_iff_left]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x ∈ Ico (0 - 1 / 2) (1 - 1 / 2) ↔ x ∈ Ico (-(1 / 2)) (1 / 2)

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x ∈ Ico (0 - 1 / 2) (1 - 1 / 2) ↔ x ∈ Ico (-(1 / 2)) (1 / 2)

Tactic:
norm_num

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNorm.lean
theorem mul (q r : ℚ) : padicNorm p (q * r) = padicNorm p q * padicNorm p r :=
  if hq : q = 0 then by simp [hq]
  else
    if hr : r = 0 then by simp [hr]
    else by
      have : (p : ℚ) ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hr]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
have : (p : ℚ) ≠ 0 := by simp [hp.1.ne_zero]

Result:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : ↑p ≠ 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : q = 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [hq]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
⊢ ↑p ≠ 0

Tactic:
simp [hp.1.ne_zero]

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ
hq : ¬q = 0
hr : ¬r = 0
this : ↑p ≠ 0
⊢ padicNorm p (q * r) = padicNorm p q * padicNorm p r

Tactic:
simp [padicNorm, *, padicValRat.mul, zpow_add₀ this, mul_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem hasProd_one : HasProd (fun _ ↦ 1 : β → α) 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
⊢ HasProd (fun x => 1) 1

Tactic:
simp [HasProd, tendsto_const_nhds]

Result:
no goals
-- Mathlib/Topology/Compactness/LocallyCompact.lean
/-- If `f : X → Y` is a continuous map in a locally compact pair of topological spaces,
`K : set X` is a compact set, and `U` is an open neighbourhood of `f '' K`,
then there exists a compact neighbourhood `L` of `K` such that `f` maps `L` to `U`.

This is a generalization of `exists_mem_nhds_isCompact_mapsTo`. -/
lemma exists_mem_nhdsSet_isCompact_mapsTo [LocallyCompactPair X Y] {f : X → Y} {K : Set X}
    {U : Set Y} (hf : Continuous f) (hK : IsCompact K) (hU : IsOpen U) (hKU : MapsTo f K U) :
    ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous f
hK : IsCompact K
hU : IsOpen U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
exact ⟨_, hKs, s.isCompact_biUnion fun x hx ↦ hVc x (hsK x hx), mapsTo_iUnion₂.2 fun x hx ↦
  hVU x (hsK x hx)⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous f
hK : IsCompact K
hU : IsOpen U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
rcases hK.elim_nhds_subcover_nhdsSet hxV with ⟨s, hsK, hKs⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous f
hK : IsCompact K
hU : IsOpen U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
s : Finset X
hsK : ∀ x ∈ s, x ∈ K
hKs : ⋃ x ∈ s, V x ∈ 𝓝ˢ K
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous f
hK : IsCompact K
hU : IsOpen U
hKU : MapsTo f K U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U

Tactic:
choose! V hxV hVc hVU using fun x (hx : x ∈ K) ↦
  exists_mem_nhds_isCompact_mapsTo hf (hU.mem_nhds (hKU hx))

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : LocallyCompactPair X Y
f : X → Y
K : Set X
U : Set Y
hf : Continuous f
hK : IsCompact K
hU : IsOpen U
hKU : MapsTo f K U
V : X → Set X
hxV : ∀ x ∈ K, V x ∈ 𝓝 x
hVc : ∀ x ∈ K, IsCompact (V x)
hVU : ∀ x ∈ K, MapsTo f (V x) U
⊢ ∃ L ∈ 𝓝ˢ K, IsCompact L ∧ MapsTo f L U
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem IsPrefix.eraseIdx {l l' : List α} (h : l <+: l') (k : Nat) :
    eraseIdx l k <+: eraseIdx l' k

Proof state:
α : Type u_1
l : List α
k : Nat
t : List α
hkl : k < l.length
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k

Tactic:
simp [eraseIdx_append_of_lt_length hkl]

Result:
no goals

Proof state:
case intro
α : Type u_1
l : List α
k : Nat
t : List α
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k

Tactic:
if hkl : k < length l then
  simp [eraseIdx_append_of_lt_length hkl]
else
  rw [Nat.not_lt] at hkl
  simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]

Result:
no goals

Proof state:
α : Type u_1
l : List α
k : Nat
t : List α
hkl : l.length ≤ k
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k

Tactic:
simp [eraseIdx_append_of_length_le hkl, eraseIdx_of_length_le hkl]

Result:
no goals

Proof state:
α : Type u_1
l : List α
k : Nat
t : List α
hkl : ¬k < l.length
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k

Tactic:
rw [Nat.not_lt] at hkl

Result:
α : Type u_1
l : List α
k : Nat
t : List α
hkl : l.length ≤ k
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k

Proof state:
α : Type u_1
l l' : List α
h : l <+: l'
k : Nat
⊢ l.eraseIdx k <+: l'.eraseIdx k

Tactic:
rcases h with ⟨t, rfl⟩

Result:
case intro
α : Type u_1
l : List α
k : Nat
t : List α
⊢ l.eraseIdx k <+: (l ++ t).eraseIdx k
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
theorem getLast_support {G : SimpleGraph V} {a b : V} (p : G.Walk a b) :
    p.support.getLast (by simp) = b

Proof state:
case cons
V : Type u
G : SimpleGraph V
a b u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.getLast ⋯ = w✝
⊢ (cons h✝ p✝).support.getLast ⋯ = w✝

Tactic:
simpa

Result:
no goals

Proof state:
case nil
V : Type u
G : SimpleGraph V
a b u✝ : V
⊢ nil.support.getLast ⋯ = u✝

Tactic:
simp

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support.getLast ⋯ = b

Tactic:
induction p

Result:
case nil
V : Type u
G : SimpleGraph V
a b u✝ : V
⊢ nil.support.getLast ⋯ = u✝

case cons
V : Type u
G : SimpleGraph V
a b u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : p✝.support.getLast ⋯ = w✝
⊢ (cons h✝ p✝).support.getLast ⋯ = w✝

Proof state:
V : Type u
V' : Type v
V'' : Type w
G✝ : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
G : SimpleGraph V
a b : V
p : G.Walk a b
⊢ p.support ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformlyOn_sUnion (S : Set (Set α)) (hS : ∀ s ∈ S, IsOpen s)
    (h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s) : TendstoLocallyUniformlyOn F f p (⋃₀ S)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃₀ S)

Tactic:
rw [sUnion_eq_biUnion]

Result:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
S : Set (Set α)
hS : ∀ s ∈ S, IsOpen s
h : ∀ s ∈ S, TendstoLocallyUniformlyOn F f p s
⊢ TendstoLocallyUniformlyOn F f p (⋃ i ∈ S, i)

Tactic:
exact tendstoLocallyUniformlyOn_biUnion hS h

Result:
no goals
-- Mathlib/Order/Filter/ZeroAndBoundedAtFilter.lean
theorem BoundedAtFilter.mul [SeminormedRing β] {l : Filter α} {f g : α → β}
    (hf : BoundedAtFilter l f) (hg : BoundedAtFilter l g) : BoundedAtFilter l (f * g)

Proof state:
case h.e'_8.h
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
x✝ : α
⊢ 1 x✝ = 1 x✝ * 1 x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ l.BoundedAtFilter (f * g)

Tactic:
refine (hf.mul hg).trans ?_

Result:
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ (fun x => 1 x * 1 x) =O[l] 1

Proof state:
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
⊢ (fun x => 1 x * 1 x) =O[l] 1

Tactic:
convert Asymptotics.isBigO_refl (E := ℝ) _ l

Result:
case h.e'_8.h
α : Type u_2
β : Type u_3
inst✝ : SeminormedRing β
l : Filter α
f g : α → β
hf : l.BoundedAtFilter f
hg : l.BoundedAtFilter g
x✝ : α
⊢ 1 x✝ = 1 x✝ * 1 x✝
-- Mathlib/FieldTheory/Galois/Profinite.lean
lemma algEquivToLimit_continuous : Continuous (algEquivToLimit k K)

Proof state:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ Continuous fun a => (Subtype.val ∘ ⇑(algEquivToLimit k K)) a L

Tactic:
convert restrictNormalHom_continuous L.unop.1

Result:
case h.e'_4.h
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2✝ :
  ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop =
    (↥(unop L).toIntermediateField ≃ₐ[k] ↥(unop L).toIntermediateField)
⊢ ((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop.str = krullTopology k ↥(unop L).toIntermediateField

Proof state:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ Continuous ⇑(algEquivToLimit k K)

Tactic:
rw [continuous_induced_rng]

Result:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ Continuous (Subtype.val ∘ ⇑(algEquivToLimit k K))

Proof state:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
⊢ Continuous (Subtype.val ∘ ⇑(algEquivToLimit k K))

Tactic:
refine continuous_pi (fun L ↦ ?_)

Result:
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
⊢ Continuous fun a => (Subtype.val ∘ ⇑(algEquivToLimit k K)) a L

Proof state:
case h.e'_4.h
k : Type u_3
K : Type u_4
inst✝² : Field k
inst✝¹ : Field K
inst✝ : Algebra k K
L : (FiniteGaloisIntermediateField k K)ᵒᵖ
e_2✝ :
  ↑((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop =
    (↥(unop L).toIntermediateField ≃ₐ[k] ↥(unop L).toIntermediateField)
⊢ ((asProfiniteGaloisGroupFunctor k K).obj L).toProfinite.toTop.str = krullTopology k ↥(unop L).toIntermediateField

Tactic:
exact (DiscreteTopology.eq_bot (α := L.unop ≃ₐ[k] L.unop)).symm

Result:
no goals
-- Mathlib/Topology/Instances/AddCircle.lean
theorem addOrderOf_div_of_gcd_eq_one' {m : ℤ} {n : ℕ} (hn : 0 < n) (h : m.natAbs.gcd n = 1) :
    addOrderOf (↑(↑m / ↑n * p) : AddCircle p) = n

Proof state:
case negSucc
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n

Tactic:
exact addOrderOf_div_of_gcd_eq_one hn h

Result:
no goals

Proof state:
case negSucc
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n

Tactic:
simp only [Int.cast_negSucc, neg_div, neg_mul, coe_neg, addOrderOf_neg]

Result:
case negSucc
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(a✝ + 1) / ↑n * p) = n

Proof state:
case ofNat
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : a✝.gcd n = 1
⊢ addOrderOf ↑(↑a✝ / ↑n * p) = n

Tactic:
exact addOrderOf_div_of_gcd_eq_one hn h

Result:
no goals

Proof state:
case ofNat
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.ofNat a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n

Tactic:
simp only [Int.ofNat_eq_coe, Int.cast_natCast, Int.natAbs_ofNat] at h ⊢

Result:
case ofNat
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : a✝.gcd n = 1
⊢ addOrderOf ↑(↑a✝ / ↑n * p) = n

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
m : ℤ
n : ℕ
hn : 0 < n
h : m.natAbs.gcd n = 1
⊢ addOrderOf ↑(↑m / ↑n * p) = n

Tactic:
cases m

Result:
case ofNat
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.ofNat a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.ofNat a✝) / ↑n * p) = n

case negSucc
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
p : 𝕜
hp : Fact (0 < p)
n : ℕ
hn : 0 < n
a✝ : ℕ
h : (Int.negSucc a✝).natAbs.gcd n = 1
⊢ addOrderOf ↑(↑(Int.negSucc a✝) / ↑n * p) = n
-- Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean
private lemma antilipschitzWith_card_equiv_pi_aux :
    AntilipschitzWith (Fintype.card ι) (equiv (Π i, E i)) :=
  AddMonoidHomClass.antilipschitz_of_bound (linearEquiv ℂ (Π i, E i)) fun x ↦ by
    simp only [NNReal.coe_natCast, linearEquiv_apply]
    calc ‖x‖ ≤ ∑ i, ‖x i‖ := pi_norm_le_sum_norm x
      _ ≤ ∑ _, ‖⇑x‖ := Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..
      _ ≤ Fintype.card ι * ‖⇑x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ∑ x_1 : ι, ‖(equiv ((i : ι) → E i)) x‖ ≤ ↑(Fintype.card ι) * ‖(equiv ((i : ι) → E i)) x‖

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ≤ ↑↑(Fintype.card ι) * ‖(linearEquiv ℂ ((i : ι) → E i)) x‖

Tactic:
simp only [NNReal.coe_natCast, linearEquiv_apply]

Result:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ≤ ↑(Fintype.card ι) * ‖(equiv ((i : ι) → E i)) x‖

Proof state:
A : Type u_1
inst✝⁷ : NonUnitalCStarAlgebra A
inst✝⁶ : PartialOrder A
ι : Type u_2
E : ι → Type u_3
inst✝⁵ : Fintype ι
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → Module ℂ (E i)
inst✝² : (i : ι) → SMul Aᵐᵒᵖ (E i)
inst✝¹ : (i : ι) → CStarModule A (E i)
inst✝ : StarOrderedRing A
x : C⋆ᵐᵒᵈ ((i : ι) → E i)
⊢ ‖x‖ ≤ ↑(Fintype.card ι) * ‖(equiv ((i : ι) → E i)) x‖

Tactic:
calc ‖x‖ ≤ ∑ i, ‖x i‖ := pi_norm_le_sum_norm x
  _ ≤ ∑ _, ‖⇑x‖ := Finset.sum_le_sum fun _ _ ↦ norm_le_pi_norm ..
  _ ≤ Fintype.card ι * ‖⇑x‖ := by simp

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem pow_dvd_pow_iff {a b n : ℕ} (n0 : n ≠ 0) : a ^ n ∣ b ^ n ↔ a ∣ b

Proof state:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : (a' * g).gcd (b' * g) > 0
⊢ a' * g ∣ b' * g

Tactic:
rw [mul_pow, mul_pow] at h

Result:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : (a' * g).gcd (b' * g) > 0
⊢ a' * g ∣ b' * g

Proof state:
case inl
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
g0 : a.gcd b = 0
⊢ a ∣ b

Tactic:
simp [eq_zero_of_gcd_eq_zero_right g0]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
h : a' ^ n * g ^ n ∣ b' ^ n * g ^ n
g0 : (a' * g).gcd (b' * g) > 0
⊢ a' * g ∣ b' * g

Tactic:
replace h := Nat.dvd_of_mul_dvd_mul_right (Nat.pow_pos g0') h

Result:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g

Proof state:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
⊢ a' * g ∣ b' * g

Tactic:
have := pow_dvd_pow a' <| Nat.pos_of_ne_zero n0

Result:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g

Proof state:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ^ succ 0 ∣ a' ^ n
⊢ a' * g ∣ b' * g

Tactic:
rw [pow_one, (co.pow n n).eq_one_of_dvd h] at this

Result:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g

Proof state:
a b n : ℕ
n0 : n ≠ 0
⊢ a ^ n ∣ b ^ n ↔ a ∣ b

Tactic:
refine ⟨fun h => ?_, fun h => pow_dvd_pow_of_dvd h _⟩

Result:
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
⊢ a ∣ b

Proof state:
case inr
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
g0 : a.gcd b > 0
⊢ a ∣ b

Tactic:
rcases exists_coprime' g0 with ⟨g, a', b', g0', co, rfl, rfl⟩

Result:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
h : (a' * g) ^ n ∣ (b' * g) ^ n
g0 : (a' * g).gcd (b' * g) > 0
⊢ a' * g ∣ b' * g

Proof state:
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
⊢ a ∣ b

Tactic:
rcases Nat.eq_zero_or_pos (gcd a b) with g0 | g0

Result:
case inl
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
g0 : a.gcd b = 0
⊢ a ∣ b

case inr
a b n : ℕ
n0 : n ≠ 0
h : a ^ n ∣ b ^ n
g0 : a.gcd b > 0
⊢ a ∣ b

Proof state:
case inr.intro.intro.intro.intro.intro.intro
n : ℕ
n0 : n ≠ 0
g a' b' : ℕ
g0' : 0 < g
co : a'.Coprime b'
g0 : (a' * g).gcd (b' * g) > 0
h : a' ^ n ∣ b' ^ n
this : a' ∣ 1
⊢ a' * g ∣ b' * g

Tactic:
simp [eq_one_of_dvd_one this]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem le_true : ∀ (x : Bool), x ≤ true

Proof state:
⊢ ∀ (x : Bool), x ≤ true

Tactic:
decide

Result:
no goals