mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ Tendsto (Prod.map u u) (atTop ×ˢ atTop) (𝓤 α) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i

Tactic:
refine (atTop_basis.prod_self.tendsto_iff h).trans ?_

Goal state after:
α : Type u
β : Type v
uniformSpace : UniformSpace α
γ : Sort u_1
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
u : β → α
p : γ → Prop
s : γ → SetRel α α
h : (𝓤 α).HasBasis p s
⊢ (∀ (ib : γ), p ib → ∃ ia, True ∧ ∀ x ∈ Ici ia ×ˢ Ici ia, Prod.map u u x ∈ s ib) ↔
    ∀ (i : γ), p i → ∃ N, ∀ (m : β), N ≤ m → ∀ (n : β), N ≤ n → (u m, u n) ∈ s i
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
⊢ ∃ x ∈ S, l ≤ 𝓝 x

Tactic:
obtain ⟨t, htS, htl, htU⟩ : ∃ t, t ⊆ S ∧ t ∈ l ∧ t ×ˢ t ⊆ U := by
    rcases hl' U hU with ⟨t, htl, htU⟩
    refine ⟨t ∩ S, inter_subset_right, inter_mem htl hls, Subset.trans ?_ htU⟩
    gcongr <;> apply inter_subset_left

Goal state after:
α : Type u
uniformSpace : UniformSpace α
ι : Sort u_1
s : ι → Set α
hs : ∀ (i : ι), IsComplete (s i)
U : SetRel α α
hU : U ∈ 𝓤 α
hd : ∀ (i j : ι), ∀ x ∈ s i, ∀ y ∈ s j, (x, y) ∈ U → i = j
S : Set α := ⋃ i, s i
l : Filter α
hl : Cauchy l
hls : S ∈ l
hl_ne : l.NeBot
hl' : ∀ s ∈ 𝓤 α, ∃ t ∈ l, t ×ˢ t ⊆ s
t : Set α
htS : t ⊆ S
htl : t ∈ l
htU : t ×ˢ t ⊆ U
⊢ ∃ x ∈ S, l ≤ 𝓝 x
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
s : Set α
hs : TotallyBounded s
U : SetRel α α
hU : U ∈ 𝓤 α
⊢ ∃ t ⊆ s, t.Finite ∧ s ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U}

Tactic:
by
  rw [← Filter.totallyBounded_principal_iff] at hs
  simp_rw [← SetRel.preimage_eq_biUnion]
  exact hs.exists_subset_of_mem (Filter.mem_principal_self s) hU

Goal state after:
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
f : α ≃ β
h₁ : UniformContinuous ⇑f
h₂ : UniformContinuous ⇑f.symm
⊢ comap (Prod.map ⇑f ⇑f) (𝓤 β) ≤ 𝓤 α

Tactic:
rwa [← Equiv.prodCongr_apply, ← map_equiv_symm]

Goal state after:
Module: Mathlib.Topology.UniformSpace.Cauchy

Goal state before:
pp: α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ TotallyBounded (interUnionBalls xs u U)

Tactic:
rw [Filter.HasBasis.totallyBounded_iff H]

Goal state after:
α : Type u
uniformSpace : UniformSpace α
p : ℕ → Prop
U : ℕ → SetRel α α
H : (𝓤 α).HasBasis p U
xs : ℕ → α
u : ℕ → ℕ
⊢ ∀ (i : ℕ), p i → ∃ t, t.Finite ∧ interUnionBalls xs u U ⊆ ⋃ y ∈ t, {x | (x, y) ∈ U i}
Module: Mathlib.Topology.UniformSpace.UniformEmbedding

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
⊢ IsUniformInducing (hid.extend f)

Tactic:
let sf := SeparationQuotient.mk ∘ f

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : UniformSpace α
inst✝³ : UniformSpace β
γ : Type u_3
inst✝² : UniformSpace γ
inst✝¹ : CompleteSpace β
inst✝ : CompleteSpace γ
i : α → β
f : α → γ
hid : IsDenseInducing i
hi : IsUniformInducing i
h : IsUniformInducing f
sf : α → SeparationQuotient γ := SeparationQuotient.mk ∘ f
⊢ IsUniformInducing (hid.extend f)
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
s : Set α
inst✝ : LocallyCompactSpace α
G : ι → α → β
g : α → β
p : Filter ι
hs : IsOpen[inst✝²] s
tfae_1_to_2 : TendstoLocallyUniformlyOn G g p s → ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
h : ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K
x : α
hx : x ∈ s
⊢ ∃ v ∈ 𝓝[s] x, TendstoUniformlyOn G g p v

