harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma density_ae_eq_limitProcess (hκν : fst κ ≤ ν) [IsFiniteKernel ν]
    (a : α) {s : Set β} (hs : MeasurableSet s) :
    (fun x ↦ density κ ν a x s)
      =ᵐ[ν a] (countableFiltration γ).limitProcess
        (fun n x ↦ densityProcess κ ν n a x s) (ν a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
a : α
s : Set β
hs : MeasurableSet s
⊢ (fun x => κ.density ν a x s) =ᶠ[ae (ν a)]
    Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s) (countableFiltration γ) (ν a)

Tactic:
filter_upwards [tendsto_densityProcess_limitProcess hκν a hs] with t ht using ht.limsup_eq

Result:
no goals
-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem colimit_eq_iff_aux [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} :
    (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔
      FilteredColimit.Rel.{v, u} F ⟨i, xi⟩ ⟨j, xj⟩

Proof state:
J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔ FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
dsimp

Result:
J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨i, xi⟩) = (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨j, xj⟩) ↔
    FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Proof state:
J : Type v
inst✝² : Category.{w, v} J
F : J ⥤ Type u
inst✝¹ : IsFilteredOrEmpty J
inst✝ : HasColimit F
i j : J
xi : F.obj i
xj : F.obj j
⊢ (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨i, xi⟩) = (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨j, xj⟩) ↔
    FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

Tactic:
rw [← (equivShrink _).symm.injective.eq_iff, Equiv.symm_apply_apply, Equiv.symm_apply_apply,
  Quot.eq, FilteredColimit.rel_eq_eqvGen_quot_rel]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Veblen.lean
theorem veblenWith_zero_strictMono (hp : 0 < f 0) : StrictMono (veblenWith f · 0)

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0

Tactic:
exact veblenWith_pos hf hp

Result:
no goals

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ StrictMono fun x => veblenWith f x 0

Tactic:
intro o₁ o₂ h

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ (fun x => veblenWith f x 0) o₁ < (fun x => veblenWith f x 0) o₂

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ (fun x => veblenWith f x 0) o₁ < (fun x => veblenWith f x 0) o₂

Tactic:
dsimp only

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0

Proof state:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ 0 < veblenWith f o₂ 0

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h, veblenWith_lt_veblenWith_iff_right hf]

Result:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ 0 < veblenWith f o₂ 0
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem Nontrivial.einfsep_ne_top (hs : s.Nontrivial) : s.einfsep ≠ ∞

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ⊤
⊢ s.Subsingleton

Tactic:
exact subsingleton_of_einfsep_eq_top hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ⊤
⊢ ¬s.Nontrivial

Tactic:
rw [not_nontrivial_iff]

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ⊤
⊢ s.Subsingleton

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.Nontrivial
⊢ s.einfsep ≠ ⊤

Tactic:
contrapose! hs

