harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/Teichmuller.lean
theorem ghostComponent_teichmullerFun (r : R) (n : ℕ) :
    ghostComponent n (teichmullerFun p r) = r ^ p ^ n

Proof state:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
exact (h (Nat.succ_pos n)).elim

Result:
no goals

Proof state:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n i : ℕ
a✝ : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0

Tactic:
simp [teichmullerFun, h0, hp.1.ne_zero]

Result:
no goals

Proof state:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
rw [Finset.mem_range]

Result:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n

Tactic:
rfl

Result:
no goals

Proof state:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ¬0 < n + 1 → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Tactic:
intro h

Result:
case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
h : ¬0 < n + 1
⊢ ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Proof state:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ (ghostComponent n) (teichmullerFun p r) = r ^ p ^ n

Tactic:
rw [ghostComponent_apply, aeval_wittPolynomial, Finset.sum_eq_single 0, pow_zero, one_mul,
  tsub_zero]

Result:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ (teichmullerFun p r).coeff 0 ^ p ^ n = r ^ p ^ n

case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

case h₁
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ 0 ∉ Finset.range (n + 1) → ↑p ^ 0 * (teichmullerFun p r).coeff 0 ^ p ^ (n - 0) = 0

Proof state:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n : ℕ
⊢ ∀ b ∈ Finset.range (n + 1), b ≠ 0 → ↑p ^ b * (teichmullerFun p r).coeff b ^ p ^ (n - b) = 0

Tactic:
intro i _ h0

