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

Goal state before:
pp: case pos
α : 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))
hga : g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

pp: case neg
α : 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))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a

Tactic:
· rw [ContinuousAt]
    simp_rw [comp_apply, hga, div_zero]
    exact (h2h hga).comp (continuousAt_id.tendsto.prodMk tendsto_top)

Goal state after:
case neg
α : 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))
hga : ¬g a = 0
⊢ ContinuousAt (↿h ∘ fun x ↦ (x, f x / g x)) a
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' Ioo a b = Ioo (update f i a) (update f i b)

Tactic:
← Ico_sdiff_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' (Ico a b \ {a}) = Ioo (update f i a) (update f i b)
Module: Mathlib.Order.Interval.Set.Pi

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' (Ico a b \ {a}) = Ioo (update f i a) (update f i b)

Tactic:
← Ico_sdiff_left,

Goal state after:
ι : Type u_1
α : ι → Type u_2
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → PartialOrder (α i)
f : (i : ι) → α i
i : ι
a b : α i
⊢ update f i '' (Ico a b \ {a}) = Ico (update f i a) (update f i b) \ {update f i a}
Module: Mathlib.Topology.Algebra.Order.Group

Goal state before:
pp: case inl
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
δ : G
hδ₁ : 1 < δ
hδε : δ < ε
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

pp: case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε

