harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/FiberedCategory/HomLift.lean
lemma eqToHom_codomain_lift_id {p : 𝒳 ⥤ 𝒮} {a b : 𝒳} (hab : a = b) {S : 𝒮} (hS : p.obj b = S) :
    p.IsHomLift (𝟙 S) (eqToHom hab)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a b : 𝒳
hab : a = b
S : 𝒮
hS : p.obj b = S
⊢ p.IsHomLift (𝟙 S) (eqToHom hab)

Tactic:
subst hS hab

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝¹ : Category.{v₁, u₂} 𝒳
inst✝ : Category.{v₂, u₁} 𝒮
p : 𝒳 ⥤ 𝒮
a : 𝒳
⊢ p.IsHomLift (𝟙 (p.obj a)) (eqToHom ⋯)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_insertMany_empty_list_of_contains_eq_false [LawfulBEq α]
    {l : List (α × β)} {k : α} [Inhabited β]
    (h : (l.map Prod.fst).contains k = false) :
    get! (insertMany (empty : Raw₀ α (fun _ => β)) l) k = (default : β)

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : LawfulBEq α
l : List (α × β)
k : α
inst✝ : Inhabited β
h : (List.map Prod.fst l).contains k = false
⊢ get! empty k = default

Tactic:
apply get!_empty

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : LawfulBEq α
l : List (α × β)
k : α
inst✝ : Inhabited β
h : (List.map Prod.fst l).contains k = false
⊢ get! (insertMany empty l).val k = default

Tactic:
rw [get!_insertMany_list_of_contains_eq_false _ Raw.WF.empty₀ h]

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : LawfulBEq α
l : List (α × β)
k : α
inst✝ : Inhabited β
h : (List.map Prod.fst l).contains k = false
⊢ get! empty k = default
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem tmod_add_tdiv' (m k : Int) : tmod m k + m.tdiv k * k = m

Proof state:
m k : Int
⊢ m.tmod k + m.tdiv k * k = m

Tactic:
rw [Int.mul_comm]

Result:
m k : Int
⊢ m.tmod k + k * m.tdiv k = m

Proof state:
m k : Int
⊢ m.tmod k + k * m.tdiv k = m

Tactic:
apply tmod_add_tdiv

Result:
no goals
-- Mathlib/Topology/Constructions.lean
lemma isClosedMap_swap : IsClosedMap (Prod.swap : X × Y → Y × X) := fun s hs ↦ by
  rw [image_swap_eq_preimage_swap]
  exact hs.preimage continuous_swap

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ IsClosed (Prod.swap '' s)

