harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem map_coe_atBot_of_Ioo_subset (ha : s ⊆ Ioi a) (hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s) :
    map ((↑) : s → α) atBot = 𝓝[>] a

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
⊢ map Subtype.val atBot = 𝓝[>] a

Tactic:
refine (map_coe_atTop_of_Ioo_subset (show ofDual ⁻¹' s ⊆ Iio (toDual a) from ha)
  fun b' hb' => ?_ :)

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
b' : αᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : OrderTopology α
inst✝ : DenselyOrdered α
a : α
s : Set α
ha : s ⊆ Ioi a
hs : ∀ b' > a, ∃ b > a, Ioo a b ⊆ s
b' : αᵒᵈ
hb' : b' < toDual a
⊢ ∃ a_1 < toDual a, Ioo a_1 (toDual a) ⊆ ⇑ofDual ⁻¹' s

Tactic:
simpa only [OrderDual.exists, dual_Ioo] using hs b' hb'

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem exists_of_mem_map {f} {b : β} : ∀ {s : Seq α}, b ∈ map f s → ∃ a, a ∈ s ∧ f a = b :=
  fun {s} h => by match s with
  | ⟨g, al⟩ =>
    let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h
    rcases o with - | a
    · injection oe
    · injection oe with h'; exact ⟨a, om, h'⟩

Proof state:
case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
exact ⟨a, om, h'⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
let ⟨o, om, oe⟩ := @Stream'.exists_of_mem_map _ _ (Option.map f) (some b) g h

Result:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ g
oe : Option.map f o = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Proof state:
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
o : Option α
om : o ∈ g
oe : Option.map f o = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
rcases o with - | a

Result:
case none
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Proof state:
case none
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
om : none ∈ g
oe : Option.map f none = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
injection oe

Result:
no goals

Proof state:
case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
oe : Option.map f (some a) = some b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b

Tactic:
injection oe with h'

Result:
case some
α : Type u
β : Type v
f : α → β
b : β
s : Seq α
g : Stream' (Option α)
al : g.IsSeq
h : b ∈ map f ⟨g, al⟩
a : α
om : some a ∈ g
h' : f a = b
⊢ ∃ a, a ∈ ⟨g, al⟩ ∧ f a = b
-- Mathlib/RingTheory/Artinian/Module.lean
theorem Function.Surjective.isArtinianRing {R} [Semiring R] {S} [Semiring S] {F}
    [FunLike F R S] [RingHomClass F R S]
    {f : F} (hf : Function.Surjective f) [H : IsArtinianRing R] : IsArtinianRing S

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinian R R
⊢ IsArtinian S S

Tactic:
exact ⟨(Ideal.orderEmbeddingOfSurjective f hf).wellFounded H.wf⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinianRing R
⊢ IsArtinianRing S

Tactic:
rw [isArtinianRing_iff] at H ⊢

Result:
R : Type u_1
inst✝³ : Semiring R
S : Type u_2
inst✝² : Semiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
H : IsArtinian R R
⊢ IsArtinian S S
-- Mathlib/Combinatorics/SimpleGraph/Prod.lean
theorem ofBoxProdLeft_boxProdLeft [DecidableEq β] [DecidableRel G.Adj] {a₁ a₂ : α} {b : β} :
    ∀ (w : G.Walk a₁ a₂), (w.boxProdLeft H b).ofBoxProdLeft = w
  | nil => rfl
  | cons' x y z h w => by
    rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]
    · simp [ofBoxProdLeft_boxProdLeft]
    · exact ⟨h, rfl⟩

Proof state:
case hc
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (x, b).1 ((G.boxProdLeft H b).toHom y).1 ∧ (x, b).2 = ((G.boxProdLeft H b).toHom y).2