Result:
α : Type u_1
inst✝ : PseudoMetricSpace α
s : Set α
hs : s.einfsep = ⊤
⊢ ¬s.Nontrivial
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem expand.go_pos [Hashable α] {i : Nat} {source : Array (AssocList α β)}
    {target : { d : Array (AssocList α β) // 0 < d.size }} (h : i < source.size) :
    expand.go i source target = go (i + 1)
      (source.set i .nil) ((source[i]).foldl (reinsertAux hash) target)

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : i < source.size
⊢ (if h : i < source.size then
      let es := source[i];
      let source := source.set i AssocList.nil h;
      let target := AssocList.foldl (reinsertAux hash) target es;
      go (i + 1) source target
    else target) =
    go (i + 1) (source.set i AssocList.nil h) (AssocList.foldl (reinsertAux hash) target source[i])

Tactic:
simp only [h, dite_true]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : i < source.size
⊢ go i source target = go (i + 1) (source.set i AssocList.nil h) (AssocList.foldl (reinsertAux hash) target source[i])

Tactic:
rw [expand.go]

Result:
α : Type u
β : α → Type v
inst✝ : Hashable α
i : Nat
source : Array (AssocList α β)
target : { d // 0 < d.size }
h : i < source.size
⊢ (if h : i < source.size then
      let es := source[i];
      let source := source.set i AssocList.nil h;
      let target := AssocList.foldl (reinsertAux hash) target es;
      go (i + 1) source target
    else target) =
    go (i + 1) (source.set i AssocList.nil h) (AssocList.foldl (reinsertAux hash) target source[i])
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
lemma eq_unit_comp_map_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    g = adj.unit.app A ≫ G.map f ↔ F.map g ≫ adj.counit.app B = f :=
  ⟨fun h => by simp [h], fun h => by simp [← h]⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : g = adj.unit.app A ≫ G.map f
⊢ F.map g ≫ adj.counit.app B = f

Tactic:
simp [h]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : F.map g ≫ adj.counit.app B = f
⊢ g = adj.unit.app A ≫ G.map f

Tactic:
simp [← h]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem attach_affineCombination_coe (s : Finset P) (w : P → k) :
    s.attach.affineCombination k ((↑) : s → P) (w ∘ (↑)) = s.affineCombination k id w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Finset P
w : P → k
⊢ (affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (affineCombination k s id) w

Tactic:
rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
univ_eq_attach, attach_image_val]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝² : Ring k
inst✝¹ : AddCommGroup V
inst✝ : Module k V
S : AffineSpace V P
s : Finset P
w : P → k
⊢ (affineCombination k s.attach Subtype.val) (w ∘ Subtype.val) = (affineCombination k s id) w

Tactic:
classical rw [attach_affineCombination_of_injective s w ((↑) : s → P) Subtype.coe_injective,
    univ_eq_attach, attach_image_val]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/SingleObj.lean
theorem pathToList_listToPath (l : List α) : pathToList (listToPath l) = l

Proof state:
case nil
α : Type u_1
⊢ pathToList (listToPath []) = []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ pathToList (listToPath l) = l

Tactic:
induction l with
| nil => rfl
| cons a l ih => change a :: pathToList (listToPath l) = a :: l; rw [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l

Tactic:
rw [ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ pathToList (listToPath (a :: l)) = a :: l

Tactic:
change a :: pathToList (listToPath l) = a :: l

Result:
case cons
α : Type u_1
a : α
l : List α
ih : pathToList (listToPath l) = l
⊢ a :: pathToList (listToPath l) = a :: l
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem getLeft?_map (f : α → β) (g : γ → δ) (x : α ⊕ γ) :
    (x.map f g).getLeft? = x.getLeft?.map f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β
g : γ → δ
x : α ⊕ γ
⊢ (Sum.map f g x).getLeft? = Option.map f x.getLeft?

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Contraction.lean
theorem dualTensorHomEquivOfBasis_symm_cancel_left (x : Module.Dual R M ⊗[R] N) :
    (dualTensorHomEquivOfBasis b).symm (dualTensorHom R M N x) = x

Proof state:
ι : Type w
R : Type u
M : Type v₁
N : Type v₂
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
b : Basis ι R M
x : Dual R M ⊗[R] N
⊢ (dualTensorHomEquivOfBasis b).symm ((dualTensorHom R M N) x) = x

Tactic:
rw [← dualTensorHomEquivOfBasis_apply b,
  LinearEquiv.symm_apply_apply <| dualTensorHomEquivOfBasis (N := N) b]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_flatten : ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l

Proof state:
case mp.intro.intro.intro.intro
α : Type u_1
a : α
l : Array (Array α)
s : Array α
m : s ∈ l.toList
h : a ∈ s.toList
⊢ ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList

Tactic:
exact ⟨s, m, h⟩

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1) ↔ ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList

Tactic:
constructor

Result:
case mp
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1) → ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList

case mpr
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList) → ∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1

Proof state:
case mpr.intro.intro
α : Type u_1
a : α
l : Array (Array α)
s : Array α
h₁ : s ∈ l.toList
h₂ : a ∈ s.toList
⊢ ∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1

Tactic:
refine ⟨s.toList, ⟨⟨s, h₁, rfl⟩, h₂⟩⟩

Result:
no goals

Proof state:
case mpr
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList) → ∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1

Tactic:
rintro ⟨s, h₁, h₂⟩

Result:
case mpr.intro.intro
α : Type u_1
a : α
l : Array (Array α)
s : Array α
h₁ : s ∈ l.toList
h₂ : a ∈ s.toList
⊢ ∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1

Proof state:
case mp
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1) → ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList

Tactic:
rintro ⟨_, ⟨s, m, rfl⟩, h⟩

