mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Group.Basic

Goal state before:
pp: H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ map (fun x ↦ x * c) (𝓝[<] a) = 𝓝[<] (a * c)

Tactic:
convert! (Homeomorph.mulRight c).isEmbedding.map_nhdsWithin_eq .. using 2

Goal state after:
case e'_3.e'_4
H : Type x
inst✝⁴ : TopologicalSpace H
inst✝³ : CommGroup H
inst✝² : PartialOrder H
inst✝¹ : IsOrderedMonoid H
inst✝ : ContinuousMul H
c a : H
⊢ Iio (a * c) = ⇑(Homeomorph.mulRight c) '' Iio a
Module: Mathlib.Topology.Algebra.IsUniformGroup.Defs

Goal state before:
pp: case refine_1
β : 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₁
φ_ψ_conj : φ = g * ψ * g⁻¹
⊢ Tendsto (fun x ↦ x.1.1⁻¹ * x.1.2) (comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1) ×ˢ comap (fun x ↦ x.1⁻¹ * x.2) (𝓝 1)) (𝓝 1)

Tactic:
exact tendsto_comap.comp tendsto_fst

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

Goal state before:
pp: G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * x.2.2⁻¹ * (x.2.1 * x.1.1⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)

Tactic:
rw [mul_assoc, mul_comm x.2.2⁻¹, mul_comm x.2.1]

Goal state after:
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
x : (G × G) × G × G
⊢ x.1.2 * (x.1.1⁻¹ * x.2.1 * x.2.2⁻¹) = x.1.2 * x.1.1⁻¹ * (x.2.1 * x.2.2⁻¹)
Module: Mathlib.Topology.Algebra.GroupWithZero

Goal state before:
pp: α : Type u_1
β : Type u_2
G₀ : Type u_3
inst✝⁵ : GroupWithZero G₀
inst✝⁴ : TopologicalSpace G₀
inst✝³ : ContinuousInv₀ G₀
inst✝² : ContinuousMul G₀
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
a : α
f g : α → G₀
h : α → G₀ → β
hf : ContinuousAt f a
hg : ContinuousAt g a
hh : g a ≠ 0 → ContinuousAt ↿h (a, f a / g a)
h2h : g a = 0 → Tendsto (↿h) (𝓝 a ×ˢ ⊤) (𝓝 (h a 0))
⊢ ContinuousAt (fun x ↦ h x (f x / g x)) a

Tactic:
change ContinuousAt (↿h ∘ fun x => (x, f x / g x)) a
  by_cases hga : g a = 0
  · rw [ContinuousAt]
    simp_rw [comp_apply, hga, div_zero]
    exact (h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)
  · fun_prop

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

Goal state before:
pp: G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : IsTopologicalGroup G
⊢ UniformSpace.comap op (IsTopologicalGroup.rightUniformSpace Gᵐᵒᵖ) = IsTopologicalGroup.leftUniformSpace G

Tactic:
ext : 1
  change comap (fun (x : G × G) ↦ (MulOpposite.op x.1, MulOpposite.op x.2))
      (comap (fun p : Gᵐᵒᵖ × Gᵐᵒᵖ => p.2 * p.1⁻¹) (𝓝 1))
    = comap (fun p : G × G => p.1⁻¹ * p.2) (𝓝 1)
  have : 𝓝 (1 : G) = comap (MulOpposite.opHomeomorph) (𝓝 (1 : Gᵐᵒᵖ)) := by
    simp [Homeomorph.comap_nhds_eq]
  simp_rw [comap_comap, this, comap_comap]
  rfl

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 𝕜
a : 𝕜
ha : 0 < a
⊢ Ioo 0 a = ((fun i ↦ Inv.inv '' Ioi i) ∘ Inv.inv) a

Tactic:
by simp [inv_Ioi₀ (inv_pos.2 ha)]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ ↑e x = ↑e' x

Tactic:
apply h.2

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
e e' : PartialEquiv α β
h : e ≈ e'
s : e.source = univ
t : e.target = univ
x : α
⊢ x ∈ e.source
Module: Mathlib.Algebra.Category.Grp.Images