Tactic:
obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds x).mem_iff.mp (hs.mem_nhds hx)
    exact ⟨K, nhdsWithin_le_nhds hK1, h K hK3 hK2⟩

Goal state after:
Module: Mathlib.Topology.UniformSpace.LocallyUniformConvergence

Goal state before:
pp: case mpr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
⊢ (∀ x ∈ s,
      ∀ u ∈ 𝓤 β,
        ∃ pa,
          (∀ᶠ (x : ι) in p, pa x) ∧
            ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u) →
    TendstoLocallyUniformlyOn F f p s

Tactic:
rintro h u hu x hx

Goal state after:
case mpr
α : Type u_1
β : Type u_2
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
s : Set α
p : Filter ι
h :
  ∀ x ∈ s,
    ∀ u ∈ 𝓤 β,
      ∃ pa,
        (∀ᶠ (x : ι) in p, pa x) ∧
          ∃ pb, (∀ᶠ (y : α) in 𝓝[s] x, pb y) ∧ ∀ {x : ι}, pa x → ∀ {y : α}, pb y → (f y, F x y) ∈ u
u : Set (β × β)
hu : u ∈ 𝓤 β
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∀ᶠ (n : ι) in p, ∀ y ∈ t, (f y, F n y) ∈ u
Module: Mathlib.Order.Filter.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ n f g) h = map₂ n' (map₂ m' f h) g

Tactic:
map₂_swap n,

Goal state after:
α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
δ' : Type u_8
ε : Type u_9
f : Filter α
g : Filter β
h : Filter γ
m : δ → γ → ε
n : α → β → δ
m' : α → γ → δ'
n' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), m (n a b) c = n' (m' a c) b
⊢ map₂ m (map₂ (fun a b ↦ n b a) g f) h = map₂ n' (map₂ m' f h) g
Module: Mathlib.Order.Filter.Pointwise

Goal state before:
pp: α : Type u_2
inst✝ : Monoid α
f : Filter α
hf : 1 ≤ f
⊢ f * ⊤ = ⊤

Tactic:
by
  refine top_le_iff.1 fun s => ?_
  simp only [mem_mul, mem_top, exists_eq_left]
  rintro ⟨t, ht, hs⟩
  rwa [mul_univ_of_one_mem (mem_one.1 <| hf ht), univ_subset_iff] at hs

Goal state after:
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_1
inst✝² : AddCommGroup α
inst✝¹ : LinearOrder α
inst✝ : IsOrderedAddMonoid α
a b c : α
⊢ (fun x ↦ x + a) ⁻¹' [[b, c]] = [[b - a, c - a]]

Tactic:
simpa only [add_comm] using preimage_const_add_uIcc a b c

Goal state after:
Module: Mathlib.Topology.Algebra.MulAction

Goal state before:
pp: M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
⊢ ContinuousSMul M X

Tactic:
refine continuousSMul_iInf fun b => ?_

Goal state after:
M : Type u_2
X : Type u_3
inst✝³ : TopologicalSpace M
inst✝² : SMul M X
t₁ t₂ : TopologicalSpace X
inst✝¹ : ContinuousSMul M X
inst✝ : ContinuousSMul M X
b : Bool
⊢ ContinuousSMul M X
Module: Mathlib.Algebra.Order.Group.Pointwise.Interval

Goal state before:
pp: α : Type u_2
inst✝³ : Monoid α
inst✝² : Preorder α
inst✝¹ : CanonicallyOrderedMul α
inst✝ : MulRightMono α
a b c : α
c_in : c ∈ Ici (a * b)
d : α
hd : c = a * b * d
⊢ ∃ y ∈ Ici b, a * y = c

Tactic:
exact ⟨b * d, by simp [← mul_assoc, hd]⟩

Goal state after:
Module: Mathlib.Topology.Algebra.Monoid