Tactic:
rw [image_swap_eq_preimage_swap]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ IsClosed (Prod.swap ⁻¹' s)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set (X × Y)
hs : IsClosed s
⊢ IsClosed (Prod.swap ⁻¹' s)

Tactic:
exact hs.preimage continuous_swap

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_eq_getLastD (a l h) : @getLast α (a::l) h = getLastD l a

Proof state:
α : Type u_1
a : α
l : List α
h : a :: l ≠ []
⊢ (a :: l).getLast h = l.getLastD a

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_nat' [AddMonoidWithOne G] [AddMonoid H] [AddConstMapClass F G H 1 b]
    (f : F) (x : G) (n : ℕ) : f (x + n) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddMonoidWithOne G
inst✝¹ : AddMonoid H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℕ
⊢ f (x + ↑n) = f x + n • b

Tactic:
simp [← map_add_nsmul]

Result:
no goals
-- Mathlib/Order/CompleteSublattice.lean
protected lemma disjoint_iff {a b : L} :
    Disjoint a b ↔ Disjoint (a : α) (b : α)

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
a b : ↥L
⊢ Disjoint a b ↔ Disjoint ↑a ↑b

Tactic:
rw [disjoint_iff, disjoint_iff, ← Sublattice.coe_inf, ← coe_bot (L := L),
  Subtype.coe_injective.eq_iff]

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem comp_continuousAt_iff' (h : X ≃ₜ Y) (f : Y → Z) (x : X) :
    ContinuousAt (f ∘ h) x ↔ ContinuousAt f (h x) :=
  h.isInducing.continuousAt_iff' (by simp)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
h : X ≃ₜ Y
f : Y → Z
x : X
⊢ range ⇑h ∈ 𝓝 (h x)

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_le {x : PGame} : 0 ≤ x ↔ ∀ j, ∃ i, 0 ≤ (x.moveRight j).moveLeft i

Proof state:
x : PGame
⊢ ((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ x.moveLeft i') ∨ ∃ j, (moveLeft 0 i).moveRight j ≤ x) ∧
      ∀ (j : x.RightMoves), (∃ i, 0 ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', moveRight 0 j' ≤ x.moveRight j) ↔
    ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i

Tactic:
simp

Result:
no goals

Proof state:
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i

Tactic:
rw [le_def]

Result:
x : PGame
⊢ ((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ x.moveLeft i') ∨ ∃ j, (moveLeft 0 i).moveRight j ≤ x) ∧
      ∀ (j : x.RightMoves), (∃ i, 0 ≤ (x.moveRight j).moveLeft i) ∨ ∃ j', moveRight 0 j' ≤ x.moveRight j) ↔
    ∀ (j : x.RightMoves), ∃ i, 0 ≤ (x.moveRight j).moveLeft i
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem cof_blsub_le {o} (f : ∀ a < o, Ordinal) : cof (blsub.{u, u} o f) ≤ o.card

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card

Tactic:
exact cof_blsub_le_lift f

Result:
no goals

Proof state:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ o.card

Tactic:
rw [← o.card.lift_id]

Result:
o : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
⊢ (o.blsub f).cof ≤ Cardinal.lift.{u, u} o.card
-- Mathlib/Topology/Separation/Hausdorff.lean
lemma Pi.isCompact_iff {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
    [∀ i, T2Space (π i)] {s : Set (Π i, π i)} :
    IsCompact s ↔ IsClosed s ∧ ∀ i, IsCompact (eval i '' s)

Proof state:
case mpr
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
H : IsClosed s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Tactic:
exact IsCompact.of_isClosed_subset (isCompact_univ_pi H.2) H.1 (subset_pi_eval_image univ s)

Result:
no goals

Proof state:
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
⊢ IsCompact s ↔ IsClosed s ∧ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
constructor <;> intro H

Result:
case mp
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
H : IsCompact s
⊢ IsClosed s ∧ ∀ (i : ι), IsCompact (eval i '' s)

case mpr
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
H : IsClosed s ∧ ∀ (i : ι), IsCompact (eval i '' s)
⊢ IsCompact s

Proof state:
case mp
ι : Type u_4
π : ι → Type u_5
inst✝¹ : (i : ι) → TopologicalSpace (π i)
inst✝ : ∀ (i : ι), T2Space (π i)
s : Set ((i : ι) → π i)
H : IsCompact s
⊢ IsClosed s ∧ ∀ (i : ι), IsCompact (eval i '' s)

Tactic:
exact ⟨H.isClosed, fun i ↦ H.image <| continuous_apply i⟩

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
private lemma pairMap_of_snd_nmem_fst {t : Finset σ × σ} (h : t.snd ∉ t.fst) :
    pairMap σ t = (t.fst.cons t.snd h, t.snd)

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h : t.2 ∉ t.1
⊢ MvPolynomial.NewtonIdentities.pairMap σ t = (cons t.2 t.1 h, t.2)

Tactic:
simp [pairMap, h]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_neg (x : ℤ√d) : (-x).norm = x.norm :=
  -- Porting note: replaced `simp` with `rw`
  -- See https://github.com/leanprover-community/mathlib4/issues/5026
  (Int.cast_inj (α := ℤ√d)).1 <| by rw [norm_eq_mul_conj, star_neg, neg_mul_neg, norm_eq_mul_conj]

Proof state:
d : ℤ
x : ℤ√d
⊢ ↑(-x).norm = ↑x.norm

Tactic:
rw [norm_eq_mul_conj, star_neg, neg_mul_neg, norm_eq_mul_conj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem modify_modify_eq (f g : α → α) (n) (l : List α) :
    (modify f n l).modify g n = modify (g ∘ f) n l

Proof state:
case h
α : Type u_1
f g : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (modify g n (modify f n l)).length) (h₂ : i < (modify (g ∘ f) n l).length),
    (modify g n (modify f n l))[i] = (modify (g ∘ f) n l)[i]

Tactic:
intro m h₁ h₂

Result:
case h
α : Type u_1
f g : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify g n (modify f n l)).length
h₂ : m < (modify (g ∘ f) n l).length
⊢ (modify g n (modify f n l))[m] = (modify (g ∘ f) n l)[m]

Proof state:
α : Type u_1
f g : α → α
n : Nat
l : List α
⊢ modify g n (modify f n l) = modify (g ∘ f) n l

Tactic:
apply ext_getElem

Result:
case hl
α : Type u_1
f g : α → α
n : Nat
l : List α
⊢ (modify g n (modify f n l)).length = (modify (g ∘ f) n l).length

case h
α : Type u_1
f g : α → α
n : Nat
l : List α
⊢ ∀ (i : Nat) (h₁ : i < (modify g n (modify f n l)).length) (h₂ : i < (modify (g ∘ f) n l).length),
    (modify g n (modify f n l))[i] = (modify (g ∘ f) n l)[i]

Proof state:
case hl
α : Type u_1
f g : α → α
n : Nat
l : List α
⊢ (modify g n (modify f n l)).length = (modify (g ∘ f) n l).length

Tactic:
simp

Result:
no goals

Proof state:
case h
α : Type u_1
f g : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify g n (modify f n l)).length
h₂ : m < (modify (g ∘ f) n l).length
⊢ (if n = m then g (if n = m then f l[m] else l[m]) else if n = m then f l[m] else l[m]) =
    if n = m then g (f l[m]) else l[m]

Tactic:
split <;> simp

Result:
no goals

Proof state:
case h
α : Type u_1
f g : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify g n (modify f n l)).length
h₂ : m < (modify (g ∘ f) n l).length
⊢ (modify g n (modify f n l))[m] = (modify (g ∘ f) n l)[m]

Tactic:
simp only [getElem_modify, Function.comp_apply]

Result:
case h
α : Type u_1
f g : α → α
n : Nat
l : List α
m : Nat
h₁ : m < (modify g n (modify f n l)).length
h₂ : m < (modify (g ∘ f) n l).length
⊢ (if n = m then g (if n = m then f l[m] else l[m]) else if n = m then f l[m] else l[m]) =
    if n = m then g (f l[m]) else l[m]
-- Mathlib/RingTheory/PowerSeries/Inverse.lean
theorem normUnit_X : normUnit (X : k⟦X⟧) = 1

Proof state:
k : Type u_2
inst✝ : Field k
⊢ normUnit X = 1

Tactic:
simp [normUnit, ← Units.val_eq_one, Unit_of_divided_by_X_pow_order_nonzero]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
lemma homMk'_comp (f : StructuredArrow S T) (g : f.right ⟶ Y') (g' : Y' ⟶ Y'') :
    homMk' f (g ≫ g') = homMk' f g ≫ homMk' (mk (f.hom ≫ T.map g)) g' ≫ eqToHom (by simp)

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y' Y'' : C
T : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ (f.homMk' (g ≫ g')).right = (f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯).right