Goal state before:
pp: G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom F'.m)
      ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯)) =
    (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯)) +
      (ConcreteCategory.hom F'.m)
        ((ConcreteCategory.hom F'.e) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯))

Tactic:
change (F'.e ≫ F'.m) _ = (F'.e ≫ F'.m) _ + (F'.e ≫ F'.m) _

Goal state after:
G H : AddCommGrpCat
f : G ⟶ H
F' : MonoFactorisation f
x y : ↥(Hom.hom f).range
this : Mono F'.m
⊢ (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑(x + y)) ⋯) =
    (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x_1 ↦ (Hom.hom f) x_1 = ↑x) ⋯) +
      (ConcreteCategory.hom (F'.e ≫ F'.m)) ↑(Classical.indefiniteDescription (fun x ↦ (Hom.hom f) x = ↑y) ⋯)
Module: Mathlib.Topology.Order.Basic

Goal state before:
pp: α : 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
⊢ induced f inst✝¹ = Preorder.topology α

Tactic:
by
  let _ := Preorder.topology α; have : OrderTopology α := ⟨rfl⟩
  refine le_antisymm (induced_topology_le_preorder hf) ?_
  refine le_of_nhds_le_nhds fun a => ?_
  simp only [nhds_eq_order, nhds_induced, comap_inf, comap_iInf, comap_principal]
  refine inf_le_inf (le_iInf₂ fun b hb => ?_) (le_iInf₂ fun b hb => ?_)
  · by_cases! h : ∃ x, ¬(b < f x)
    · rcases h with ⟨x, hx⟩
      rcases H₁ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => hyb.trans_lt (hf.2 hz))
    · exact le_principal_iff.2 (univ_mem' h)
  · by_cases! h : ∃ x, ¬(f x < b)
    · rcases h with ⟨x, hx⟩
      rcases H₂ hb hx with ⟨y, hya, hyb⟩
      exact iInf₂_le_of_le y hya (principal_mono.2 fun z hz => (hf.2 hz).trans_le hyb)
    · exact le_principal_iff.2 (univ_mem' h)

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)
a : 𝕜
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑x = (equivIoc p a).symm ⟨x, hx⟩

Tactic:
equivIoc,

Goal state after:
𝕜 : Type u_1
inst✝³ : AddCommGroup 𝕜
p : 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsOrderedAddMonoid 𝕜
hp : Fact (0 < p)
a : 𝕜
inst✝ : Archimedean 𝕜
x : 𝕜
hx : x ∈ Ioc a (a + p)
⊢ ↑x = (QuotientAddGroup.equivIocMod ⋯ a).symm ⟨x, hx⟩
Module: Mathlib.CategoryTheory.Monoidal.CommMon_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : MonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : MonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : MonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
G : D ⥤ E
inst✝² : F.LaxBraided
inst✝¹ : F'.LaxBraided
inst✝ : G.LaxBraided
A : CommMon C
⊢ (β_ (F.mapMon.obj A.toMon).X (F.mapMon.obj A.toMon).X).hom ≫ μ = μ

Tactic:
by
            dsimp
            rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.CommGrp_

Goal state before:
pp: C : Type u₁
inst✝¹¹ : Category.{v₁, u₁} C
inst✝¹⁰ : CartesianMonoidalCategory C
inst✝⁹ : BraidedCategory C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : CartesianMonoidalCategory D
inst✝⁶ : BraidedCategory D
E : Type u₃
inst✝⁵ : Category.{v₃, u₃} E
inst✝⁴ : CartesianMonoidalCategory E
inst✝³ : BraidedCategory E
F F' : C ⥤ D
inst✝² : F.Braided
inst✝¹ : F'.Braided
G : D ⥤ E
inst✝ : G.Braided
A : CommGrp C
⊢ (β_ (F.mapGrp.obj A.toGrp).X (F.mapGrp.obj A.toGrp).X).hom ≫ μ = μ

Tactic:
by
            dsimp
            rw [← Functor.LaxBraided.braided_assoc, ← Functor.map_comp, IsCommMonObj.mul_comm]

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
⊢ ∀ ⦃A : C⦄ (x₂ : A ⟶ S.L₁'.X₂), x₂ ≫ S.L₁'.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.L₁'.f

Tactic:
intro A₀ x₃ hx₃

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
A₀ : C
x₃ : A₀ ⟶ S.L₁'.X₂
hx₃ : x₃ ≫ S.L₁'.g = 0
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₃ = x₁ ≫ S.L₁'.f
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'
this :
  Limits.PreservesFiniteLimits (ModuleCat.restrictScalars f) ∧
    Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)
⊢ Limits.PreservesFiniteColimits (ModuleCat.restrictScalars f)

Tactic:
exact this.2

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ f ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b

Tactic:
reassoc_of% h

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
hK : IsLimit K
T : C
f g : T ⟶ K.pt
h : ∀ (a : J.L), f ≫ K.ι a = g ≫ K.ι a
b : J.R
⊢ g ≫ K.ι (J.fst b) ≫ I.fst b = g ≫ K.ι (J.fst b) ≫ I.fst b
Module: Mathlib.CategoryTheory.Monad.Comonadicity

Goal state before:
pp: case refine_2
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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
A B : C
B' : adj.toComonad.Coalgebra
g : A ⟶ B
h : (comparison adj).obj B ⟶ B'
⊢ (comparisonRightAdjointHomEquiv adj B' A) ((comparison adj).map g ≫ h) ≫
      equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A)) =
    (g ≫ (comparisonRightAdjointHomEquiv adj B' B) h) ≫ equalizer.ι (G.map B'.a) (adj.unit.app (G.1 B'.A))

Tactic:
simp [Adjunction.homEquiv_unit]

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✝ : ∀ (A : adj.toComonad.Coalgebra), HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))
B : C
⊢ equalizer.lift ((adj.homEquiv B (F.obj B)) (𝟙 (F.obj B))) ⋯ ≫
      equalizer.ι (G.map ((comparison adj).obj B).a) (adj.unit.app (G.1 ((comparison adj).obj B).A)) =
    equalizer.lift (adj.unit.app B) ⋯ ≫ equalizer.ι (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))

