harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_eq_zpow_neg_valuation {f : PadicSeq p} (hf : ¬f ≈ 0) :
    f.norm = (p : ℚ) ^ (-f.valuation : ℤ)

Proof state:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ LimZero f

Tactic:
intro ε hε

Result:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑f j) < ε

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑f j) < ε

Tactic:
intro n hn

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f n) < ε

Tactic:
rw [stationaryPoint_spec hf le_rfl hn]

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f (stationaryPoint hf)) < ε

Proof state:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∃ i, ∀ j ≥ i, padicNorm p (↑f j) < ε

Tactic:
use stationaryPoint hf

Result:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
⊢ ∀ j ≥ stationaryPoint hf, padicNorm p (↑f j) < ε

Proof state:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0

Tactic:
intro H

Result:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ False

Proof state:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
ε : ℚ
hε : ε > 0
n : ℕ
hn : n ≥ stationaryPoint hf
⊢ padicNorm p (↑f (stationaryPoint hf)) < ε

Tactic:
simpa [H] using hε

Result:
no goals

Proof state:
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ f.norm = ↑p ^ (-f.valuation)

Tactic:
rw [norm, valuation, dif_neg hf, dif_neg hf, padicNorm, if_neg]

Result:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
⊢ ¬↑f (stationaryPoint hf) = 0

Proof state:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ False

Tactic:
apply CauSeq.not_limZero_of_not_congr_zero hf

Result:
case hnc
p : ℕ
inst✝ : Fact (Nat.Prime p)
f : PadicSeq p
hf : ¬f ≈ 0
H : ↑f (stationaryPoint hf) = 0
⊢ LimZero f
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
theorem IsClique.of_induce {S : Subgraph G} {F : Set α} {A : Set F}
    (c : (S.induce F).coe.IsClique A) : G.IsClique (Subtype.val '' A)

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
anb : x✝ ≠ y✝
⊢ G.Adj x✝ y✝

Tactic:
exact S.adj_sub (c ainA binA (Subtype.coe_ne_coe.mp anb)).2.2

Result:
no goals

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ G.IsClique (Subtype.val '' A)

Tactic:
simp only [Set.Pairwise, Set.mem_image, Subtype.exists, exists_and_right, exists_eq_right]

Result:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ ∀ ⦃x : α⦄, (∃ (x_1 : x ∈ F), ⟨x, ⋯⟩ ∈ A) → ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x ≠ y → G.Adj x y

Proof state:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
⊢ ∀ ⦃x : α⦄, (∃ (x_1 : x ∈ F), ⟨x, ⋯⟩ ∈ A) → ∀ ⦃y : α⦄, (∃ (x : y ∈ F), ⟨y, ⋯⟩ ∈ A) → x ≠ y → G.Adj x y

Tactic:
intro _ ⟨_, ainA⟩ _ ⟨_, binA⟩ anb

Result:
α : Type u_1
G : SimpleGraph α
S : G.Subgraph
F : Set α
A : Set ↑F
c : (S.induce F).coe.IsClique A
x✝ : α
w✝¹ : x✝ ∈ F
ainA : ⟨x✝, ⋯⟩ ∈ A
y✝ : α
w✝ : y✝ ∈ F
binA : ⟨y✝, ⋯⟩ ∈ A
anb : x✝ ≠ y✝
⊢ G.Adj x✝ y✝
-- Mathlib/Tactic/Abel.lean
theorem term_smul {α} [AddCommMonoid α] (c n x a n' a')
    (h₁ : c * n = n') (h₂ : smul c a = a') :
    smul c (@term α _ n x a) = term n' x a'

Proof state:
α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'

Tactic:
simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem terminatedAt_zero_iff {s : Seq α} : s.TerminatedAt 0 ↔ s = nil

Proof state:
case refine_2
α : Type u
⊢ nil.TerminatedAt 0

Tactic:
simp [TerminatedAt]

Result:
no goals

Proof state:
case refine_1.h.a
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ a✝ ∈ none ↔ a✝ ∈ nil.get? n

Tactic:
simp

Result:
no goals

Proof state:
case refine_1.h.a
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ a✝ ∈ s.get? n ↔ a✝ ∈ nil.get? n

Tactic:
rw [le_stable _ (Nat.zero_le _) h]

Result:
case refine_1.h.a
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ a✝ ∈ none ↔ a✝ ∈ nil.get? n

Proof state:
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 ↔ s = nil

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Proof state:
case refine_2
α : Type u
s : Seq α
⊢ s = nil → s.TerminatedAt 0