Tactic:
simp [eqToHom_right]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S S' S'' : D
Y Y' Y'' : C
T T' : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ mk ((mk (f.hom ≫ T.map g)).hom ≫ T.map g') = mk (f.hom ≫ T.map (g ≫ g'))

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y' Y'' : C
T : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ f.homMk' (g ≫ g') = f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯

Tactic:
ext

Result:
case h
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
Y' Y'' : C
T : C ⥤ D
f : StructuredArrow S T
g : f.right ⟶ Y'
g' : Y' ⟶ Y''
⊢ (f.homMk' (g ≫ g')).right = (f.homMk' g ≫ (mk (f.hom ≫ T.map g)).homMk' g' ≫ eqToHom ⋯).right
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
/-- Left unitality of the enriched structure -/
@[reassoc (attr := simp)]
lemma id_comp (x y : C) [Closed x] :
    (λ_ ((ihom x).obj y)).inv ≫ id x ▷ _ ≫ comp x x y = 𝟙 _

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ (λ_ ((ihom x).obj y)).inv ≫ id x ▷ (ihom x).obj y ≫ comp x x y = 𝟙 ((ihom x).obj y)

Tactic:
apply uncurry_injective

Result:
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ uncurry ((λ_ ((ihom x).obj y)).inv ≫ id x ▷ (ihom x).obj y ≫ comp x x y) = uncurry (𝟙 ((ihom x).obj y))

Proof state:
case a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
x y : C
inst✝ : Closed x
⊢ uncurry ((λ_ ((ihom x).obj y)).inv ≫ id x ▷ (ihom x).obj y ≫ comp x x y) = uncurry (𝟙 ((ihom x).obj y))

Tactic:
rw [uncurry_natural_left, uncurry_natural_left, comp_eq, uncurry_curry, id_eq, compTranspose_eq,
    associator_inv_naturality_middle_assoc, ← comp_whiskerRight_assoc, ← uncurry_eq,
    uncurry_curry, triangle_assoc_comp_right_assoc, whiskerLeft_inv_hom_assoc,
    uncurry_id_eq_ev _ _]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_aleph_succ (o : Ordinal) : IsRegular (ℵ_ (succ o))

Proof state:
o : Ordinal.{u_1}
⊢ (ℵ_ (succ o)).IsRegular

Tactic:
rw [aleph_succ]

Result:
o : Ordinal.{u_1}
⊢ (succ (ℵ_ o)).IsRegular

Proof state:
o : Ordinal.{u_1}
⊢ (succ (ℵ_ o)).IsRegular

Tactic:
exact isRegular_succ (aleph0_le_aleph o)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem algEquivOfEq_apply_root {p q : K[X]} (hp : p ≠ 0) (h_eq : p = q) :
    algEquivOfEq hp h_eq (root p) = root q

Proof state:
K : Type u_1
inst✝ : Field K
p q : K[X]
hp : p ≠ 0
h_eq : p = q
⊢ (algEquivOfEq hp h_eq) (root p) = root q

Tactic:
rw [← coe_algHom, algEquivOfEq_toAlgHom, liftHom_root]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem inf_eq {u₁ u₂ : UniformSpace γ} :
    𝒰(α, γ, u₁ ⊓ u₂) = 𝒰(α, γ, u₁) ⊓ 𝒰(α, γ, u₂)

Proof state:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ uniformSpace α γ = uniformSpace α γ ⊓ uniformSpace α γ

Tactic:
rw [inf_eq_iInf, inf_eq_iInf, UniformFun.iInf_eq]

Result:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ

Proof state:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ

Tactic:
cases i <;> rfl

Result:
no goals

Proof state:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
⊢ ⨅ i, uniformSpace α γ = ⨅ b, bif b then uniformSpace α γ else uniformSpace α γ

Tactic:
refine iInf_congr fun i => ?_

Result:
α : Type u_1
γ : Type u_3
u₁ u₂ : UniformSpace γ
i : Bool
⊢ uniformSpace α γ = bif i then uniformSpace α γ else uniformSpace α γ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isNone_map' {x : Option α} : (x.map f).isNone = x.isNone

Proof state:
α : Type u_1
α✝ : Type u_2
f : α → α✝
x : Option α
⊢ (Option.map f x).isNone = x.isNone

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem summable_nnnorm_mul_pow (p : FormalMultilinearSeries 𝕜 E F) {r : ℝ≥0} (h : ↑r < p.radius) :
    Summable fun n : ℕ => ‖p n‖₊ * r ^ n

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a => ↑(‖p a‖₊ * r ^ a)

Tactic:
push_cast

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a => ‖p a‖ * ↑r ^ a

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun n => ‖p n‖₊ * r ^ n

Tactic:
rw [← NNReal.summable_coe]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a => ↑(‖p a‖₊ * r ^ a)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0
h : ↑r < p.radius
⊢ Summable fun a => ‖p a‖ * ↑r ^ a

Tactic:
exact p.summable_norm_mul_pow h

Result:
no goals
-- Mathlib/CategoryTheory/Types.lean
theorem eqToHom_map_comp_apply (p : X = Y) (q : Y = Z) (x : F.obj X) :
    F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom <| p.trans q) x

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
X Y Z : C
p : X = Y
q : Y = Z
x : F.obj X
⊢ F.map (eqToHom q) (F.map (eqToHom p) x) = F.map (eqToHom ⋯) x

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem image_mul_right : (· * b) '' t = (· * b⁻¹) ⁻¹' t