Tactic:
simp [Adjunction.homEquiv_unit]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Reflexive

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
F G : WalkingReflexivePair ⥤ C
e₀ : F.obj zero ⟶ G.obj zero
e₁ : F.obj one ⟶ G.obj one
h₁ : F.map left ≫ e₀ = e₁ ≫ G.map left
h₂ : F.map right ≫ e₀ = e₁ ≫ G.map right
h₃ : F.map reflexion ≫ e₁ = e₀ ≫ G.map reflexion
D : Type u₂
inst✝ : Category.{v₂, u₂} D
H : C ⥤ D
⊢ (F ⋙ H).map reflexion ≫ H.map e₁ = H.map e₀ ≫ (G ⋙ H).map reflexion

Tactic:
simp only [Functor.comp_obj, Functor.comp_map, ← Functor.map_comp, h₃]

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

Goal state before:
pp: M : Type u_1
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S T : Ideal R
h : a • S ≤ a • T
⊢ S ≤ T

Tactic:
simpa using smul_mono_right a⁻¹ h

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

Tactic:
rw [IsPrimary, Submodule.IsPrimary, forall_comm]

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
⊢ (I ≠ ⊤ ∧ ∀ (b a : R), a • b ∈ I → b ∈ I ∨ ∃ n, a ^ n • ⊤ ≤ I) ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid N
inst✝² : Module R M
inst✝¹ : Module R N
p : Submonoid R
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M' : Submodule R M
⊢ map f M' ≤ localized₀ p f M'

Tactic:
by
  rintro - ⟨x, hx, rfl⟩
  rw [mem_localized₀]
  exact ⟨x, hx, 1, IsLocalizedModule.mk'_one p f x⟩

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N N' : Submodule R M
r : R
⊢ r ∈ N.colon ↑N' ↔ r • N' ≤ N