Tactic:
rintro rfl

Result:
case refine_2
α : Type u
⊢ nil.TerminatedAt 0

Proof state:
case refine_1
α : Type u
s : Seq α
⊢ s.TerminatedAt 0 → s = nil

Tactic:
intro h

Result:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
⊢ s = nil

Proof state:
case refine_1
α : Type u
s : Seq α
h : s.TerminatedAt 0
⊢ s = nil

Tactic:
ext n

Result:
case refine_1.h.a
α : Type u
s : Seq α
h : s.TerminatedAt 0
n : ℕ
a✝ : α
⊢ a✝ ∈ s.get? n ↔ a✝ ∈ nil.get? n
-- Mathlib/Data/Analysis/Filter.lean
theorem mem_sets {f : Filter α} (F : f.Realizer) {a : Set α} : a ∈ f ↔ ∃ b, F.F b ⊆ a

Proof state:
α : Type u_1
f : Filter α
F : f.Realizer
a : Set α
⊢ a ∈ f ↔ ∃ b, F.F.f b ⊆ a

Tactic:
cases F

Result:
case mk
α : Type u_1
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ a ∈ f ↔ ∃ b, { σ := σ✝, F := F✝, eq := eq✝ }.F.f b ⊆ a

Proof state:
case mk
α : Type u_1
f : Filter α
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
eq✝ : F✝.toFilter = f
⊢ a ∈ f ↔ ∃ b, { σ := σ✝, F := F✝, eq := eq✝ }.F.f b ⊆ a

Tactic:
subst f

Result:
case mk
α : Type u_1
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ F✝.toFilter ↔ ∃ b, { σ := σ✝, F := F✝, eq := ⋯ }.F.f b ⊆ a

Proof state:
case mk
α : Type u_1
a : Set α
σ✝ : Type u_5
F✝ : CFilter (Set α) σ✝
⊢ a ∈ F✝.toFilter ↔ ∃ b, { σ := σ✝, F := F✝, eq := ⋯ }.F.f b ⊆ a

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey?_modifyKey [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β))
    (hl : DistinctKeys l) :
    getKey? k' (modifyKey k f l) =
      if k == k' then
        if containsKey k l then some k else none
      else
        getKey? k' l

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
k k' : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
⊢ getKey? k' (modifyKey k f l) =
    if (k == k') = true then if containsKey k l = true then some k else none else getKey? k' l

Tactic:
simp [modifyKey_eq_alterKey, getKey?_alterKey, containsKey_eq_isSome_getValue?, hl]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem inf_le_right (f g : α →ₘ[μ] β) : f ⊓ g ≤ g

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f a✝ ⊓ ↑g a✝ ≤ ↑g a✝

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ g

Tactic:
rw [← coeFn_le]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᶠ[ae μ] ↑g

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑g a✝

Tactic:
rw [ha]

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f a✝ ⊓ ↑g a✝ ≤ ↑g a✝

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᶠ[ae μ] ↑g

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑g a✝
-- Mathlib/RingTheory/Binomial.lean
theorem choose_succ_succ [NatPowAssoc R] (r : R) (k : ℕ) :
    choose (r + 1) (k + 1) = choose r k + choose r (k + 1)

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))

Tactic:
simp only [smul_add, ← descPochhammer_eq_factorial_smul_choose]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1).factorial • choose r k + (descPochhammer ℤ (k + 1)).smeval r

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (descPochhammer ℤ (k + 1)).smeval (r + 1) = (k + 1).factorial • choose r k + (descPochhammer ℤ (k + 1)).smeval r

Tactic:
rw [Nat.factorial_succ, mul_smul,
  ← descPochhammer_eq_factorial_smul_choose r, descPochhammer_succ_succ_smeval r k]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ choose (r + 1) (k + 1) = choose r k + choose r (k + 1)

Tactic:
rw [← nsmul_right_inj (Nat.factorial_ne_zero (k + 1))]

Result:
R : Type u_1
inst✝³ : NonAssocRing R
inst✝² : Pow R ℕ
inst✝¹ : BinomialRing R
inst✝ : NatPowAssoc R
r : R
k : ℕ
⊢ (k + 1).factorial • choose (r + 1) (k + 1) = (k + 1).factorial • (choose r k + choose r (k + 1))
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_finset_prod
    (hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) :
    derivWithin (∏ i ∈ u, f i ·) s x =
      ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x