Tactic:
exact ⟨h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ (Walk.boxProdLeft H b (cons' x y z h w)).ofBoxProdLeft = cons' x y z h w

Tactic:
rw [Walk.boxProdLeft, map_cons, ofBoxProdLeft, Or.by_cases, dif_pos, ← Walk.boxProdLeft]

Result:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w

case hc
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ G.Adj (x, b).1 ((G.boxProdLeft H b).toHom y).1 ∧ (x, b).2 = ((G.boxProdLeft H b).toHom y).2

Proof state:
α : Type u_1
β : Type u_2
G : SimpleGraph α
H : SimpleGraph β
inst✝¹ : DecidableEq β
inst✝ : DecidableRel G.Adj
a₁ a₂ : α
b : β
x z y : α
h : G.Adj x y
w : G.Walk y z
⊢ cons ⋯ (Walk.boxProdLeft H b w).ofBoxProdLeft = cons' x y z h w

Tactic:
simp [ofBoxProdLeft_boxProdLeft]

Result:
no goals
-- Mathlib/Analysis/Convex/Side.lean
theorem _root_.Wbtw.wSameSide₂₃ {s : AffineSubspace R P} {x y z : P} (h : Wbtw R x y z)
    (hx : x ∈ s) : s.WSameSide y z

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y z : P
h : Wbtw R x y z
hx : x ∈ s
⊢ s.WSameSide y z

Tactic:
rcases h with ⟨t, ⟨ht0, -⟩, rfl⟩

Result:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ s.WSameSide ((lineMap x z) t) z

Proof state:
case intro.intro.intro
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : StrictOrderedCommRing R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x z : P
hx : x ∈ s
t : R
ht0 : 0 ≤ t
⊢ s.WSameSide ((lineMap x z) t) z

Tactic:
exact wSameSide_lineMap_left z hx ht0

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma sSup_add (hs : s.Nonempty) : sSup s + a = ⨆ b ∈ s, b + a

Proof state:
s : Set ℝ≥0∞
a : ℝ≥0∞
hs : s.Nonempty
⊢ sSup s + a = ⨆ b ∈ s, b + a

Tactic:
rw [sSup_eq_iSup, biSup_add hs]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
lemma yonedaEquiv_yoneda_map {X Y : C} (f : X ⟶ Y) : J.yonedaEquiv (J.yoneda.map f) = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (J.yoneda.map f).val.app (op X) (𝟙 X) = f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ J.yonedaEquiv (J.yoneda.map f) = f

Tactic:
rw [yonedaEquiv_apply]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
f : X ⟶ Y
⊢ (J.yoneda.map f).val.app (op X) (𝟙 X) = f
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitLeftOpIsoUnopColimit_hom_comp_ι (F : J ⥤ Cᵒᵖ) [HasColimit F] (j : J) :
    (limitLeftOpIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.leftOp (op j)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasColimit F
j : J
⊢ (limitLeftOpIsoUnopColimit F).hom ≫ (colimit.ι F j).unop = limit.π F.leftOp (op j)

Tactic:
simp [← Iso.eq_inv_comp]

Result:
no goals
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem star_adjoin_comm (s : Set A) : star (Algebra.adjoin R s) = Algebra.adjoin R (star s) :=
  have this : ∀ t : Set A, Algebra.adjoin R (star t) ≤ star (Algebra.adjoin R t) := fun _ =>
    Algebra.adjoin_le fun _ hx => Algebra.subset_adjoin hx
  le_antisymm (by simpa only [star_star] using Subalgebra.star_mono (this (star s))) (this s)

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
s : Set A
this : ∀ (t : Set A), Algebra.adjoin R (star t) ≤ star (Algebra.adjoin R t)
⊢ star (Algebra.adjoin R s) ≤ Algebra.adjoin R (star s)

Tactic:
simpa only [star_star] using Subalgebra.star_mono (this (star s))

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem push_parentD (arr : Array UFNode) : parentD (arr.push ⟨arr.size, 0⟩) i = parentD arr i

Proof state:
i : Nat
arr : Array UFNode
⊢ (if i < arr.size + 1 then (if h : i < arr.size then arr[i] else { parent := arr.size, rank := 0 }).parent else i) =
    if h : i < arr.size then arr[i].parent else i

Tactic:
split <;> split <;> try simp

Result:
case isTrue.isFalse
i : Nat
arr : Array UFNode
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
⊢ arr.size = i

case isFalse.isTrue
i : Nat
arr : Array UFNode
h✝¹ : ¬i < arr.size + 1
h✝ : i < arr.size
⊢ i = arr[i].parent

Proof state:
case isTrue.isFalse
i : Nat
arr : Array UFNode
h✝¹ : i < arr.size + 1
h✝ : ¬i < arr.size
⊢ arr.size = i

Tactic:
exact Nat.le_antisymm (Nat.ge_of_not_lt ‹_›) (Nat.le_of_lt_succ ‹_›)

Result:
no goals

Proof state:
i : Nat
arr : Array UFNode
⊢ parentD (arr.push { parent := arr.size, rank := 0 }) i = parentD arr i

Tactic:
simp only [parentD, Array.size_push, Array.get_eq_getElem, Array.getElem_push, dite_eq_ite]

Result:
i : Nat
arr : Array UFNode
⊢ (if i < arr.size + 1 then (if h : i < arr.size then arr[i] else { parent := arr.size, rank := 0 }).parent else i) =
    if h : i < arr.size then arr[i].parent else i

Proof state:
case isFalse.isFalse
i : Nat
arr : Array UFNode
h✝¹ : ¬i < arr.size + 1
h✝ : ¬i < arr.size
⊢ i = i

Tactic:
simp

Result:
no goals

Proof state:
case isFalse.isTrue
i : Nat
arr : Array UFNode
h✝¹ : ¬i < arr.size + 1
h✝ : i < arr.size
⊢ i = arr[i].parent

Tactic:
cases ‹¬_› (Nat.lt_succ_of_lt ‹_›)

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem forIn_eq_bindList [Monad m] [LawfulMonad m]
    (f : α → β → m (ForInStep β)) (l : List α) (init : β) :
    forIn l init f = ForInStep.run <$> (ForInStep.yield init).bindList f l

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (do
      let x ← f head✝ init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield b)) =
    do
    let a ← f head✝ init
    ForInStep.run <$> ForInStep.bindList f tail✝ a

Tactic:
congr

Result:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield b)) =
    fun a => ForInStep.run <$> ForInStep.bindList f tail✝ a