Tactic:
by
  aesop (add simp SetLike.coe_subset_coe)

Goal state after:
Module: Mathlib.RingTheory.Nilpotent.Lemmas

Goal state before:
pp: case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
⊢ LinearMap.restrict f hp ^ n = 0

Tactic:
ext ⟨x, hx⟩

Goal state after:
case h
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : End R M
p q : Submodule R M
hp : MapsTo ⇑f ↑p ↑p
hq : MapsTo ⇑f ↑q ↑q
h : p ≤ q
n : ℕ
hn : LinearMap.restrict f hq ^ n = 0
x : M
hx : x ∈ p
⊢ ↑((LinearMap.restrict f hp ^ n) ⟨x, hx⟩) = ↑(0 ⟨x, hx⟩)
Module: Mathlib.RingTheory.Ideal.MinimalPrime.Basic

Goal state before:
pp: case refine_2
R : Type u_2
inst✝¹ : CommRing R
p I J : Ideal R
inst✝ : p.IsPrime
hle : I ≤ p
h : map (Quotient.mk I) p ∈ (map (Quotient.mk I) J).minimalPrimes
q : Ideal R
x✝ : (fun q ↦ q.IsPrime ∧ I ⊔ J ≤ q) q
hqp : q ≤ p
left✝ : q.IsPrime
hq : I ⊔ J ≤ q
⊢ p ≤ q

Tactic:
rw [sup_le_iff] at hq
    have h2 : p.map (Quotient.mk I) ≤ q.map (Quotient.mk I) :=
      h.2 ⟨isPrime_map_quotientMk_of_isPrime hq.1, map_mono hq.2⟩ (map_mono hqp)
    simpa [comap_map_quotientMk, hq.1, sup_le_iff] using comap_mono (f := Ideal.Quotient.mk I) h2

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Submodule

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
s : Set R
span_eq : Ideal.span s = ⊤
Mₚ : ↑s → Type u_5
inst✝² : (r : ↑s) → AddCommMonoid (Mₚ r)
inst✝¹ : (r : ↑s) → Module R (Mₚ r)
f : (r : ↑s) → M →ₗ[R] Mₚ r
inst✝ : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)
m : M
N : Submodule R M
h : ∀ (r : ↑s), (f r) m ∈ localized₀ (Submonoid.powers ↑r) (f r) N
I : Ideal R := comap (LinearMap.toSpanSingleton R M m) N
ne : I ≠ ⊤
r✝ : R
hrs : r✝ ∈ s
disj : Disjoint ↑I ↑(Submonoid.powers r✝)
r : ↑s := ⟨r✝, hrs⟩
a : M
ha : a ∈ N
t : ↥(Submonoid.powers ↑r)
e : ∃ s_1, s_1 • t • m = s_1 • 1 • a
u : ↥(Submonoid.powers ↑r)
hu : (u * t) • m = (u * 1) • a
⊢ False

Tactic:
exact Set.disjoint_right.mp disj (u * t).2 (by apply hu ▸ smul_mem _ _ ha)

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

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

Tactic:
coeff_mul,

Goal state after:
case e_a.e_a
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
k : ℕ
a₁ a₂ : A
p₁ p₂ : R[X]
⊢ (algebraMap R A) (∑ x ∈ Finset.antidiagonal k, p₁.coeff x.1 * p₂.coeff x.2) =
    ∑ x ∈ Finset.antidiagonal k, (algebraMap R A) (p₁.coeff x.1) * (algebraMap R A) (p₂.coeff x.2)
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
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p

Tactic:
rw [← sum_C_mul_X_pow_eq p]

Goal state after:
R : Type u_1
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : A ⊗[R] R[X]
a : A
p : R[X]
| a ⊗ₜ[R] p.sum fun n a ↦ C a * X ^ n
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
x✝¹ : R[X]
x✝ : A[X]
n✝ : ℕ
⊢ ((mapRingHom (algebraMap R A)) x✝¹ * x✝).coeff n✝ = (x✝ * (mapRingHom (algebraMap R A)) x✝¹).coeff n✝

