mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto ((fun x ↦ x.2 * x.1⁻¹) ∘ fun x ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2)) (𝓤 (β × β)) (𝓝 1)

Tactic:
uniformity_prod_eq_prod,

Goal state after:
β : Type u_2
inst✝³ : UniformSpace β
inst✝² : Group β
inst✝¹ : IsLeftUniformGroup β
inst✝ : IsRightUniformGroup β
φ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₂ * y₂⁻¹ * y₁ * x₁⁻¹
ψ : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁⁻¹ * x₂ * (y₂⁻¹ * y₁)
g : (β × β) × β × β → β :=
  fun x ↦
    match x with
    | ((x₁, x₂), y₁, y₂) => x₁
this : Tendsto φ (𝓤 β ×ˢ 𝓤 β) (𝓝 1)
⊢ Tendsto ((fun x ↦ x.2 * x.1⁻¹) ∘ fun x ↦ (x.1.1 / x.1.2, x.2.1 / x.2.2))
    (map (fun p ↦ ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 β ×ˢ 𝓤 β)) (𝓝 1)
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₀
x : G₀
l : Filter α
f : α → G₀
hx : x ≠ 0
⊢ Tendsto (fun x ↦ (f x)⁻¹) l (𝓝 x⁻¹) ↔ Tendsto f l (𝓝 x)

Tactic:
by
  simp only [nhds_inv₀ hx, ← Filter.comap_inv, tendsto_comap_iff, Function.comp_def, inv_inv]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)

Tactic:
have comm : ((fun x : α × α => x.2 / x.1) ∘ fun t : β × β => (e t.1, e t.2)) =
      e ∘ fun t : β × β => t.2 / t.1 := by
    ext t
    simp

Goal state after:
α : Type u_1
β : Type u_2
hom : Type u_3
inst✝⁶ : TopologicalSpace α
inst✝⁵ : Group α
inst✝⁴ : IsTopologicalGroup α
inst✝³ : TopologicalSpace β
inst✝² : Group β
inst✝¹ : FunLike hom β α
inst✝ : MonoidHomClass hom β α
e : hom
de : IsDenseInducing ⇑e
x₀ : α
comm : ((fun x ↦ x.2 / x.1) ∘ fun t ↦ (e t.1, e t.2)) = ⇑e ∘ fun t ↦ t.2 / t.1
⊢ Tendsto (fun t ↦ t.2 / t.1) (comap (fun p ↦ (e p.1, e p.2)) (𝓝 (x₀, x₀))) (𝓝 1)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
⊢ ((univ.pi fun i ↦ Ioc (x i) (update y i₀ m i)) ∪ univ.pi fun i ↦ Ioc (update x i₀ m i) (y i)) =
    univ.pi fun i ↦ Ioc (x i) (y i)

Tactic:
by
  simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← ofPred_or, le_or_gt, ofPred_true, univ_inter]

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

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
us : UniformSpace G
inst✝² : IsLeftUniformGroup G
inst✝¹ : FirstCountableTopology G
N : Subgroup G
inst✝ : N.Normal
hG : CompleteSpace G
⊢ CompleteSpace (G ⧸ N)

Tactic:
by
  have : IsTopologicalGroup.leftUniformSpace G = us := by
    ext : 1
    rw [@IsLeftUniformGroup.uniformity_eq (G := G) us _ _]
    rfl
  rw [← this] at hG
  infer_instance

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : CommGroup α
inst✝² : LinearOrder α
inst✝¹ : IsOrderedMonoid α
inst✝ : OrderTopology α
a x : α
⊢ ⨅ (_ : (Equiv.divLeft a) x > 1), 𝓟 {a_1 | a / a_1 < (Equiv.divLeft a) x} = ⨅ (_ : x ∈ Iio a), 𝓟 (Ioi x)

Tactic:
simp [Ioi]

Goal state after:
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (s ∩ e.source) = e.target ∩ ↑e.symm ⁻¹' s
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