Tactic:
· filter_upwards [(eventually_mabs_div_lt _ hδ₁).prod_nhds
        (eventually_mabs_div_lt _ (one_lt_div'.mpr hδε))]
      rintro ⟨c, d⟩ ⟨hc, hd⟩
      calc
        |c * d / (a * b)|ₘ = |(c / a) * (d / b)|ₘ := by rw [div_mul_div_comm]
        _ ≤ |c / a|ₘ * |d / b|ₘ := mabs_mul_le ..
        _ < δ * (ε / δ) := mul_lt_mul_of_lt_of_lt hc hd
        _ = ε := mul_div_cancel ..

Goal state after:
case inr
G : Type u_1
inst✝⁴ : TopologicalSpace G
inst✝³ : CommGroup G
inst✝² : LinearOrder G
inst✝¹ : IsOrderedMonoid G
inst✝ : OrderTopology G
a b ε : G
hε : ε > 1
hε_min : ∀ a < ε, a ≤ 1
⊢ ∀ᶠ (b_1 : G × G) in 𝓝 (a, b), |b_1.1 * b_1.2 / (a * b)|ₘ < ε
Module: Mathlib.Topology.Algebra.IsUniformGroup.Basic

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ W' ∈
    map (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1)
      (comap (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) (𝓝 (x₀, y₀) ×ˢ 𝓝 (x₀, y₀)))

Tactic:
rw [mem_map, mem_comap, nhds_prod_eq]

Goal state after:
case right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
G : Type u_5
inst✝¹⁴ : TopologicalSpace α
inst✝¹³ : AddCommGroup α
inst✝¹² : IsTopologicalAddGroup α
inst✝¹¹ : TopologicalSpace β
inst✝¹⁰ : AddCommGroup β
inst✝⁹ : TopologicalSpace γ
inst✝⁸ : AddCommGroup γ
inst✝⁷ : IsTopologicalAddGroup γ
inst✝⁶ : TopologicalSpace δ
inst✝⁵ : AddCommGroup δ
inst✝⁴ : UniformSpace G
inst✝³ : AddCommGroup G
e : β →+ α
de : IsDenseInducing ⇑e
f : δ →+ γ
df : IsDenseInducing ⇑f
φ : β →+ δ →+ G
hφ : Continuous[instTopologicalSpaceProd, inst✝⁴.toTopologicalSpace] fun p ↦ (φ p.1) p.2
inst✝² : IsUniformAddGroup G
inst✝¹ : T0Space G
inst✝ : CompleteSpace G
x₀ : α
y₀ : γ
W' : Set G
W'_nhds : W' ∈ 𝓝 0
U : Set β
V : Set δ
h : ∀ x ∈ U, ∀ x' ∈ U, ∀ y ∈ V, ∀ y' ∈ V, (fun p ↦ (φ p.1) p.2) (x', y') - (fun p ↦ (φ p.1) p.2) (x, y) ∈ W'
U' : Set α
U'_nhds : U' ∈ 𝓝 x₀
U'_sub : ⇑e ⁻¹' U' ⊆ U
V' : Set γ
V'_nhds : V' ∈ 𝓝 y₀
V'_sub : ⇑f ⁻¹' V' ⊆ V
⊢ ∃ t ∈ (𝓝 x₀ ×ˢ 𝓝 y₀) ×ˢ 𝓝 x₀ ×ˢ 𝓝 y₀,
    (fun p ↦ ((e p.1.1, f p.1.2), e p.2.1, f p.2.2)) ⁻¹' t ⊆
      (fun p ↦ (fun p ↦ (φ p.1) p.2) p.2 - (fun p ↦ (φ p.1) p.2) p.1) ⁻¹' W'
Module: Mathlib.Topology.Order.LeftRightNhds

Goal state before:
pp: α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε ↦ 1 < ε) fun ε ↦ Ioo (a / ε) (a * ε)

Tactic:
convert! nhds_basis_mabs_div_lt a

Goal state after:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CommGroup α
inst✝³ : LinearOrder α
inst✝² : IsOrderedMonoid α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x✝ : α
⊢ Ioo (a / x✝) (a * x✝) = {b | |b / a|ₘ < x✝}
Module: Mathlib.Logic.Equiv.PartialEquiv

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

Tactic:
simp only [trans_source, restr_source, refl_source, univ_inter]
    rw [← inter_assoc, inter_self]

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

Goal state before:
pp: 𝕜 : Type u_1
inst✝² : AddCommGroup 𝕜
p : 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsOrderedAddMonoid 𝕜
n : ℕ
hn : 0 < n
x✝ : 𝕜
⊢ n • x✝ = 0 → x✝ = 0

Tactic:
by simp [hn.ne']

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

Goal state before:

Tactic:
f x < z x := (hz x hx).1
      _ ≤ f y := (hz x hx).2 y hy.1 hxy

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

Goal state before:
pp: case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ↑((MonoOver.forget M).obj (representative.obj S)).1 ≃ₗ[R] ↥((fun S ↦ (Hom.hom S.arrow).range) S)

Tactic:
apply LinearEquiv.ofBijective (LinearMap.codRestrict
            (LinearMap.range S.arrow.hom) S.arrow.hom _)

Goal state after:
case i
R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ Function.Bijective ⇑(LinearMap.codRestrict (Hom.hom S.arrow).range (Hom.hom S.arrow) ?m.424)

R : Type u
inst✝ : Ring R
M : ModuleCat R
S : Subobject M
⊢ ∀ (c : ↑(underlying.obj S)), (Hom.hom S.arrow) c ∈ (Hom.hom S.arrow).range
Module: Mathlib.Algebra.Category.ModuleCat.Subobject

Goal state before:
pp: R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
x y : ↑N
l : ↑L
w : x = y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)
⊢ (ConcreteCategory.hom (cokernel.π g)) x = (ConcreteCategory.hom (cokernel.π g)) y

Tactic:
subst w

Goal state after:
R : Type u
inst✝² : Ring R
L M N : ModuleCat R
f : L ⟶ M
inst✝¹ : HasImage f
g : underlying.obj (imageSubobject f) ⟶ N
inst✝ : HasCokernel g
y : ↑N
l : ↑L
⊢ (ConcreteCategory.hom (cokernel.π g))
      (y + (ConcreteCategory.hom g) ((ConcreteCategory.hom (factorThruImageSubobject f)) l)) =
    (ConcreteCategory.hom (cokernel.π g)) y
Module: Mathlib.CategoryTheory.Preadditive.CommGrp_

Goal state before:
pp: case refine_3
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : BraidedCategory C
⊢ ∀ {X Y : CommGrp C} (f : X ⟶ Y),
    (CommGrp.forget C ⋙ toCommGrp C).map f ≫
        (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj Y).X) ⋯ ⋯).hom =
      (CommGrp.mkIso (Iso.refl ((CommGrp.forget C ⋙ toCommGrp C).obj X).X) ⋯ ⋯).hom ≫ (𝟭 (CommGrp C)).map f