Result:
case mp.intro.intro.intro.intro
α : Type u_1
a : α
l : Array (Array α)
s : Array α
m : s ∈ l.toList
h : a ∈ s.toList
⊢ ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList

Proof state:
α : Type u_1
a : α
⊢ ∀ {L : Array (Array α)}, a ∈ L.flatten ↔ ∃ l, l ∈ L ∧ a ∈ l

Tactic:
simp only [mem_def, toList_flatten, List.mem_flatten, List.mem_map]

Result:
α : Type u_1
a : α
⊢ ∀ {L : Array (Array α)}, (∃ l, (∃ a, a ∈ L.toList ∧ a.toList = l) ∧ a ∈ l) ↔ ∃ l, l ∈ L.toList ∧ a ∈ l.toList

Proof state:
α : Type u_1
a : α
⊢ ∀ {L : Array (Array α)}, (∃ l, (∃ a, a ∈ L.toList ∧ a.toList = l) ∧ a ∈ l) ↔ ∃ l, l ∈ L.toList ∧ a ∈ l.toList

Tactic:
intro l

Result:
α : Type u_1
a : α
l : Array (Array α)
⊢ (∃ l_1, (∃ a, a ∈ l.toList ∧ a.toList = l_1) ∧ a ∈ l_1) ↔ ∃ l_1, l_1 ∈ l.toList ∧ a ∈ l_1.toList
-- Mathlib/Algebra/Ring/Semiconj.lean
theorem add_right [Distrib R] {a x y x' y' : R} (h : SemiconjBy a x y) (h' : SemiconjBy a x' y') :
    SemiconjBy a (x + x') (y + y')

Proof state:
R : Type u
inst✝ : Distrib R
a x y x' y' : R
h : SemiconjBy a x y
h' : SemiconjBy a x' y'
⊢ SemiconjBy a (x + x') (y + y')

Tactic:
simp only [SemiconjBy, left_distrib, right_distrib, h.eq, h'.eq]

Result:
no goals
-- Mathlib/Data/List/Sigma.lean
theorem kunion_nil : ∀ {l : List (Sigma β)}, kunion l [] = l
  | [] => rfl
  | _ :: l => by rw [kunion, kerase_nil, kunion_nil]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
head✝ : Sigma β
l : List (Sigma β)
⊢ (head✝ :: l).kunion [] = head✝ :: l

Tactic:
rw [kunion, kerase_nil, kunion_nil]

Result:
no goals
-- Mathlib/Algebra/CharP/MixedCharZero.lean
theorem nonempty_algebraRat_iff :
    Nonempty (Algebra ℚ R) ↔ ∀ I : Ideal R, I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Nonempty (Algebra ℚ R)

Tactic:
apply Nonempty.intro

Result:
case mpr.val
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Algebra ℚ R

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) ↔ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

case mpr
R : Type u_1
inst✝ : CommRing R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Nonempty (Algebra ℚ R)

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
⊢ Nonempty (Algebra ℚ R) → ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
intro h_alg

Result:
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
haveI h_alg' : Algebra ℚ R := h_alg.some

Result:
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
h_alg' : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Proof state:
case mpr.val
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Algebra ℚ R

Tactic:
exact algebraRat h

Result:
no goals

Proof state:
case mpr
R : Type u_1
inst✝ : CommRing R
⊢ (∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)) → Nonempty (Algebra ℚ R)

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝ : CommRing R
h : ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)
⊢ Nonempty (Algebra ℚ R)

Proof state:
case mp
R : Type u_1
inst✝ : CommRing R
h_alg : Nonempty (Algebra ℚ R)
h_alg' : Algebra ℚ R
⊢ ∀ (I : Ideal R), I ≠ ⊤ → CharZero (R ⧸ I)

Tactic:
apply of_algebraRat

Result:
no goals
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem span_fourierLp_closure_eq_top {p : ℝ≥0∞} [Fact (1 ≤ p)] (hp : p ≠ ∞) :
    (span ℂ (range (@fourierLp T _ p _))).topologicalClosure = ⊤

Proof state:
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
⊢ (span ℂ (range (fourierLp p))).topologicalClosure = ⊤

Tactic:
convert
  (ContinuousMap.toLp_denseRange ℂ (@haarAddCircle T hT) ℂ hp).topologicalClosure_map_submodule
    span_fourier_closure_eq_top