Result:
case h₀
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
r : R
n i : ℕ
a✝ : i ∈ Finset.range (n + 1)
h0 : i ≠ 0
⊢ ↑p ^ i * (teichmullerFun p r).coeff i ^ p ^ (n - i) = 0
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem eraseKey_of_perm [BEq α] [EquivBEq α] {l l' : List ((a : α) × β a)} {k : α}
    (hl : DistinctKeys l) (h : Perm l l') : Perm (eraseKey k l) (eraseKey k l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
hl : DistinctKeys l
h : l.Perm l'
⊢ (eraseKey k l).Perm (eraseKey k l')

Tactic:
apply getEntry?_ext hl.eraseKey (hl.perm h.symm).eraseKey

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (eraseKey k l) = getEntry? a (eraseKey k l')

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l l' : List ((a : α) × β a)
k : α
hl : DistinctKeys l
h : l.Perm l'
⊢ ∀ (a : α), getEntry? a (eraseKey k l) = getEntry? a (eraseKey k l')

Tactic:
simp [getEntry?_eraseKey hl, getEntry?_eraseKey (hl.perm h.symm), getEntry?_of_perm hl h]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Different.lean
lemma le_traceDual {I J : Submodule B L} :
    I ≤ Jᵛ ↔ I * J ≤ 1ᵛ

Proof state:
A : Type u_1
K : Type u_2
L : Type u
B : Type u_3
inst✝¹⁰ : CommRing A
inst✝⁹ : Field K
inst✝⁸ : CommRing B
inst✝⁷ : Field L
inst✝⁶ : Algebra A K
inst✝⁵ : Algebra B L
inst✝⁴ : Algebra A B
inst✝³ : Algebra K L
inst✝² : Algebra A L
inst✝¹ : IsScalarTower A K L
inst✝ : IsScalarTower A B L
I J : Submodule B L
⊢ I ≤ Jᵛ ↔ I * J ≤ 1ᵛ

Tactic:
rw [← le_traceDual_mul_iff, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem mem_eraseIdx_iff_getElem? {x : α} {l} {k} : x ∈ eraseIdx l k ↔ ∃ i ≠ k, l[i]? = some x

Proof state:
case mpr.intro
α : Type u_1
x : α
l : List α
k i : Nat
h : l[i]? = some x
h' : i < l.length
⊢ ∃ x_1, l[i]? = some x

Tactic:
exact ⟨h', h⟩

Result:
no goals

Proof state:
α : Type u_1
x : α
l : List α
k : Nat
⊢ x ∈ l.eraseIdx k ↔ ∃ i, i ≠ k ∧ l[i]? = some x

Tactic:
simp only [mem_eraseIdx_iff_getElem, getElem_eq_iff, exists_and_left]

Result:
α : Type u_1
x : α
l : List α
k : Nat
⊢ (∃ i, i ≠ k ∧ ∃ x_1, l[i]? = some x) ↔ ∃ i, i ≠ k ∧ l[i]? = some x

Proof state:
α : Type u_1
x : α
l : List α
k i : Nat
⊢ (∃ x_1, l[i]? = some x) ↔ l[i]? = some x

Tactic:
constructor

Result:
case mp
α : Type u_1
x : α
l : List α
k i : Nat
⊢ (∃ x_1, l[i]? = some x) → l[i]? = some x

case mpr
α : Type u_1
x : α
l : List α
k i : Nat
⊢ l[i]? = some x → ∃ x_1, l[i]? = some x

Proof state:
case mpr
α : Type u_1
x : α
l : List α
k i : Nat
⊢ l[i]? = some x → ∃ x_1, l[i]? = some x

Tactic:
rintro h

Result:
case mpr
α : Type u_1
x : α
l : List α
k i : Nat
h : l[i]? = some x
⊢ ∃ x_1, l[i]? = some x

Proof state:
case mpr
α : Type u_1
x : α
l : List α
k i : Nat
h : l[i]? = some x
⊢ ∃ x_1, l[i]? = some x

Tactic:
obtain ⟨h', -⟩ := getElem?_eq_some_iff.1 h

Result:
case mpr.intro
α : Type u_1
x : α
l : List α
k i : Nat
h : l[i]? = some x
h' : i < l.length
⊢ ∃ x_1, l[i]? = some x

Proof state:
α : Type u_1
x : α
l : List α
k : Nat
⊢ (∃ i, i ≠ k ∧ ∃ x_1, l[i]? = some x) ↔ ∃ i, i ≠ k ∧ l[i]? = some x

Tactic:
refine exists_congr fun i => and_congr_right' ?_

Result:
α : Type u_1
x : α
l : List α
k i : Nat
⊢ (∃ x_1, l[i]? = some x) ↔ l[i]? = some x

Proof state:
case mp.intro
α : Type u_1
x : α
l : List α
k i : Nat
w✝ : i < l.length
h : l[i]? = some x
⊢ l[i]? = some x

Tactic:
exact h

Result:
no goals

Proof state:
case mp
α : Type u_1
x : α
l : List α
k i : Nat
⊢ (∃ x_1, l[i]? = some x) → l[i]? = some x

Tactic:
rintro ⟨_, h⟩

Result:
case mp.intro
α : Type u_1
x : α
l : List α
k i : Nat
w✝ : i < l.length
h : l[i]? = some x
⊢ l[i]? = some x
-- Mathlib/NumberTheory/LSeries/Injectivity.lean
/-- If the coefficients `f m` of an L-series are zero for `m ≤ n` and the L-series converges
at some point, then `f (n+1)` is the limit of `(n+1)^x * LSeries f x` as `x → ∞`. -/
lemma LSeries.tendsto_cpow_mul_atTop {f : ℕ → ℂ} {n : ℕ} (h : ∀ m ≤ n, f m = 0)
    (ha : abscissaOfAbsConv f < ⊤):
    Tendsto (fun x : ℝ ↦ (n + 1) ^ (x : ℂ) * LSeries f x) atTop (nhds (f (n + 1)))

Proof state:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1)))

Tactic:
conv => enter [3, 1]; rw [← add_zero (f _)]

Result:
case intro.intro.intro
f : ℕ → ℂ
n : ℕ
h : ∀ m ≤ n, f m = 0
ha : abscissaOfAbsConv f < ⊤
y : ℝ
hay : abscissaOfAbsConv f < ↑y
hyt : ↑y < ⊤
F : ℝ → ℕ → ℂ := fun x => {m | n + 1 < m}.indicator fun m => f m / (↑m / (↑n + 1)) ^ ↑x
hF₀ : ∀ (x : ℝ) {m : ℕ}, m ≤ n + 1 → F x m = 0
hF : ∀ (x : ℝ) {m : ℕ}, m ≠ n + 1 → F x m = (↑n + 1) ^ ↑x * term f (↑x) m
hs : ∀ {x : ℝ}, x ≥ y → Summable fun m => (↑n + 1) ^ ↑x * term f (↑x) m
key : ∀ x ≥ y, (↑n + 1) ^ ↑x * LSeries f ↑x = f (n + 1) + ∑' (m : ℕ), F x m
⊢ Tendsto (fun x => (↑n + 1) ^ ↑x * LSeries f ↑x) atTop (nhds (f (n + 1) + 0))
-- Mathlib/Data/Matroid/Circuit.lean
lemma mem_closure_iff_exists_isCircuit (he : e ∉ X) :
    e ∈ M.closure X ↔ ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C :=
  ⟨fun h ↦ exists_isCircuit_of_mem_closure h he, fun ⟨C, hCX, hC, heC⟩ ↦ mem_of_mem_of_subset
    (hC.mem_closure_diff_singleton_of_mem heC) (M.closure_subset_closure (by simpa))⟩

Proof state:
α : Type u_1
M : Matroid α
X : Set α
e : α
he : e ∉ X
x✝ : ∃ C ⊆ insert e X, M.IsCircuit C ∧ e ∈ C
C : Set α
hCX : C ⊆ insert e X
hC : M.IsCircuit C
heC : e ∈ C
⊢ C \ {e} ⊆ X

Tactic:
simpa

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem forall_mem_map {f : α → β} {o : Option α} {p : β → Prop} :
    (∀ y ∈ o.map f, p y) ↔ ∀ x ∈ o, p (f x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
o : Option α
p : β → Prop
⊢ (∀ (y : β), y ∈ Option.map f o → p y) ↔ ∀ (x : α), x ∈ o → p (f x)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/Map2.lean
theorem map₂Left_eq_zipWith :
    ∀ as bs, length as ≤ length bs → map₂Left f as bs = zipWith (fun a b => f a (some b)) as bs
  | [], [], _ => by simp
  | [], _ :: _, _ => by simp
  | a :: as, [], h => by
    simp at h
  | a :: as, b :: bs, h => by
    simp only [length_cons, succ_le_succ_iff] at h
    simp [h, map₂Left_eq_zipWith]

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
h : (a :: as).length ≤ [].length
⊢ map₂Left f (a :: as) [] = zipWith (fun a b => f a (some b)) (a :: as) []

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : as.length ≤ bs.length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)

Tactic:
simp [h, map₂Left_eq_zipWith]

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : (a :: as).length ≤ (b :: bs).length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)

Tactic:
simp only [length_cons, succ_le_succ_iff] at h

Result:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
a : α
as : List α
b : β
bs : List β
h : as.length ≤ bs.length
⊢ map₂Left f (a :: as) (b :: bs) = zipWith (fun a b => f a (some b)) (a :: as) (b :: bs)

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
x✝ : [].length ≤ [].length
⊢ map₂Left f [] [] = zipWith (fun a b => f a (some b)) [] []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → Option β → γ
head✝ : β
tail✝ : List β
x✝ : [].length ≤ (head✝ :: tail✝).length
⊢ map₂Left f [] (head✝ :: tail✝) = zipWith (fun a b => f a (some b)) [] (head✝ :: tail✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_iSup (hf : ∀ i, f i ≠ ∞) : (iSup f).toNNReal = ⨆ i, (f i).toNNReal

Proof state:
case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
rw [NNReal.iSup_of_not_bddAbove h, iSup_coe_eq_top.2 h, top_toNNReal]

Result:
no goals

Proof state:
case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
rw [← coe_iSup h, toNNReal_coe]

Result:
no goals

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
hf : ∀ (i : ι), f i ≠ ⊤
⊢ (iSup f).toNNReal = ⨆ i, (f i).toNNReal

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case intro
ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, ((fun i => ↑(f i)) i).toNNReal

Proof state:
case intro
ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Tactic:
by_cases h : BddAbove (range f)

Result:
case pos
ι : Sort u_1
f : ι → ℝ≥0
h : BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

case neg
ι : Sort u_1
f : ι → ℝ≥0
h : ¬BddAbove (range f)
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i

Proof state:
case intro
ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, ((fun i => ↑(f i)) i).toNNReal

Tactic:
simp_rw [toNNReal_coe]

Result:
case intro
ι : Sort u_1
f : ι → ℝ≥0
⊢ (⨆ i, ↑(f i)).toNNReal = ⨆ i, f i
-- Mathlib/Data/Seq/Seq.lean
theorem eq_of_bisim (bisim : IsBisimulation R) {s₁ s₂} (r : s₁ ~ s₂) : s₁ = s₂

Proof state:
case nil.nil
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head ∧ R nil.tail nil.tail

Tactic:
constructor

Result:
case nil.nil.left
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ nil.head = nil.head

case nil.nil.right
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
r : R nil nil
this✝ : BisimO R nil.destruct nil.destruct
⊢ R nil.tail nil.tail

Proof state:
case mk
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r✝¹ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
s : Seq α
val✝ : Stream' (Option α)
property✝ : val✝.IsSeq
r✝ : R s ⟨val✝, property✝⟩
this : s.head = head ⟨val✝, property✝⟩ ∧ R s.tail (tail ⟨val✝, property✝⟩)
r : R s.tail (tail ⟨val✝, property✝⟩)
⊢ ↑(tail ⟨val✝, property✝⟩) = (↑⟨val✝, property✝⟩).tail

Tactic:
rfl

Result:
no goals

Proof state:
case a.a
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∃ s s', ↑s = ↑s₁ ∧ ↑s' = ↑s₂ ∧ R s s'

Tactic:
exact ⟨s₁, s₂, rfl, rfl, r⟩

Result:
no goals

Proof state:
case a.bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
⊢ ∀ ⦃s₁ s₂ : Stream' (Option α)⦄,
    (∃ s s', ↑s = s₁ ∧ ↑s' = s₂ ∧ R s s') → s₁.head = s₂.head ∧ ∃ s s', ↑s = s₁.tail ∧ ↑s' = s₂.tail ∧ R s s'

Tactic:
intro t₁ t₂ e

Result:
case a.bisim
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
⊢ t₁.head = t₂.head ∧ ∃ s s', ↑s = t₁.tail ∧ ↑s' = t₂.tail ∧ R s s'

Proof state:
case cons.cons.intro
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ some x✝¹ = some x✝ ∧ R s✝¹ s✝

Tactic:
constructor

Result:
case cons.cons.intro.left
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ some x✝¹ = some x✝

case cons.cons.intro.right
α : Type u
R : Seq α → Seq α → Prop
bisim : IsBisimulation R
s₁ s₂ : Seq α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', ↑s = t₁ ∧ ↑s' = t₂ ∧ R s s'
x✝¹ : α
s✝¹ : Seq α
x✝ : α
s✝ : Seq α
r✝ : R (cons x✝¹ s✝¹) (cons x✝ s✝)
h1 : x✝¹ = x✝
h2 : R s✝¹ s✝
⊢ R s✝¹ s✝
-- Mathlib/RingTheory/Polynomial/Dickson.lean
theorem dickson_of_two_le {n : ℕ} (h : 2 ≤ n) :
    dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2)

Proof state:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ n
⊢ dickson k a n = X * dickson k a (n - 1) - C a * dickson k a (n - 2)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_of_le h

Result:
case intro
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - C a * dickson k a (2 + n - 2)

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (2 + n) = X * dickson k a (2 + n - 1) - C a * dickson k a (2 + n - 2)

Tactic:
rw [add_comm]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - C a * dickson k a (n + 2 - 2)

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
k : ℕ
a : R
n : ℕ
h : 2 ≤ 2 + n
⊢ dickson k a (n + 2) = X * dickson k a (n + 2 - 1) - C a * dickson k a (n + 2 - 2)

Tactic:
exact dickson_add_two k a n

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem norm_toL1 (f : α → β) (hf : Integrable f μ) :
    ‖hf.toL1 f‖ = (∫⁻ a, edist (f a) 0 ∂μ).toReal

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), edist (f a) 0 ∂μ).toReal

Tactic:
simp [toL1, Lp.norm_toLp, eLpNorm, eLpNorm'_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/NumberTheory/EulerProduct/Basic.lean
/-- Given a (completely) multiplicative function `f : ℕ → F`, where `F` is a normed field,
such that `‖f p‖ < 1` for all primes `p`, we can express the sum of `f n` over all `s`-factored
positive integers `n` as a product of `(1 - f p)⁻¹` over the primes `p ∈ s`. At the same time,
we show that the sum involved converges absolutely. -/
lemma summable_and_hasSum_factoredNumbers_prod_filter_prime_geometric {f : ℕ →* F}
    (h : ∀ {p : ℕ}, p.Prime → ‖f p‖ < 1) (s : Finset ℕ) :
    Summable (fun m : factoredNumbers s ↦ ‖f m‖) ∧
      HasSum (fun m : factoredNumbers s ↦ f m) (∏ p ∈ s with p.Prime, (1 - f p)⁻¹)

Proof state:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
⊢ ∀ {p : ℕ}, Nat.Prime p → Summable fun n => ‖f (p ^ n)‖

Tactic:
intro p hp

Result:
F : Type u_1
inst✝¹ : NormedField F
inst✝ : CompleteSpace F
f : ℕ →* F
h : ∀ {p : ℕ}, Nat.Prime p → ‖f p‖ < 1
s : Finset ℕ
hmul : ∀ {m n : ℕ}, m.Coprime n → f (m * n) = f m * f n
H₁ : ∏ p ∈ filter (fun p => Nat.Prime p) s, ∑' (n : ℕ), f (p ^ n) = ∏ p ∈ filter (fun p => Nat.Prime p) s, (1 - f p)⁻¹
p : ℕ
hp : Nat.Prime p
⊢ Summable fun n => ‖f (p ^ n)‖
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem coeff_algebraMap [Nontrivial S] (h : IsAdjoinRootMonic S f) (x : R) :
    h.coeff (algebraMap R S x) = Pi.single 0 x

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ x * Pi.single 0 1 i = Pi.single 0 x i

Tactic:
refine (Pi.apply_single (fun _ y => x * y) ?_ 0 1 i).trans (by simp)

Result:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ ∀ (i : ℕ), (fun x_1 y => x * y) i 0 = 0

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
⊢ h.coeff ((algebraMap R S) x) = Pi.single 0 x

Tactic:
ext i

Result:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ h.coeff ((algebraMap R S) x) i = Pi.single 0 x i

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ ∀ (i : ℕ), (fun x_1 y => x * y) i 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ Pi.single 0 (x * 1) i = Pi.single 0 x i

Tactic:
simp

Result:
no goals

Proof state:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ h.coeff ((algebraMap R S) x) i = Pi.single 0 x i

Tactic:
rw [Algebra.algebraMap_eq_smul_one, map_smul, coeff_one, Pi.smul_apply, smul_eq_mul]

Result:
case h
R : Type u
S : Type v
inst✝³ : CommRing R
inst✝² : Ring S
f : R[X]
inst✝¹ : Algebra R S
inst✝ : Nontrivial S
h : IsAdjoinRootMonic S f
x : R
i : ℕ
⊢ x * Pi.single 0 1 i = Pi.single 0 x i
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_pos [PosMulStrictMono G₀] (ha : 0 < a) : ∀ n : ℤ, 0 < a ^ n
  | (n : ℕ) => by rw [zpow_natCast]; exact pow_pos ha _
  |-(n + 1 : ℕ) => by rw [zpow_neg, inv_pos, zpow_natCast]; exact pow_pos ha _

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n

Tactic:
exact pow_pos ha _

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)

Tactic:
exact pow_pos ha _

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ ↑n

Tactic:
rw [zpow_natCast]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (-↑(n + 1))

Tactic:
rw [zpow_neg, inv_pos, zpow_natCast]

Result:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
n : ℕ
⊢ 0 < a ^ (n + 1)