Tactic:
· cat_disch

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

Goal state before:
pp: case mp
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : ShortComplex C
⊢ (∀ ⦃A : C⦄ (y : A ⟶ S.cycles), ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ S.toCycles) →
    ∀ ⦃A : C⦄ (x₂ : A ⟶ S.X₂), x₂ ≫ S.g = 0 → ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ S.f

Tactic:
intro hS A a ha
    obtain ⟨A', π, hπ, x₁, fac⟩ := hS (S.liftCycles a ha)
    exact ⟨A', π, hπ, x₁, by simpa only [assoc, liftCycles_i, toCycles_i] using fac =≫ S.iCycles⟩

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

Goal state before:
pp: case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.g = 0 →
      ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f

Tactic:
obtain ⟨A', π, hπ, x₁, fac⟩ := h y hy

Goal state after:
case refine_1
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
A : C
y : A ⟶ Y
hy : y ≫ Cofork.π c = 0
h :
  ∀ ⦃A : C⦄ (x₂ : A ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.X₂),
    x₂ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.g = 0 →
      ∃ A' π, ∃ (_ : Epi π), ∃ x₁, π ≫ x₂ = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
A' : C
π : A' ⟶ A
hπ : Epi π
x₁ : A' ⟶ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.X₁
fac : π ≫ y = x₁ ≫ { X₁ := X, X₂ := Y, X₃ := c.pt, f := f, g := Cofork.π c, zero := ⋯ }.f
⊢ ∃ A' π, ∃ (_ : Epi π), ∃ x, π ≫ y = x ≫ f
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
⊢ (S.v₀₁ ≫ S.v₁₂).τ₁ = 0

Tactic:
S.w₀₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Hom.τ₁ 0 = 0
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
⊢ (S.v₀₁ ≫ S.v₁₂).τ₂ = 0

Tactic:
S.w₀₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Hom.τ₂ 0 = 0
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
⊢ (S.v₀₁ ≫ S.v₁₂).τ₃ = 0

Tactic:
S.w₀₂,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ Hom.τ₃ 0 = 0
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
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.right b) = E.π.app (WalkingMulticospan.right b)

Tactic:
← E.w (WalkingMulticospan.Hom.fst b),

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
J : MulticospanShape
I : MulticospanIndex J C
K : Multifork I
lift : (E : Multifork I) → E.pt ⟶ K.pt
fac : ∀ (E : Multifork I) (i : J.L), lift E ≫ K.ι i = E.ι i
uniq : ∀ (E : Multifork I) (m : E.pt ⟶ K.pt), (∀ (i : J.L), m ≫ K.ι i = E.ι i) → m = lift E
E : Cone I.multicospan
b : J.R
⊢ lift E ≫ K.π.app (WalkingMulticospan.right b) =
    E.π.app (WalkingMulticospan.left (J.fst b)) ≫ I.multicospan.map (WalkingMulticospan.Hom.fst b)
Module: Mathlib.CategoryTheory.ComposableArrows.Basic

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

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

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

Goal state before:
pp: case zero
C : Type u
inst✝ : Category.{v, u} C
⊢ Nonempty (StructuredArrow WalkingReflexivePair.zero inclusionWalkingReflexivePair)

Tactic:
exact ⟨StructuredArrow.mk (Y := one) (𝟙 _)⟩

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

Goal state before:
pp: M : Type u_1
N : Type u_2
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
I : Ideal R
H : I.IsPrime
g : M
⊢ (g • I).IsPrime

Tactic:
rw [I.pointwise_smul_eq_comap]