Tactic:
inter_comm,

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (s ∩ e.source) = e.target ∩ ↑e.symm ⁻¹' (s ∩ e.source)
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = ↑e.symm '' (e.target ∩ e'.source)

Tactic:
e.trans_source',

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source) = ↑e.symm '' (e.target ∩ e'.source)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
⊢ ∀ x ∈ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i,
    ∀ y ∈ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i, Icc x y ⊆ (⋂ i ∈ s.1, Ioi ↑i) ∩ ⋂ i ∈ s.2, Iio ↑i

Tactic:
refine ((ordConnected_biInter ?_).inter (ordConnected_biInter ?_)).out <;> intro _ _

Goal state after:
case refine_1
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Iio a))
hi✝ : i✝ ∈ s.1
⊢ (Ioi ↑i✝).OrdConnected

case refine_2
α : Type u
β : Type v
γ : Type w
ts : TopologicalSpace α
inst✝¹ : Preorder α
inst✝ : OrderTopology α
a : α
s : Set (Subtype (Membership.mem (Iio a))) × Set (Subtype (Membership.mem (Ioi a)))
x✝ : s.1.Finite ∧ s.2.Finite
i✝ : Subtype (Membership.mem (Ioi a))
hi✝ : i✝ ∈ s.2
⊢ (Iio ↑i✝).OrdConnected
Module: Mathlib.Logic.Equiv.PartialEquiv

Goal state before:
pp: α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩

Goal state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
f : A →ₗ[R] B
r : R
c : CharacterModule B
x : A
⊢ (AddMonoidHom.comp (r • c) f.toAddMonoidHom) x = ((RingHom.id R) r • AddMonoidHom.comp c f.toAddMonoidHom) x

Tactic:
exact congr(c $(f.map_smul r x)).symm

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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : CharacterModule B
x✝ : A
⊢ ((dual 0) f) x✝ = (0 f) x✝

Tactic:
exact map_zero f

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

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
⊢ (dual f) φ = (dual f) ψ → φ = ψ

Tactic:
eq

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
⊢ φ = ψ
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) φ) y = ((dual f) ψ) y

Tactic:
eq

Goal state after:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) ψ) y = ((dual f) ψ) y
Module: Mathlib.Algebra.Module.CharacterModule

Goal state before:
pp: R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
⊢ uncurry ∘ₗ curry = LinearMap.id

Tactic:
ext _ z

Goal state after:
R : Type uR
inst✝⁶ : CommRing R
A : Type uA
inst✝⁵ : AddCommGroup A
A' : Type u_1
inst✝⁴ : AddCommGroup A'
B : Type uB
inst✝³ : AddCommGroup B
inst✝² : Module R A
inst✝¹ : Module R A'
inst✝ : Module R B
x✝ : CharacterModule (A ⊗[R] B)
z : A ⊗[R] B
⊢ ((uncurry ∘ₗ curry) x✝) z = (LinearMap.id x✝) z
Module: Mathlib.Topology.Instances.AddCircle.Defs

Goal state before:
pp: 𝕜 : Type u_1
inst✝ : AddCommGroup 𝕜
p : 𝕜
n : ℕ
hn : IsSMulRegular 𝕜 n
⊢ {x | n • x = 0}.Finite

Tactic:
nontriviality 𝕜
  obtain rfl | h0 := eq_or_ne n 0
  exacts [hn.not_zero.elim, ENat.card_lt_top.mp <|
    (card_torsion_le_of_isSMulRegular p n h0 hn).trans_lt <| ENat.natCast_lt_top n]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
inst✝ : Archimedean 𝕜
a : AddCircle p
b : ↑(Ioc 0 (0 + p)) := (QuotientAddGroup.equivIocMod ⋯ 0) a
⊢ ∃ b ∈ Ioc 0 p, ↑b = a

Tactic:
exact ⟨b.1, by simpa only [zero_add] using b.2,
    (QuotientAddGroup.equivIocMod hp.out 0).symm_apply_apply a⟩

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Internal.Types.Basic

Goal state before:
pp: A : Type u
inst✝ : MonObj A
x : A
⊢ x * 1 = x

Tactic:
convert! congr_hom (CC := fun X ↦ X) (mul_one A) (x, PUnit.unit)

Goal state after:
Module: Mathlib.CategoryTheory.Abelian.Refinements

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Epi f ↔ ∀ ⦃A : C⦄ (y : A ⟶ Y), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
by
  constructor
  · intro _ A a
    exact ⟨pullback a f, pullback.fst a f, inferInstance, pullback.snd a f, pullback.condition⟩
  · intro hf
    obtain ⟨A, π, hπ, a', fac⟩ := hf (𝟙 Y)
    rw [comp_id] at fac
    exact epi_of_epi_fac fac.symm