Proof state:
case inr
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
case inl
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x

Tactic:
exact (HasDerivWithinAt.finset_prod fun i hi ↦ (hf i hi).hasDerivWithinAt).derivWithin hxs

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
⊢ derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x

case inr
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
x : 𝕜
s : Set 𝕜
ι : Type u_2
inst✝² : DecidableEq ι
𝔸' : Type u_3
inst✝¹ : NormedCommRing 𝔸'
inst✝ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
f : ι → 𝕜 → 𝔸'
hf : ∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
-- Mathlib/LinearAlgebra/CliffordAlgebra/Basic.lean
theorem lift_unique (f : M →ₗ[R] A) (cond : ∀ m : M, f m * f m = algebraMap _ _ (Q m))
    (g : CliffordAlgebra Q →ₐ[R] A) : g.toLinearMap.comp (ι Q) = f ↔ g = lift Q ⟨f, cond⟩

Proof state:
case h.e'_1.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ (lift Q).symm g = ⟨f, cond⟩

Tactic:
rw [lift_symm_apply, Subtype.mk_eq_mk]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ g = (lift Q) ⟨f, cond⟩

Tactic:
convert (lift Q : _ ≃ (CliffordAlgebra Q →ₐ[R] A)).symm_apply_eq

Result:
case h.e'_1.a
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
cond : ∀ (m : M), f m * f m = (algebraMap R A) (Q m)
g : CliffordAlgebra Q →ₐ[R] A
⊢ g.toLinearMap ∘ₗ ι Q = f ↔ (lift Q).symm g = ⟨f, cond⟩
-- Mathlib/Analysis/Complex/Hadamard.lean
/-- If `f` is bounded on the unit vertical strip, then `f` is bounded by `sSupNormIm` there. -/
lemma norm_le_sSupNormIm (f : ℂ → E) (z : ℂ) (hD : z ∈ verticalClosedStrip 0 1)
    (hB : BddAbove ((norm ∘ f) '' verticalClosedStrip 0 1)) :
    ‖f z‖ ≤ sSupNormIm f (z.re)

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ≤ sSupNormIm f z.re

Tactic:
refine le_csSup ?_ ?_