Proof state:
case cons.e_a
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (fun x =>
      match x with
      | ForInStep.done b => pure b
      | ForInStep.yield b => ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield b)) =
    fun a => ForInStep.run <$> ForInStep.bindList f tail✝ a

Tactic:
ext (b | b) <;> simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
l : List α
init : β
⊢ forIn l init f = ForInStep.run <$> ForInStep.bindList f l (ForInStep.yield init)

Tactic:
induction l generalizing init <;> simp [*]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → β → m (ForInStep β)
head✝ : α
tail✝ : List α
tail_ih✝ : ∀ (init : β), forIn tail✝ init f = ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield init)
init : β
⊢ (do
      let x ← f head✝ init
      match x with
        | ForInStep.done b => pure b
        | ForInStep.yield b => ForInStep.run <$> ForInStep.bindList f tail✝ (ForInStep.yield b)) =
    do
    let a ← f head✝ init
    ForInStep.run <$> ForInStep.bindList f tail✝ a
-- Mathlib/ModelTheory/Ultraproducts.lean
theorem realize_formula_cast {β : Type*} (φ : L.Formula β) (x : β → ∀ a, M a) :
    (φ.Realize fun i => (x i : (u : Filter α).Product M)) ↔
      ∀ᶠ a : α in u, φ.Realize fun i => x i a

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : L.Formula β
x : β → (a : α) → M a
⊢ (φ.Realize fun i => Quotient.mk' (x i)) ↔ ∀ᶠ (a : α) in ↑u, φ.Realize fun i => x i a

Tactic:
simp_rw [Formula.Realize, ← boundedFormula_realize_cast φ x, iff_eq_eq]

Result:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : L.Formula β
x : β → (a : α) → M a
⊢ BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) default =
    BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' fun a => default i

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
β : Type u_3
φ : L.Formula β
x : β → (a : α) → M a
⊢ BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) default =
    BoundedFormula.Realize φ (fun i => Quotient.mk' (x i)) fun i => Quotient.mk' fun a => default i

Tactic:
exact congr rfl (Subsingleton.elim _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem tail_zipWith : (zipWith f l l').tail = zipWith f l.tail l'.tail

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : List α✝²
l' : List α✝¹
⊢ (zipWith f l l').tail = zipWith f l.tail l'.tail

Tactic:
rw [← drop_one]

Result:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : List α✝²
l' : List α✝¹
⊢ drop 1 (zipWith f l l') = zipWith f l.tail l'.tail

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : List α✝²
l' : List α✝¹
⊢ drop 1 (zipWith f l l') = zipWith f l.tail l'.tail

Tactic:
simp [drop_zipWith]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/PiTensorProduct/InjectiveSeminorm.lean
theorem liftIsometry_tprodL :
    liftIsometry 𝕜 E _ (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] i, E i)

Proof state:
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
⊢ (liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜) = ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)

Tactic:
ext _

Result:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝

Proof state:
case h
ι : Type uι
inst✝³ : Fintype ι
𝕜 : Type u𝕜
inst✝² : NontriviallyNormedField 𝕜
E : ι → Type uE
inst✝¹ : (i : ι) → SeminormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace 𝕜 (E i)
x✝ : ⨂[𝕜] (i : ι), E i
⊢ ((liftIsometry 𝕜 E (⨂[𝕜] (i : ι), E i)) (tprodL 𝕜)) x✝ = (ContinuousLinearMap.id 𝕜 (⨂[𝕜] (i : ι), E i)) x✝

Tactic:
simp only [liftIsometry_apply_apply, tprodL_coe, lift_tprod, LinearMap.id_coe, id_eq,
  ContinuousLinearMap.coe_id']

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma IsSelfAdjoint.neg_algebraMap_norm_le_self {a : A} (ha : IsSelfAdjoint a

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ -a ≤ (algebraMap ℝ A) ‖a‖

Tactic:
rw [← norm_neg]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ -a ≤ (algebraMap ℝ A) ‖-a‖

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ -a ≤ (algebraMap ℝ A) ‖-a‖

Tactic:
exact IsSelfAdjoint.le_algebraMap_norm_self (neg ha)

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
this : -a ≤ (algebraMap ℝ A) ‖a‖
⊢ -(algebraMap ℝ A) ‖a‖ ≤ a

Tactic:
exact neg_le.mp this

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
⊢ -(algebraMap ℝ A) ‖a‖ ≤ a

Tactic:
have : - a ≤ algebraMap ℝ A ‖a‖ := by
  rw [← norm_neg]
  exact IsSelfAdjoint.le_algebraMap_norm_self (neg ha)

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
ha : autoParam (IsSelfAdjoint a) _auto✝
this : -a ≤ (algebraMap ℝ A) ‖a‖
⊢ -(algebraMap ℝ A) ‖a‖ ≤ a
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem borel_eq_generateFrom_Iic_rat : borel ℝ = .generateFrom (⋃ a : ℚ, {Iic (a : ℝ)})

Proof state:
⊢ borel ℝ = generateFrom (⋃ a, {Iic ↑a})

Tactic:
rw [borel_eq_generateFrom_Ioi_rat, iUnion_singleton_eq_range, iUnion_singleton_eq_range]

Result:
⊢ generateFrom (range fun a => Ioi ↑a) = generateFrom (range fun a => Iic ↑a)

Proof state:
⊢ generateFrom (range fun a => Ioi ↑a) = generateFrom (range fun a => Iic ↑a)

Tactic:
refine le_antisymm (generateFrom_le ?_) (generateFrom_le ?_) <;>
rintro _ ⟨q, rfl⟩ <;>
dsimp only <;>
[rw [← compl_Iic]; rw [← compl_Ioi]] <;>
exact MeasurableSet.compl (GenerateMeasurable.basic _ (mem_range_self q))

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
/-- A symmetric relation `r : α → α → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some involutive function `f`. -/
protected lemma Symmetric.forall_existsUnique_iff' {r : α → α → Prop} (hr : Symmetric r) :
    (∀ a, ∃! b, r a b) ↔ ∃ f : α → α, Involutive f ∧ r = (f · = ·)

Proof state:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, Involutive f ∧ r = fun x1 x2 => f x1 = x2

Tactic:
refine ⟨fun h ↦ ?_, fun ⟨f, _, hf⟩ ↦ forall_existsUnique_iff'.2 ⟨f, hf⟩⟩

Result:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, Involutive f ∧ r = fun x1 x2 => f x1 = x2

Proof state:
case intro
α : Sort u_1
f : α → α
hr : Symmetric fun x1 x2 => f x1 = x2
h : ∀ (a : α), ∃! b, (fun x1 x2 => f x1 = x2) a b
⊢ ∃ f_1, Involutive f_1 ∧ (fun x1 x2 => f x1 = x2) = fun x1 x2 => f_1 x1 = x2

Tactic:
exact ⟨f, symmetric_apply_eq_iff.1 hr, rfl⟩

Result:
no goals

Proof state:
α : Sort u_1
r : α → α → Prop
hr : Symmetric r
h : ∀ (a : α), ∃! b, r a b
⊢ ∃ f, Involutive f ∧ r = fun x1 x2 => f x1 = x2

Tactic:
rcases forall_existsUnique_iff'.1 h with ⟨f, rfl : r = _⟩

Result:
case intro
α : Sort u_1
f : α → α
hr : Symmetric fun x1 x2 => f x1 = x2
h : ∀ (a : α), ∃! b, (fun x1 x2 => f x1 = x2) a b
⊢ ∃ f_1, Involutive f_1 ∧ (fun x1 x2 => f x1 = x2) = fun x1 x2 => f_1 x1 = x2
-- Mathlib/GroupTheory/SpecificGroups/Dihedral.lean
lemma card_conjClasses_odd (hn : Odd n) :
    Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

Proof state:
n : ℕ
hn : Odd n
⊢ Nat.card (ConjClasses (DihedralGroup n)) = (n + 3) / 2

Tactic:
rw [← Nat.mul_div_mul_left _ 2 hn.pos, ← card_commute_odd hn, mul_comm,
  card_comm_eq_card_conjClasses_mul_card, nat_card, Nat.mul_div_left _ (mul_pos two_pos hn.pos)]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nndist_eq_add [PseudoMetricSpace α] [PseudoMetricSpace β]
    (hp : p ≠ ∞) (x y : WithLp p (α × β)) :
    nndist x y = (nndist x.fst y.fst ^ p.toReal + nndist x.snd y.snd ^ p.toReal) ^ (1 / p.toReal) :=
  NNReal.eq <| by
    push_cast
    exact prod_dist_eq_add (p.toReal_pos_iff_ne_top.mpr hp) _ _

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : p ≠ ⊤
x y : WithLp p (α × β)
⊢ ↑(nndist x y) = ↑((nndist x.1 y.1 ^ p.toReal + nndist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal))

Tactic:
push_cast

Result:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : p ≠ ⊤
x y : WithLp p (α × β)
⊢ dist x y = (dist x.1 y.1 ^ p.toReal + dist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Proof state:
p : ℝ≥0∞
α : Type u_2
β : Type u_3
hp✝ : Fact (1 ≤ p)
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
hp : p ≠ ⊤
x y : WithLp p (α × β)
⊢ dist x y = (dist x.1 y.1 ^ p.toReal + dist x.2 y.2 ^ p.toReal) ^ (1 / p.toReal)

Tactic:
exact prod_dist_eq_add (p.toReal_pos_iff_ne_top.mpr hp) _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Eigenspace/Basic.lean
lemma mem_genEigenspace_top {f : End R M} {μ : R} {x : M} :
    x ∈ f.genEigenspace μ ⊤ ↔ ∃ k : ℕ, x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Proof state:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
x : M
⊢ x ∈ (f.genEigenspace μ) ⊤ ↔ ∃ k, x ∈ LinearMap.ker ((f - μ • 1) ^ k)

Tactic:
simp [mem_genEigenspace]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem coe_toAffineMap : ⇑f.toAffineMap = f

Proof state:
𝕜 : Type u_1
V : Type u_2
V₂ : Type u_5
P : Type u_10
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V
inst✝⁶ : NormedSpace 𝕜 V
inst✝⁵ : PseudoMetricSpace P
inst✝⁴ : NormedAddTorsor V P
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
f : P →ᵃⁱ[𝕜] P₂
⊢ ⇑f.toAffineMap = ⇑f

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem mem_append {a : α} {s t : List α} : a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Proof state:
α : Type u_1
a : α
s t : List α
⊢ a ∈ s ++ t ↔ a ∈ s ∨ a ∈ t

Tactic:
induction s <;> simp_all [or_assoc]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem coe_sInf {s : Set α} (hs : s.Nonempty) (h's : BddBelow s) :
    ↑(sInf s) = (⨅ a ∈ s, ↑a : WithTop α)

Proof state:
α : Type u_1
inst✝ : ConditionallyCompleteLinearOrderBot α
s : Set α
hs : s.Nonempty
h's : BddBelow s
⊢ ↑(sInf s) = ⨅ a ∈ s, ↑a

Tactic:
rw [coe_sInf' hs h's, sInf_image]

Result:
no goals