Goal state before:
pp: case refine_3
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ ⦃s t : Set M⦄, (∃ V ∈ 𝓝 0, s * V ⊆ U) → (∃ V ∈ 𝓝 0, t * V ⊆ U) → ∃ V ∈ 𝓝 0, (s ∪ t) * V ⊆ U

pp: case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U

Tactic:
· rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Goal state after:
case refine_4
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : MulZeroClass M
inst✝ : ContinuousMul M
K U : Set M
hK : IsCompact K
hU : U ∈ 𝓝 0
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 0, t * V ⊆ U
Module: Mathlib.Topology.Algebra.Group.Pointwise

Goal state before:
pp: G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T2Space G

Tactic:
by
  suffices T1Space G from inferInstance
  refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_
  rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩
  exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_const y⁻¹) (by rwa [mul_inv_cancel])

Goal state after:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: case refine_3
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ ⦃s t : Set G⦄, (∃ V ∈ 𝓝 1, s * V ⊆ U) → (∃ V ∈ 𝓝 1, t * V ⊆ U) → ∃ V ∈ 𝓝 1, (s ∪ t) * V ⊆ U

pp: case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U

Tactic:
· rintro s t ⟨V, V_in, hV'⟩ ⟨W, W_in, hW'⟩
    use V ∩ W, inter_mem V_in W_in
    rw [union_mul]
    exact
      union_subset ((mul_subset_mul_left V.inter_subset_left).trans hV')
        ((mul_subset_mul_left V.inter_subset_right).trans hW')

Goal state after:
case refine_4
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : MulOneClass G
inst✝ : ContinuousMul G
K U : Set G
hK : IsCompact K
hU : IsOpen[inst✝²] U
hKU : K ⊆ U
⊢ ∀ x ∈ K, ∃ t ∈ 𝓝[K] x, ∃ V ∈ 𝓝 1, t * V ⊆ U
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))

Tactic:
refine Tendsto.congr' ?_ (hfg.div hg hy)

Goal state after:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : ContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n ↦ f n * g n) l (𝓝 (x * y))
⊢ (fun n ↦ f n * g n) / g =ᶠ[l] f
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case refine_2
G✝ : Type u_1
inst✝⁵ : Group G✝
inst✝⁴ : TopologicalSpace G✝
inst✝³ : IsTopologicalGroup G✝
G : Type u_2
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
this✝ : UniformSpace G := IsTopologicalGroup.leftUniformSpace G
this : UniformSpace Gᵐᵒᵖ := IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ
⊢ UniformContinuous opEquiv.invFun

Tactic:
· simp [uniformContinuous_iff_le_comap, ← comap_op_rightUniformSpace, ← UniformSpace.comap_comap]

Goal state after:
Module: Mathlib.Topology.Algebra.Order.Field

Goal state before:
pp: 𝕜 : Type u_1
inst✝⁴ : Semifield 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x ↦ x ^ n) atTop (𝓝 0)

Tactic:
simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'

Goal state after:
Module: Mathlib.CategoryTheory.ObjectProperty.EpiMono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
P : ObjectProperty C
inst✝¹ : P.IsClosedUnderSubobjects
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hS : S.ShortExact
h₂ : P S.X₂
⊢ P S.X₁