Result:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))

Proof state:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range (fourierLp p)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
unfold fourierLp

Result:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range fun n => (toLp p haarAddCircle ℂ) (fourier n)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Proof state:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range fun n => (toLp p haarAddCircle ℂ) (fourier n)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
rw [range_comp']

Result:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (⇑(toLp p haarAddCircle ℂ) '' range fourier) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Proof state:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range (fourierLp p)) = Submodule.map (↑(toLp p haarAddCircle ℂ)) (span ℂ (range fourier))

Tactic:
rw [map_span]

Result:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (range (fourierLp p)) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Proof state:
case h.e'_2.h.e'_9.h.h
T : ℝ
hT : Fact (0 < T)
p : ℝ≥0∞
inst✝ : Fact (1 ≤ p)
hp : p ≠ ⊤
e_3✝ : Complex.instSemiring = DivisionSemiring.toSemiring
he✝ : Lp.instModule = Lp.instModule
⊢ span ℂ (⇑(toLp p haarAddCircle ℂ) '' range fourier) = span ℂ (⇑↑(toLp p haarAddCircle ℂ) '' range fourier)

Tactic:
simp only [ContinuousLinearMap.coe_coe]

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
/-- An additive character maps negatives to inverses (when defined) -/
lemma map_neg_eq_inv (ψ : AddChar A M) (a : A) : ψ (-a) = (ψ a)⁻¹

Proof state:
A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) = (ψ a)⁻¹

Tactic:
apply eq_inv_of_mul_eq_one_left

Result:
case h
A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) * ψ a = 1

Proof state:
case h
A : Type u_1
M : Type u_2
inst✝¹ : AddGroup A
inst✝ : DivisionMonoid M
ψ : AddChar A M
a : A
⊢ ψ (-a) * ψ a = 1

Tactic:
simp only [← map_add_eq_mul, neg_add_cancel, map_zero_eq_one]

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem map_id_apply (a : F.obj X) : (F.map (𝟙 X)) a = a

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X : C
a : F.obj X
⊢ F.map (𝟙 X) a = a

Tactic:
simp [types_id]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
@[simp] lemma krullDim_withBot [Nonempty α] : krullDim (WithBot α) = krullDim α + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithBot α)ᵒᵈ = krullDim αᵒᵈ + 1

Tactic:
exact krullDim_WithTop (α := αᵒᵈ)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithBot α) = krullDim α + 1

Tactic:
conv_lhs => rw [← krullDim_orderDual]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithBot α)ᵒᵈ = krullDim α + 1

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithBot α)ᵒᵈ = krullDim α + 1

Tactic:
conv_rhs => rw [← krullDim_orderDual]

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ krullDim (WithBot α)ᵒᵈ = krullDim αᵒᵈ + 1
-- Mathlib/Order/OrdContinuous.lean
theorem iterate {f : α → α} (hf : LeftOrdContinuous f) (n : ℕ) :
    LeftOrdContinuous f^[n]

Proof state:
case succ
α : Type u
inst✝ : Preorder α
f : α → α
hf : LeftOrdContinuous f
n : ℕ
ihn : LeftOrdContinuous f^[n]
⊢ LeftOrdContinuous f^[n + 1]

Tactic:
exact ihn.comp hf

Result:
no goals

Proof state:
case zero
α : Type u
inst✝ : Preorder α
f : α → α
hf : LeftOrdContinuous f
⊢ LeftOrdContinuous f^[0]

Tactic:
exact LeftOrdContinuous.id α

Result:
no goals

Proof state:
α : Type u
inst✝ : Preorder α
f : α → α
hf : LeftOrdContinuous f
n : ℕ
⊢ LeftOrdContinuous f^[n]

Tactic:
induction n with
| zero => exact LeftOrdContinuous.id α
| succ n ihn => exact ihn.comp hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsb'_eq_getLsb' (x : BitVec w) (i : Fin w) :
    x.getMsb' i = x.getLsb' ⟨w - 1 - i, by omega⟩

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ x.getMsb' i = x.getLsb' ⟨w - 1 - ↑i, ⋯⟩

Tactic:
simp only [getMsb', getLsb']

Result:
no goals