Tactic:
coeff_mul,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring S
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Algebra R S
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
x✝¹ : R[X]
x✝ : A[X]
n✝ : ℕ
⊢ ∑ x ∈ Finset.antidiagonal n✝, ((mapRingHom (algebraMap R A)) x✝¹).coeff x.1 * x✝.coeff x.2 =
    (x✝ * (mapRingHom (algebraMap R A)) x✝¹).coeff n✝
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: R : Type u_1
inst✝³ : CommSemiring R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
M N : Submonoid R
inst✝ : IsLocalization M S
h : M ≤ N
h' : ∀ (x : ↥N), ∃ m, m * ↑x ∈ M
y : ↥N
m : R
hm : m * ↑y ∈ M
this : IsUnit ((algebraMap R S) m * (algebraMap R S) ↑y)
⊢ IsUnit ((algebraMap R S) ↑y)

Tactic:
exact (IsUnit.mul_iff.mp this).2

Goal state after:
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
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap (↑f.symm) (Ideal.comap (↑f) J)

Tactic:
Ideal.comap_comap,

Goal state after:
R : Type u_1
inst✝⁴ : CommSemiring R
S : Type u_2
inst✝³ : CommSemiring S
inst✝² : Algebra R S
P : Type u_3
inst✝¹ : CommSemiring P
I : Ideal R
hI : I.IsPrime
J : Ideal P
inst✝ : J.IsPrime
f : R ≃+* P
hIJ : I = Ideal.comap f J
⊢ J = Ideal.comap ((↑f).comp ↑f.symm) J
Module: Mathlib.LinearAlgebra.TensorProduct.Quotient

Goal state before:
pp: case refine_1
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
⊢ {x | ∃ a m n, (a • m) ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) = x} ⊆ ↑(mapOfCompatibleSMul A R A M N).ker

Tactic:
rintro - ⟨a, m, n, rfl⟩
    simp [smul_tmul]

Goal state after:
Module: Mathlib.RingTheory.EssentialFiniteness

Goal state before:
pp: R : Type u_1
S : Type u_2
T : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
hf : f.EssFiniteType
g₁ g₂ : S →+* T
h₁ : g₁.comp f = g₂.comp f
h₂ : ∀ x ∈ hf.finset, g₁ x = g₂ x
algInst✝¹ : Algebra R S := f.toAlgebra
algInst✝ : Algebra R T := (g₁.comp f).toAlgebra
algebraizeInst✝ : Algebra.EssFiniteType R S
x : S
⊢ g₁ x = g₂ x

Tactic:
exact DFunLike.congr_fun (Algebra.EssFiniteType.algHom_ext T
    ⟨g₁, fun _ ↦ rfl⟩ ⟨g₂, DFunLike.congr_fun h₁.symm⟩ h₂) x

Goal state after:
Module: Mathlib.Algebra.Polynomial.Laurent

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹ : CommSemiring R
S : Type u_3
inst✝ : CommSemiring S
f : R →+* S
x : Sˣ
⊢ ∀ (y : ↥(Submonoid.powers X)), IsUnit ((eval₂RingHom f ↑x) ↑y)

Tactic:
rintro ⟨y, n, rfl⟩
    simpa only [coe_eval₂RingHom, eval₂_X_pow] using x.isUnit.pow n

Goal state after:
Module: Mathlib.LinearAlgebra.Dimension.Localization

Goal state before:
pp: case inr.refine_1
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
⊢ Algebra.algebraMapSubmonoid FT R⁰ ≤ IsUnit.submonoid FT

Tactic:
rintro _ ⟨_, mem, rfl⟩