Goal state after:
Module: Mathlib.Algebra.Homology.ShortComplex.SnakeLemma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Epi S.L₂.g
⊢ Epi S.L₃.g

Tactic:
have : Epi (S.v₂₃.τ₂ ≫ S.L₃.g) := by
    rw [S.v₂₃.comm₂₃]
    apply epi_comp

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Abelian C
S : SnakeInput C
inst✝ : Epi S.L₂.g
this : Epi (S.v₂₃.τ₂ ≫ S.L₃.g)
⊢ Epi S.L₃.g
Module: Mathlib.Algebra.Category.ModuleCat.Adjunctions

Goal state before:
pp: case single
R : Type u_1
inst✝⁴ : CommRing R
C : Type u
inst✝³ : Category.{v, u} C
D : Type u
inst✝² : Category.{v, u} D
inst✝¹ : Preadditive D
inst✝ : Linear R D
F : C ⥤ D
X Y Z : Free R C
g : Y ⟶ Z
f' : X ⟶ Y
r : R
⊢ (sum (single f' r ≫ g) fun f' r ↦ r • F.map f') =
    ((single f' r).sum fun f' r ↦ r • F.map f') ≫ sum g fun f' r ↦ r • F.map f'

Tactic:
induction g using Finsupp.induction_linear with
      | zero => simp
      | add f₁ f₂ w₁ w₂ =>
        rw [comp_add]
        rw [Finsupp.sum_add_index', Finsupp.sum_add_index']
        · simp only [w₁, w₂, comp_add]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
        · intros; rw [zero_smul]
        · intros; simp only [add_smul]
      | single g' s =>
        rw [single_comp_single _ _ f' g' r s]
        simp [mul_comm r s, mul_smul]

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

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
R' : Type u'
inst✝ : CommRing R'
f : R →+* R'
S : ShortComplex (ModuleCat R')
h : S.Exact
⊢ (S.map (restrictScalars f)).Exact

Tactic:
by
  rw [CategoryTheory.ShortComplex.ShortExact.moduleCat_exact_iff_function_exact] at h ⊢
  exact h

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
n : ℕ
F G : ComposableArrows C n
h : ∀ (i : Fin (n + 1)), F.obj i = G.obj i
w : ∀ (i : ℕ) (hi : i < n), F.map' i (i + 1) ⋯ hi = eqToHom ⋯ ≫ G.map' i (i + 1) ⋯ hi ≫ eqToHom ⋯
i : ℕ
hi : i < n
⊢ F.map' i (i + 1) ⋯ hi ≫ (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ G.map' i (i + 1) ⋯ hi

Tactic:
simp [w i hi]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
⊢ (adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ = 𝟙 (𝟭 C)

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
i : L ⋙ R ≅ 𝟭 C
X : C
⊢ ((adj.unit ≫ i.hom) ≫ (adj.toMonad.transport i).μ).app X = (𝟙 (𝟭 C)).app X
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
⊢ (adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit = 𝟙 (𝟭 D)

Tactic:
ext X

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
adj : L ⊣ R
j : R ⋙ L ≅ 𝟭 D
X : D
⊢ ((adj.toComonad.transport j).δ ≫ j.inv ≫ adj.counit).app X = (𝟙 (𝟭 D)).app X
Module: Mathlib.CategoryTheory.Monad.Adjunction

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
L : C ⥤ D
R : D ⥤ C
h : L ⊣ R
X✝ Y✝ : D
f : X✝ ⟶ Y✝
⊢ h.toMonad.map (R.map f) ≫ { A := R.obj Y✝, a := R.map (h.counit.app Y✝), unit := ⋯, assoc := ⋯ }.a =
    { A := R.obj X✝, a := R.map (h.counit.app X✝), unit := ⋯, assoc := ⋯ }.a ≫ R.map f

Tactic:
by
        dsimp
        rw [← R.map_comp, Adjunction.counit_naturality, R.map_comp]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s)) ≫ T.map (c.π.app j) ≫ (D.obj j).a =
    s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝ : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cone (D ⋙ T.forget)
t : IsLimit c
s : Cone D
j : J
⊢ T.map (t.lift (T.forget.mapCone s) ≫ c.π.app j) ≫ (D.obj j).a = s.pt.a ≫ t.lift (T.forget.mapCone s) ≫ c.π.app j
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
A : adj.toComonad.Coalgebra
B : C
inst✝ : HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
f : B ⟶ comparisonRightAdjointObj adj A
⊢ (comparison adj).obj B ⟶ A

Tactic:
by
        refine ⟨(adj.homEquiv _ _).symm (f ≫ (equalizer.ι _ _)), (adj.homEquiv _ _).injective ?_⟩
        simp only [Adjunction.toComonad_coe, Functor.comp_obj, comparison_obj_A, comparison_obj_a,
          Adjunction.homEquiv_counit, Functor.map_comp, Category.assoc,
          Functor.comp_map, Adjunction.homEquiv_unit, Adjunction.unit_naturality_assoc,
          Adjunction.unit_naturality, Adjunction.right_triangle_components_assoc]
        congr 1
        exact (equalizer.condition _ _).symm

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

Goal state before:
pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.hom β.hom w ≫ homMkSucc α.inv β.inv ⋯) = δ₀Functor.map (𝟙 F)

Tactic:
ext ⟨i, hi⟩
      simp

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

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (c.ι.app j) ≫ T.map (t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s)

Tactic:
← Functor.map_comp_assoc,

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
T : Monad C
J : Type u
inst✝² : Category.{v, u} J
D : J ⥤ T.Algebra
c : Cocone (D ⋙ T.forget)
t : IsColimit c
inst✝¹ : PreservesColimit (D ⋙ T.forget) T.toFunctor
inst✝ : PreservesColimit ((D ⋙ T.forget) ⋙ T.toFunctor) T.toFunctor
s : Cocone D
j : J
⊢ T.map (c.ι.app j ≫ t.desc (T.forget.mapCocone s)) ≫ s.pt.a =
    T.map (c.ι.app j) ≫ lambda c t ≫ t.desc (T.forget.mapCocone s)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

Goal state before:
pp: case h₁
C : Type u_1
inst✝ : Category.{v_1, u_1} C
n m : ℕ
F✝ G✝ : ComposableArrows C n
F G : ComposableArrows C (n + 1)
α : F.obj' 0 ⋯ ≅ G.obj' 0 ⋯
β : F.δ₀ ≅ G.δ₀
w : F.map' 0 1 homMk₁._proof_4 ⋯ ≫ app' β.hom 0 ⋯ = α.hom ≫ G.map' 0 1 homMk₁._proof_4 ⋯
⊢ δ₀Functor.map (homMkSucc α.inv β.inv ⋯ ≫ homMkSucc α.hom β.hom w) = δ₀Functor.map (𝟙 G)

Tactic:
ext ⟨i, hi⟩
      simp

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✝² : HasCoreflexiveEqualizers C
inst✝¹ : F.ReflectsIsomorphisms
inst✝ : PreservesLimitOfIsCoreflexivePair F
this : ∀ (X : adj.toComonad.Coalgebra), IsIso ((comparisonAdjunction adj).counit.app X)
Y : C
⊢ adj.unit.app (G.obj (F.obj Y)) ≫ G.map (adj.counit.app (F.1 ((𝟭 C).obj Y))) =
    𝟙 (G.obj ((𝟭 D).obj (F.1 ((𝟭 C).obj Y))))

Tactic:
rw [← G.map_id]
          simp

Goal state after:
Module: Mathlib.RingTheory.Flat.Stability

Goal state before:
pp: R : Type u
M : Type u_1
Mp : Type u_2
Rp : Type v
inst✝¹⁰ : CommSemiring R
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : CommSemiring Rp
inst✝⁶ : Algebra R Rp
inst✝⁵ : AddCommMonoid Mp
inst✝⁴ : Module R Mp
inst✝³ : Module Rp Mp
inst✝² : IsScalarTower R Rp Mp
inst✝¹ : Flat R M
S : Submonoid R
inst✝ : IsLocalization S Rp
f : M →ₗ[R] Mp
h : IsLocalizedModule S f
⊢ Flat Rp Mp

Tactic:
fapply Flat.isBaseChange (R := R) (M := M) (S := Rp) (N := Mp)
  exact (isLocalizedModule_iff_isBaseChange S Rp f).mp h

Goal state after:
Module: Mathlib.RingTheory.Localization.Ideal

Goal state before:
pp: case mpr
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
J : Ideal S
⊢ (∃ x ∈ ↑M, x ∈ ↑(Ideal.under R J)) → J = ⊤

Tactic:
rintro ⟨x, hxM, hxJ⟩
    exact J.eq_top_of_isUnit_mem hxJ (IsLocalization.map_units S ⟨x, hxM⟩)

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ ((p₁ * p₂).sum fun a b ↦ ((monomial a) (a₁ * a₂ * (algebraMap R A) b)).coeff k) =
    ((p₁.sum fun n r ↦ (monomial n) (a₁ * (algebraMap R A) r)) *
          p₂.sum fun n r ↦ (monomial n) (a₂ * (algebraMap R A) r)).coeff
      k

Tactic:
coeff_monomial,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ ((p₁ * p₂).sum fun a b ↦ if a = k then a₁ * a₂ * (algebraMap R A) b else 0) =
    ((p₁.sum fun n r ↦ (monomial n) (a₁ * (algebraMap R A) r)) *
          p₂.sum fun n r ↦ (monomial n) (a₂ * (algebraMap R A) r)).coeff
      k
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (∑ b ∈ p₁.support, ((monomial b) (a₁ * (algebraMap R A) (p₁.coeff b))).coeff x.1) *
        ∑ b ∈ p₂.support, ((monomial b) (a₂ * (algebraMap R A) (p₂.coeff b))).coeff x.2

Tactic:
coeff_monomial,

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a₁ a₂ : A
p₁ p₂ : R[X]
k : ℕ
⊢ (if ¬(p₁ * p₂).coeff k = 0 then a₁ * a₂ * (algebraMap R A) ((p₁ * p₂).coeff k) else 0) =
    ∑ x ∈ Finset.antidiagonal k,
      (∑ x_1 ∈ p₁.support, if x_1 = x.1 then a₁ * (algebraMap R A) (p₁.coeff x_1) else 0) *
        ∑ x_1 ∈ p₂.support, if x_1 = x.2 then a₂ * (algebraMap R A) (p₂.coeff x_1) else 0
Module: Mathlib.RingTheory.Localization.AtPrime.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
I : Ideal R
hI : I.IsPrime
inst✝ : IsLocalization.AtPrime S I
x : R
y : ↥I.primeCompl
h : IsLocalRing S
⊢ mk' S x y ∉ IsLocalRing.maximalIdeal S ↔ x ∉ I

Tactic:
by
    simpa only [IsLocalRing.mem_maximalIdeal, mem_nonunits_iff, Classical.not_not] using!
      isUnit_mk'_iff S I x y

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
m : M
a : A
n : N
⊢ S.mkQ (m ⊗ₜ[R] (a • n)) = (RingHom.id A) a • S.mkQ (m ⊗ₜ[R] n)

Tactic:
rw [Submodule.mkQ_apply, Submodule.mkQ_apply, ← Submodule.Quotient.mk_smul, eq_comm,
            Submodule.Quotient.eq, RingHom.id_apply]
          exact Submodule.subset_span ⟨a, m, n, rfl⟩

Goal state after:
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ S

Tactic:
rw [← Submodule.ker_mkQ S, ← h]

Goal state after:
case refine_2
R : Type u_1
A : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing A
inst✝⁸ : Algebra R A
M : Type u_4
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Module A M
inst✝⁴ : IsScalarTower R A M
N : Type u_5
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module A N
inst✝ : IsScalarTower R A N
S : Submodule A (M ⊗[R] N) := Submodule.span A {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x}
F : M ⊗[A] N →ₗ[A] M ⊗[R] N ⧸ S :=
  TensorProduct.lift
    { toFun := fun m ↦ { toFun := fun n ↦ S.mkQ (m ⊗ₜ[R] n), map_add' := ⋯, map_smul' := ⋯ }, map_add' := ⋯,
      map_smul' := ⋯ }
h : F ∘ₗ mapOfCompatibleSMul A R A M N = S.mkQ
⊢ (mapOfCompatibleSMul A R A M N).ker ≤ (F ∘ₗ mapOfCompatibleSMul A R A M N).ker