Goal state after:
M : Type u_1
N : Type u_2
R : Type u_3
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
I : Ideal R
H : I.IsPrime
g : M
⊢ (Ideal.comap (RingEquiv.symm ((MulSemiringAction.toRingAut M R) g)) I).IsPrime
Module: Mathlib.Algebra.Ring.Action.Pointwise.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
b : β
hb : b ∈ t
h : (fun x1 x2 ↦ x1 • x2) a b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

Tactic:
obtain rfl | rfl := smul_eq_zero.1 h

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
s : Set α
t : Set β
b : β
hb : b ∈ t
ha : 0 ∈ s
h : (fun x1 x2 ↦ x1 • x2) 0 b = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty

case inr
α : Type u_1
β : Type u_2
inst✝⁴ : Semiring α
inst✝³ : AddCommMonoid β
inst✝² : Module α β
inst✝¹ : IsDomain α
inst✝ : Module.IsTorsionFree α β
s : Set α
t : Set β
a : α
ha : a ∈ s
hb : 0 ∈ t
h : (fun x1 x2 ↦ x1 • x2) a 0 = 0
⊢ 0 ∈ s ∧ t.Nonempty ∨ 0 ∈ t ∧ s.Nonempty
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ IsLocalizedModule.mk' (Algebra.linearMap R S) r s • n ∈ I • restrictScalars R N'

Tactic:
rw [← IsLocalization.mk'_eq_mk', IsLocalization.mk'_eq_mul_mk'_one, mul_smul, algebraMap_smul]

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁷ : CommSemiring R
inst✝⁶ : CommSemiring S
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Algebra R S
inst✝² : Module S N
inst✝¹ : IsScalarTower R S N
p : Submonoid R
inst✝ : IsLocalization p S
I : Submodule R R
N' : Submodule S N
x : N
hx : x ∈ restrictScalars R (localized' S p (Algebra.linearMap R S) I • N')
r : R
hr : r ∈ I
s : ↥p
n : N
hn : n ∈ N'
⊢ r • IsLocalization.mk' S 1 s • n ∈ I • restrictScalars R N'
Module: Mathlib.Algebra.Module.LocalizedModule.Submodule

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
N✝ : Type u_4
inst✝²¹ : CommSemiring R✝
inst✝²⁰ : CommSemiring S✝
inst✝¹⁹ : AddCommMonoid M✝
inst✝¹⁸ : AddCommMonoid N✝
inst✝¹⁷ : Module R✝ M✝
inst✝¹⁶ : Module R✝ N✝
inst✝¹⁵ : Algebra R✝ S✝
inst✝¹⁴ : Module S✝ N✝
inst✝¹³ : IsScalarTower R✝ S✝ N✝
p✝ : Submonoid R✝
inst✝¹² : IsLocalization p✝ S✝
f✝ : M✝ →ₗ[R✝] N✝
inst✝¹¹ : IsLocalizedModule p✝ f✝
M'✝¹ M'' : Submodule R✝ M✝
R : Type u_5
S : Type u_6
M : Type u_7
N : Type u_8
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : AddCommGroup M
inst✝⁷ : AddCommGroup N
inst✝⁶ : Module R M
inst✝⁵ : Module R N
inst✝⁴ : Algebra R S
inst✝³ : Module S N
inst✝² : IsScalarTower R S N
p : Submonoid R
inst✝¹ : IsLocalization p S
f : M →ₗ[R] N
inst✝ : IsLocalizedModule p f
M'✝ M' : Submodule R M
x : ↥p
m : N ⧸ localized' S p f M'
⊢ ((algebraMap R (Module.End R (N ⧸ localized' S p f M'))) ↑x) (IsLocalization.mk' S 1 x • m) = m

Tactic:
by rw [Module.algebraMap_end_apply, ← smul_assoc, smul_mk'_one, mk'_self', one_smul]

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
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)
inst✝¹ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst✝ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
h : ∀ (P : Ideal R) [inst : P.IsMaximal], Subsingleton (Mₚ P)
⊢ Subsingleton M

Tactic:
rw [subsingleton_iff_forall_eq 0]
  intro x
  exact Module.eq_of_localization_maximal Mₚ f x 0 fun _ _ ↦ Subsingleton.elim _ _

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
p : R[X]
⊢ a • ∑ i ∈ p.support, Polynomial.map (algebraMap R A) ((monomial i) (p.coeff i)) =
    p.sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)