Tactic:
have := hS.mono_f
  exact P.prop_of_mono S.f h₂

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Iio (f a)
h : ∀ (x : α), b < f x
⊢ ⨅ b ∈ Iio a, 𝓟 (Ioi b) ≤ 𝓟 (f ⁻¹' Ioi b)

Tactic:
· exact le_principal_iff.2 (univ_mem' h)

Goal state after:
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: case neg
α : Type u
β : Type v
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hf : ∀ {x y : α}, f x < f y ↔ x < y
H₁ : ∀ {a : α} {b : β} {x : α}, b < f a → ¬b < f x → ∃ y < a, b ≤ f y
H₂ : ∀ {a : α} {b : β} {x : α}, f a < b → ¬f x < b → ∃ y, a < y ∧ f y ≤ b
x✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α
a : α
b : β
hb : b ∈ Ioi (f a)
h : ∀ (x : α), f x < b
⊢ ⨅ b ∈ Ioi a, 𝓟 (Iio b) ≤ 𝓟 (f ⁻¹' Iio b)

Tactic:
· exact le_principal_iff.2 (univ_mem' h)

Goal state after:
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
hn : 1 = if addOrderOf a = 0 then 2 else addOrderOf a
⊢ a = 0

Tactic:
split_ifs at hn

Goal state after:
case pos
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : addOrderOf a = 0
hn : 1 = 2
⊢ a = 0

case neg
A : Type uA
inst✝ : AddCommGroup A
a : A
n : ℤ
h✝ : ¬addOrderOf a = 0
hn : 1 = addOrderOf a
⊢ a = 0
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ a ∈ Ico 0 (0 + p)

Tactic:
zero_add

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
ha : a ∈ Ico 0 p
h0 : 0 ∈ Ico 0 (0 + p)
⊢ a ∈ Ico 0 p
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: ι : Type u_1
X : ι → Type u_2
inst✝⁴ : Finite ι
inst✝³ : (i : ι) → LinearOrder (X i)
inst✝² : (i : ι) → TopologicalSpace (X i)
inst✝¹ : ∀ (i : ι), OrderTopology (X i)
a b x : (i : ι) → X i
inst✝ : Nonempty ι
ha : ∀ (i : ι), a i < x i
hb : ∀ (i : ι), x i < b i
i : ι
x✝ : i ∈ univ
⊢ Ioo (a i) (b i) ∈ 𝓝 (x i)

Tactic:
exact Ioo_mem_nhds (ha i) (hb i)

Goal state after:
Module: Mathlib.Algebra.Category.Grp.LeftExactFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map
          (Functor.LaxMonoidal.μ F X X ≫ F.map (SemiCartesianMonoidalCategory.fst X X) +
            Functor.LaxMonoidal.μ F X X ≫ F.map (SemiCartesianMonoidalCategory.snd X X))

Tactic:
Functor.Monoidal.μ_fst,

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : HasFiniteBiproducts C
F : C ⥤ AddCommGrpCat
inst✝ : PreservesFiniteLimits F
X : C
this✝¹ : (F ⋙ forget AddCommGrpCat).Braided := Functor.Braided.ofChosenFiniteProducts (F ⋙ forget AddCommGrpCat)
this✝ : F.Monoidal := Functor.Monoidal.ofChosenFiniteProducts F
this : F.Additive
⊢ μ ≫ Multiplicative.toAdd.toIso.hom =
    (Multiplicative.toAdd.toIso.hom ⊗ₘ Multiplicative.toAdd.toIso.hom) ≫
      Functor.LaxMonoidal.μ (forget AddCommGrpCat) (F.obj X) (F.obj X) ≫
        (forget AddCommGrpCat).map
          (SemiCartesianMonoidalCategory.fst (F.obj X) (F.obj X) +
            Functor.LaxMonoidal.μ F X X ≫ F.map (SemiCartesianMonoidalCategory.snd X X))
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p a : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
x : 𝕜
h : a ≡ x [PMOD p]
⊢ Quot.mk (EndpointIdent p a) ⟨a, ⋯⟩ = Quot.mk (EndpointIdent p a) ⟨a + p, ⋯⟩

Tactic:
exact Quot.sound EndpointIdent.mk

Goal state after:
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 (0 + p)

Tactic:
zero_add

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ico 0 p
⊢ x ∈ Ico 0 p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc 0 p
⊢ x ∈ Ioc 0 (0 + p)

Tactic:
zero_add

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝³ : AddCommGroup 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
f : 𝕜 → B
x : 𝕜
hx : x ∈ Ioc 0 p
⊢ x ∈ Ioc 0 p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f (0 + p)

Tactic:
zero_add

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ f 0 = f p
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 (0 + p))

Tactic:
zero_add

Goal state after:
𝕜 : Type u_1
B : Type u_2
inst✝⁶ : AddCommGroup 𝕜
inst✝⁵ : LinearOrder 𝕜
inst✝⁴ : IsOrderedAddMonoid 𝕜
p : 𝕜
hp : Fact (0 < p)
inst✝³ : Archimedean 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : TopologicalSpace B
f : 𝕜 → B
hf : f 0 = f p
hc : ContinuousOn f (Icc 0 p)
⊢ ContinuousOn f (Icc 0 p)
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : Ring R
X : Type u
M : ModuleCat R
f : X ⟶ ↑M
x : X
⊢ (ConcreteCategory.hom (freeDesc f)) (freeMk x) = (ConcreteCategory.hom f) x

Tactic:
dsimp [freeDesc]
  erw [Finsupp.lift_apply, Finsupp.sum_single_index]
  all_goals simp

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: R : Type u
inst✝ : CommRing R
x : PUnit.{u + 1}
⊢ (ConcreteCategory.hom (εIso R).inv) (freeMk x) = 1

Tactic:
dsimp [εIso, freeMk]
  erw [Finsupp.lapply_apply]
  rw [Finsupp.single_eq_same]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ⟶ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ app ⟨i + 1, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i (i + 1) ⋯ hi
k : ℕ
⊢ ∀ (i j : ℕ) (hj : i + k = j) (hj' : j ≤ n), F.map' i j ⋯ hj' ≫ app ⟨j, ⋯⟩ = app ⟨i, ⋯⟩ ≫ G.map' i j ⋯ hj'

Tactic:
induction k with intro i j hj hj'
    | zero =>
      simp only [add_zero] at hj
      obtain rfl := hj
      rw [F.map'_self i, G.map'_self i, id_comp, comp_id]
    | succ k hk =>
      rw [← add_assoc] at hj
      subst hj
      rw [F.map'_comp i (i + k) (i + k + 1), G.map'_comp i (i + k) (i + k + 1), assoc,
        w (i + k) (by valid), reassoc_of% (hk i (i + k) rfl (by valid))]

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi = (app ⟨i, ⋯⟩).hom ≫ (app ⟨i, ⋯⟩).inv ≫ F.map' i (i + 1) ⋯ hi

Tactic:
Iso.hom_inv_id_assoc

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ F G : ComposableArrows C n
app : (i : Fin (n + 1)) → F.obj i ≅ G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi ≫ (app ⟨i + 1, ⋯⟩).hom = (app ⟨i, ⋯⟩).hom ≫ G.map' i (i + 1) ⋯ hi
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi = F.map' i (i + 1) ⋯ hi
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
J : MultispanShape
I : MultispanIndex J C
K : Multicofork I
desc : (E : Multicofork I) → K.pt ⟶ E.pt
fac : ∀ (E : Multicofork I) (i : J.R), K.π i ≫ desc E = E.π i
uniq : ∀ (E : Multicofork I) (m : K.pt ⟶ E.pt), (∀ (i : J.R), K.π i ≫ m = E.π i) → m = desc E
S : Cocone I.multispan
a : J.L
⊢ K.ι.app (WalkingMultispan.left a) ≫ desc S = S.ι.app (WalkingMultispan.left a)

Tactic:
rw [← K.w (WalkingMultispan.Hom.fst a), ← S.w (WalkingMultispan.Hom.fst a),
          Category.assoc]
        congr 1
        apply fac

Goal state after:
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case zero.succ.succ
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F : ComposableArrows C n
X : C
f : X ⟶ F.left
k : ℕ
hk : k < n + 1 + 1
hi : 0 < n + 1 + 1
j : ℕ
hj : j + 1 + 1 < n + 1 + 1
hjk : ⟨j + 1 + 1, hj⟩ ≤ ⟨k, hk⟩
hij : ⟨0, hi⟩ ≤ ⟨j + 1 + 1, hj⟩
⊢ map F f ⟨0, hi⟩ ⟨k, hk⟩ ⋯ = map F f ⟨0, hi⟩ ⟨j + 1 + 1, hj⟩ hij ≫ map F f ⟨j + 1 + 1, hj⟩ ⟨k, hk⟩ hjk

Tactic:
· obtain _ | _ | k := k
      · simp [Fin.ext_iff] at hjk
      · simp [Fin.le_def] at hjk
      · dsimp
        rw [assoc, ← F.map_comp, homOfLE_comp]

Goal state after:
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso ((comparisonAdjunction adj).unit.app Y)

Tactic:
rw [comparisonAdjunction_unit_app]

Goal state after:
C : Type u₁
D : Type u₂
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : Category.{v₁, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝² : HasEqualizerOfIsCosplitPair F
inst✝¹ : PreservesLimitOfIsCosplitPair F
inst✝ : ReflectsLimitOfIsCosplitPair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ IsIso (limit.lift (parallelPair (G.map (F.map (adj.unit.app Y))) (adj.unit.app (G.obj (F.obj Y)))) (unitFork adj Y))