Proof state:
α : Type u_2
inst✝ : Group α
t : Set α
b : α
⊢ (fun x => x * b) '' t = (fun x => x * b⁻¹) ⁻¹' t

Tactic:
rw [image_eq_preimage_of_inverse] <;> intro c <;> simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem insertP_cons_pos (p : α → Bool) (a b l) (h : p b) :
    insertP p a (b :: l) = a :: b :: l

Proof state:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : p b = true
⊢ insertP p a (b :: l) = a :: b :: l

Tactic:
simp only [insertP, insertP.loop, cond, h]

Result:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : p b = true
⊢ [a].reverseAux (b :: l) = a :: b :: l

Proof state:
α : Type u_1
p : α → Bool
a b : α
l : List α
h : p b = true
⊢ [a].reverseAux (b :: l) = a :: b :: l

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Exposed.lean
theorem mono (hC : IsExposed 𝕜 A C) (hBA : B ⊆ A) (hCB : C ⊆ B) : IsExposed 𝕜 B C

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ B ∧ ∀ y ∈ B, l y ≤ l x}

Tactic:
obtain ⟨l, rfl⟩ := hC ⟨w, hw⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hBA : B ⊆ A
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ B ∧ ∀ y ∈ B, l_1 y ≤ l_1 x}

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
⊢ IsExposed 𝕜 B C