Proof state:
w : Nat
x : BitVec w
i : Fin w
⊢ w - 1 - ↑i < w

Tactic:
omega

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/Semiconj.lean
theorem coverEntropyInf_image_le_of_uniformContinuous [UniformSpace X] [UniformSpace Y] {S : X → X}
    {T : Y → Y} {φ : X → Y} (h : Semiconj φ S T) (h' : UniformContinuous φ) (F : Set X) :
    coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F

Tactic:
exact coverEntropyInf_antitone S F (uniformContinuous_iff.1 h')

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf T (φ '' F) ≤ coverEntropyInf S F

Tactic:
rw [coverEntropyInf_image_of_comap _ h F]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : UniformSpace X
inst✝ : UniformSpace Y
S : X → X
T : Y → Y
φ : X → Y
h : Semiconj φ S T
h' : UniformContinuous φ
F : Set X
⊢ coverEntropyInf S F ≤ coverEntropyInf S F
-- Mathlib/AlgebraicGeometry/Spec.lean
theorem Spec.locallyRingedSpaceMap_comp {R S T : CommRingCat.{u}} (f : R ⟶ S) (g : S ⟶ T) :
    Spec.locallyRingedSpaceMap (f ≫ g) =
      Spec.locallyRingedSpaceMap g ≫ Spec.locallyRingedSpaceMap f :=
  LocallyRingedSpace.Hom.ext' <| by
    rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_comp]; rfl

Proof state:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap (f ≫ g)) =
    LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f)

Tactic:
rw [Spec.locallyRingedSpaceMap_toShHom, Spec.sheafedSpaceMap_comp]

Result:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ sheafedSpaceMap g ≫ sheafedSpaceMap f =
    LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f)

Proof state:
R S T : CommRingCat
f : R ⟶ S
g : S ⟶ T
⊢ sheafedSpaceMap g ≫ sheafedSpaceMap f =
    LocallyRingedSpace.Hom.toShHom (locallyRingedSpaceMap g ≫ locallyRingedSpaceMap f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma ediv_dvd_of_dvd (hmn : m ∣ n) : n / m ∣ n

Proof state:
case inr.intro
m n : ℤ
hm : ¬m = 0
a : ℤ
ha : n = m * a
⊢ n / m ∣ n

Tactic:
simp [ha, Int.mul_ediv_cancel_left _ hm, Int.dvd_mul_left]

Result:
no goals

Proof state:
m n : ℤ
hmn : m ∣ n
⊢ n / m ∣ n

Tactic:
obtain rfl | hm := Decidable.em (m = 0)

Result:
case inl
n : ℤ
hmn : 0 ∣ n
⊢ n / 0 ∣ n

case inr
m n : ℤ
hmn : m ∣ n
hm : ¬m = 0
⊢ n / m ∣ n

Proof state:
case inl
n : ℤ
hmn : 0 ∣ n
⊢ n / 0 ∣ n

Tactic:
simpa using hmn

Result:
no goals

Proof state:
case inr
m n : ℤ
hmn : m ∣ n
hm : ¬m = 0
⊢ n / m ∣ n

Tactic:
obtain ⟨a, ha⟩ := hmn

Result:
case inr.intro
m n : ℤ
hm : ¬m = 0
a : ℤ
ha : n = m * a
⊢ n / m ∣ n
-- Mathlib/Data/Num/Lemmas.lean
theorem add_ofNat' (m n) : Num.ofNat' (m + n) = Num.ofNat' m + Num.ofNat' n

Proof state:
m n : ℕ
⊢ ofNat' (m + n) = ofNat' m + ofNat' n

Tactic:
induction n

Result:
case zero
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0

case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)

Proof state:
case succ
m n✝ : ℕ
a✝ : ofNat' (m + n✝) = ofNat' m + ofNat' n✝
⊢ ofNat' (m + (n✝ + 1)) = ofNat' m + ofNat' (n✝ + 1)

Tactic:
simp only [Nat.add_succ, Nat.add_zero, ofNat'_succ, add_one, add_succ, *]

Result:
no goals

Proof state:
case zero
m : ℕ
⊢ ofNat' (m + 0) = ofNat' m + ofNat' 0

Tactic:
simp only [Nat.add_zero, ofNat'_zero, add_zero]

Result:
no goals