Goal state after:
case inr.refine_1
R : Type uR
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
T : Type uT
inst✝⁷ : CommRing T
inst✝⁶ : NoZeroDivisors T
inst✝⁵ : Algebra R T
inst✝⁴ : FaithfulSMul R T
P : Type uP
inst✝³ : AddCommGroup P
inst✝² : Module R P
inst✝¹ : Module T P
inst✝ : IsScalarTower R T P
g✝ : M →ₗ[R] P
bc : IsBaseChange T g✝
this✝¹ : NoZeroDivisors R
h✝ : Nontrivial R
this✝ : IsDomain T
FR : Type uR := FractionRing R
FT : Type uT := FractionRing T
inj : Function.Injective ⇑(algebraMap R FT)
g : P →ₗ[T] FT ⊗[T] P := (TensorProduct.mk T FT P) 1
this : IsLocalizedModule R⁰ ((TensorProduct.mk R FR FT) 1)
x✝ : Algebra FT (FR ⊗[R] FT) := Algebra.TensorProduct.rightAlgebra
w✝ : R
mem : w✝ ∈ ↑R⁰
⊢ (algebraMap R FT) w✝ ∈ IsUnit.submonoid FT
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
⊢ (⅟A)ᵀ = ⅟Aᵀ

Tactic:
let := invertibleTranspose A

Goal state after:
n : Type u_2
α : Type u_3
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : CommSemiring α
A : Matrix n n α
inst✝¹ : Invertible A
inst✝ : Invertible Aᵀ
this : Invertible Aᵀ := A.invertibleTranspose
⊢ (⅟A)ᵀ = ⅟Aᵀ
Module: Mathlib.LinearAlgebra.Matrix.Transvection

Goal state before:
pp: case neg.inr.hnc
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
hM : M (inr ()) (inr ()) ≠ 0
i : Fin r
k n : ℕ
hn : n < r
IH : ((List.drop (n + 1) (listTransvecCol M)).prod * M) (inl i) (inr ()) = if n + 1 ≤ ↑i then 0 else M (inl i) (inr ())
hn' : n < (listTransvecCol M).length
n' : Fin r := ⟨n, hn⟩
A : (listTransvecCol M)[n] = transvection (inl n') (inr ()) (-M (inl n') (inr ()) / M (inr ()) (inr ()))
h : ¬n' = i
hni : n ≠ ↑i
hi : ↑i < n + 1
⊢ ¬n ≤ ↑i

Tactic:
simpa only [hni.symm, not_le, or_false] using Nat.lt_succ_iff_lt_or_eq.1 hi

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Invertible

Goal state before:
pp: m : Type u_1
n : Type u_2
α : Type u_3
inst✝⁷ : Fintype n
inst✝⁶ : DecidableEq n
inst✝⁵ : Fintype m
inst✝⁴ : DecidableEq m
inst✝³ : Ring α
A : Matrix n n α
U : Matrix n m α
C : Matrix m m α
V : Matrix m n α
inst✝² : Invertible A
inst✝¹ : Invertible C
inst✝ : Invertible (⅟C + V * ⅟A * U)
⊢ 1 + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (V + V * ⅟A * U * C * V) =
    1 + ⅟A * U * C * V - ⅟A * U * ⅟(⅟C + V * ⅟A * U) * (⅟C + V * ⅟A * U) * C * V

Tactic:
by
      simp only [Matrix.mul_add, Matrix.add_mul, ← Matrix.mul_assoc,
        Matrix.invOf_mul_cancel_right]

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.Block

Goal state before:
pp: α : Type u_1
m : Type u_3
R : Type v
b : m → α
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq m
i j : m
hij : b i ≤ b j
c : R
⊢ (single i j c).BlockTriangular b

Tactic:
by
  intro r s hrs
  apply single_apply_of_ne
  rintro ⟨rfl, rfl⟩
  exact (hij.trans_lt hrs).false

Goal state after:
Module: Mathlib.LinearAlgebra.Matrix.NonsingularInverse

Goal state before:
pp: case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ

Tactic:
have := isUnit_diagonal.not.mpr h

Goal state after:
case neg
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
v : n → α
h : ¬IsUnit v
this : ¬IsUnit (diagonal v)
⊢ (diagonal v)⁻¹ʳ = diagonal v⁻¹ʳ