Result:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ f '' (re ⁻¹' {z.re}))

case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ∈ norm ∘ f '' (re ⁻¹' {z.re})

Proof state:
case refine_1
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ BddAbove (norm ∘ f '' (re ⁻¹' {z.re}))

Tactic:
apply BddAbove.mono (image_subset (norm ∘ f) _) hB

Result:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1

Proof state:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ ‖f z‖ ∈ norm ∘ f '' (re ⁻¹' {z.re})

Tactic:
apply mem_image_of_mem (norm ∘ f)

Result:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ re ⁻¹' {z.re}

Proof state:
case refine_2
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ z ∈ re ⁻¹' {z.re}

Tactic:
simp only [mem_preimage, mem_singleton]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hD : z ∈ verticalClosedStrip 0 1
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
⊢ re ⁻¹' {z.re} ⊆ verticalClosedStrip 0 1

Tactic:
exact preimage_mono (singleton_subset_iff.mpr hD)

Result:
no goals
-- Mathlib/Topology/Algebra/Ring/Basic.lean
theorem IsTopologicalSemiring.continuousNeg_of_mul [TopologicalSpace α] [NonAssocRing α]
    [ContinuousMul α] : ContinuousNeg α where
  continuous_neg

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : NonAssocRing α
inst✝ : ContinuousMul α
⊢ Continuous fun a => -a

Tactic:
simpa using (continuous_const.mul continuous_id : Continuous fun x : α => -1 * x)

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Finite.exists_univ_list (α) [Finite α] : ∃ l : List α, l.Nodup ∧ ∀ x : α, x ∈ l

Proof state:
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ List.Nodup ?m.8134 ∧ ∀ (x : α), x ∈ ?m.8134

Tactic:
rwa [← e] at this

Result:
no goals

Proof state:
case intro.intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
exact ⟨_, by rwa [← e] at this⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
have := And.intro (@univ α _).2 (@mem_univ_val α _)

Result:
case intro.intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
this : univ.val.Nodup ∧ ∀ (x : α), x ∈ univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Proof state:
case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
obtain ⟨l, e⟩ := Quotient.exists_rep (@univ α _).1

Result:
case intro.intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
l : List α
e : ⟦l⟧ = univ.val
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Proof state:
α : Type u_4
inst✝ : Finite α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l

Tactic:
cases nonempty_fintype α

Result:
case intro
α : Type u_4
inst✝ : Finite α
val✝ : Fintype α
⊢ ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
-- Mathlib/Data/PFunctor/Multivariate/W.lean
theorem w_map_wMk {α β : TypeVec n} (g : α ⟹ β) (a : P.A) (f' : P.drop.B a ⟹ α)
    (f : P.last.B a → P.W α) : g <$$> P.wMk a f' f = P.wMk a (g ⊚ f') fun i => g <$$> f i

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i => ⟨(f i).fst, (f i).snd⟩
⊢ g <$$> ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩ =
    ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn (g ⊚ f') fun i => g ⊚ (f i).snd⟩

Tactic:
have h := MvPFunctor.map_eq P.wp g

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i => ⟨(f i).fst, (f i).snd⟩
h : ∀ (a : P.wp.A) (f : P.wp.B a ⟹ α), g <$$> ⟨a, f⟩ = ⟨a, g ⊚ f⟩
⊢ g <$$> ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn f' fun i => (f i).snd⟩ =
    ⟨WType.mk a fun i => (f i).fst, P.wPathCasesOn (g ⊚ f') fun i => g ⊚ (f i).snd⟩

Proof state:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i => ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i => ⟨(f i).fst, (f i).snd⟩) =
    P.wMk a (g ⊚ f') fun i => ⟨((fun i => ⟨(f i).fst, (f i).snd⟩) i).fst, g ⊚ ((fun i => ⟨(f i).fst, (f i).snd⟩) i).snd⟩

Tactic:
dsimp

Result:
n : ℕ
P : MvPFunctor.{u} (n + 1)
α β : TypeVec.{u} n
g : α ⟹ β
a : P.A
f' : P.drop.B a ⟹ α
f : P.last.B a → P.W α
this✝ : MvFunctor.map g ∘ f = fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
this : f = fun i => ⟨(f i).fst, (f i).snd⟩
⊢ (g <$$> P.wMk a f' fun i => ⟨(f i).fst, (f i).snd⟩) = P.wMk a (g ⊚ f') fun i => ⟨(f i).fst, g ⊚ (f i).snd⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_eq_getLsbD_last (x : BitVec w) :
    x.msb = x.getLsbD (w - 1)

Proof state:
w : Nat
x : BitVec w
⊢ (decide (0 < w) && x.getLsbD (w - 1 - 0)) = x.getLsbD (w - 1)

Tactic:
rcases w  with rfl | w

Result:
case zero
x : BitVec 0
⊢ (decide (0 < 0) && x.getLsbD (0 - 1 - 0)) = x.getLsbD (0 - 1)

case succ
w : Nat
x : BitVec (w + 1)
⊢ (decide (0 < w + 1) && x.getLsbD (w + 1 - 1 - 0)) = x.getLsbD (w + 1 - 1)

Proof state:
case zero
x : BitVec 0
⊢ (decide (0 < 0) && x.getLsbD (0 - 1 - 0)) = x.getLsbD (0 - 1)

Tactic:
simp [BitVec.eq_nil x]

Result:
no goals

Proof state:
case succ
w : Nat
x : BitVec (w + 1)
⊢ (decide (0 < w + 1) && x.getLsbD (w + 1 - 1 - 0)) = x.getLsbD (w + 1 - 1)

Tactic:
simp

Result:
no goals

Proof state:
w : Nat
x : BitVec w
⊢ x.msb = x.getLsbD (w - 1)

Tactic:
simp only [BitVec.msb, getMsbD]

Result:
w : Nat
x : BitVec w
⊢ (decide (0 < w) && x.getLsbD (w - 1 - 0)) = x.getLsbD (w - 1)
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_pair (f : α →ₘ[μ] β) (g : α →ₘ[μ] γ) : f.pair g =ᵐ[μ] fun x => (f x, g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ ↑(f.pair g) =ᶠ[ae μ] fun x => (↑f x, ↑g x)

Tactic:
rw [pair_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ ↑(mk (fun x => (↑f x, ↑g x)) ⋯) =ᶠ[ae μ] fun x => (↑f x, ↑g x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
inst✝¹ : TopologicalSpace β
inst✝ : TopologicalSpace γ
f : α →ₘ[μ] β
g : α →ₘ[μ] γ
⊢ ↑(mk (fun x => (↑f x, ↑g x)) ⋯) =ᶠ[ae μ] fun x => (↑f x, ↑g x)

Tactic:
apply coeFn_mk

Result:
no goals