Tactic:
simp [Finset.smul_sum, sum, ← smul_eq_mul]

Goal state after:
Module: Mathlib.RingTheory.PolynomialAlgebra

Goal state before:
pp: case refine_2
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]
⊢ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) (p.sum fun n r ↦ (monomial n) (a * (algebraMap R A) r)) = a ⊗ₜ[R] p

Tactic:
eval₂_sum

Goal state after:
case refine_2
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]
⊢ (p.sum fun n a_1 ↦ eval₂ (↑includeLeft) (1 ⊗ₜ[R] X) ((monomial n) (a * (algebraMap R A) a_1))) = a ⊗ₜ[R] p
Module: Mathlib.RingTheory.Localization.LocalizationLocalization

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ (algebraMap R S) ↑c * (↑z * (algebraMap R S) ↑s) = ↑z * ((algebraMap R S) ↑c * (algebraMap R S) ↑s)

Tactic:
mul_left_comm

Goal state after:
case refine_1
R : Type u_1
inst✝⁸ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
N : Submonoid S
T : Type u_3
inst✝⁵ : CommSemiring T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsLocalization M S
inst✝ : IsLocalization N T
x y : R
z : ↥N
eq₁ : ↑z * (algebraMap R S) x = ↑z * (algebraMap R S) y
z' : R
s : ↥M
eq₂ : ↑z * (algebraMap R S) ↑s = (algebraMap R S) z'
this : (algebraMap R S) (x * z') = (algebraMap R S) (y * z')
c : ↥M
eq₃ : ↑c * (x * z') = ↑c * (y * z')
⊢ ↑z * ((algebraMap R S) ↑c * (algebraMap R S) ↑s) = ↑z * ((algebraMap R S) ↑c * (algebraMap R S) ↑s)
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]

Goal state after:
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
⊢ a • m ⊗ₜ[R] n - m ⊗ₜ[R] (a • n) ∈ S
Module: Mathlib.LinearAlgebra.Matrix.Adjugate

Goal state before:
pp: case map_add
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
i : n
⊢ A.cramerMap (x✝ + y✝) i = (A.cramerMap x✝ + A.cramerMap y✝) i

Tactic:
apply (cramerMap_is_linear A i).1

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

Goal state before:
pp: n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = ((M.updateRow k (Pi.single i 1)).map ⇑f).det

Tactic:
← RingHom.mapMatrix_apply,

Goal state after:
n : Type v
inst✝³ : DecidableEq n
inst✝² : Fintype n
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
M : Matrix n n R
i k : n
this : Pi.single i 1 = ⇑f ∘ Pi.single i 1
⊢ f (M.adjugate i k) = (f.mapMatrix (M.updateRow k (Pi.single i 1))).det
Module: Mathlib.LinearAlgebra.Matrix.Trace

Goal state before:
pp: n : Type u_3
R : Type u_6
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (vecMulVec a b).trace = a ⬝ᵥ b

Tactic:
by
  rw [vecMulVec_eq Unit, trace_replicateCol_mul_replicateRow]

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

Goal state before:
pp: n : Type u_10
α : Type u_12
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : AddCommMonoid α
i j : n
c : α
h : i ≠ j
⊢ (single i j c).trace = 0

Tactic:
simp [trace, h]

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

Goal state before:
pp: n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ A.det⁻¹ʳ • A.adjugate = 0

Tactic:
Ring.inverse_non_unit _ h,

Goal state after:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
h : ¬IsUnit A.det
⊢ 0 • A.adjugate = 0