Tactic:
rintro ⟨w, hw⟩

Result:
case intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B C : Set E
hC : IsExposed 𝕜 A C
hBA : B ⊆ A
hCB : C ⊆ B
w : E
hw : w ∈ C
⊢ ∃ l, C = {x | x ∈ B ∧ ∀ y ∈ B, l y ≤ l x}

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : OrderedRing 𝕜
inst✝² : AddCommMonoid E
inst✝¹ : TopologicalSpace E
inst✝ : Module 𝕜 E
A B : Set E
hBA : B ⊆ A
w : E
l : E →L[𝕜] 𝕜
hC : IsExposed 𝕜 A {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
hCB : {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} ⊆ B
hw : w ∈ {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x}
⊢ ∃ l_1, {x | x ∈ A ∧ ∀ y ∈ A, l y ≤ l x} = {x | x ∈ B ∧ ∀ y ∈ B, l_1 y ≤ l_1 x}

Tactic:
exact ⟨l, Subset.antisymm (fun x hx => ⟨hCB hx, fun y hy => hx.2 y (hBA hy)⟩) fun x hx =>
  ⟨hBA hx.1, fun y hy => (hw.2 y hy).trans (hx.2 w (hCB hw))⟩⟩

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem lt_div_iff_of_neg' (hc : c < 0) : a < b / c ↔ b < c * a

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : c < 0
⊢ a < b / c ↔ b < c * a

Tactic:
rw [mul_comm, lt_div_iff_of_neg hc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CNF.lean
theorem constToCNF_eval :
    (constToCNF output b).eval assign
      =
    (assign output == b)

Proof state:
α✝ : Type u_1
output : α✝
b : Bool
assign : α✝ → Bool
⊢ CNF.eval assign (constToCNF output b) = (assign output == b)

Tactic:
simp [constToCNF, CNF.eval, CNF.Clause.eval]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_ext₂_right {J : Type} [Fintype J]
    {f : J → C} {X Y Z : C} {g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z}
    (w : ∀ j, g ≫ ((biproduct.π f j ▷ Y) ▷ Z) = h ≫ ((biproduct.π f j ▷ Y) ▷ Z)) :
    g = h

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g = h

Tactic:
apply (cancel_mono (α_ _ _ _).hom).mp

Result:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
⊢ g ≫ (α_ (⨁ f) Y Z).hom = h ≫ (α_ (⨁ f) Y Z).hom

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
j✝ : J
⊢ (g ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z) = (h ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z)

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X Y Z : C
g h : X ⟶ ((⨁ f) ⊗ Y) ⊗ Z
w : ∀ (j : J), g ≫ biproduct.π f j ▷ Y ▷ Z = h ≫ biproduct.π f j ▷ Y ▷ Z
j✝ : J
⊢ (g ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z) = (h ≫ (α_ (⨁ f) Y Z).hom) ≫ biproduct.π f j✝ ▷ (Y ⊗ Z)

Tactic:
simp [w]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem isIntegral_algHom_iff (f : A →ₐ[R] B) (hf : Function.Injective f) {x : A} :
    IsIntegral R (f x) ↔ IsIntegral R x

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
x : A
⊢ IsIntegral R (f x) ↔ IsIntegral R x

Tactic:
refine ⟨fun ⟨p, hp, hx⟩ ↦ ⟨p, hp, ?_⟩, IsIntegral.map f⟩

Result:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
x : A
x✝ : IsIntegral R (f x)
p : R[X]
hp : p.Monic
hx : eval₂ (algebraMap R B) (f x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
A : Type u_5
B : Type u_6
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
f : A →ₐ[R] B
hf : Function.Injective ⇑f
x : A
x✝ : IsIntegral R (f x)
p : R[X]
hp : p.Monic
hx : eval₂ (algebraMap R B) (f x) p = 0
⊢ eval₂ (algebraMap R A) x p = 0

Tactic:
rwa [← f.comp_algebraMap, ← AlgHom.coe_toRingHom, ← hom_eval₂, AlgHom.coe_toRingHom,
  map_eq_zero_iff f hf] at hx

Result:
no goals