mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f c = f (a * b)
⊢ x ∈ map f I ∨ y ∈ map f I

Tactic:
← sub_eq_zero,

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
F : Type u_3
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : FunLike F R S
rc : RingHomClass F R S
f : F
hf : Function.Surjective ⇑f
I : Ideal R
H : I.IsPrime
hk : RingHom.ker f ≤ I
x y : S
a : R
ha : f a = x
b : R
hb : f b = y
c : R
hc : c ∈ I
hc' : f c - f (a * b) = 0
⊢ x ∈ map f I ∨ y ∈ map f I
Module: Mathlib.Algebra.GCDMonoid.Nat

Goal state before:
pp: case refine_2
n : ℕ
⊢ (fun x ↦ x.out.natAbs) ((fun x ↦ Associates.mk ↑x) n) = n

Tactic:
· dsimp only [Associates.out_mk]
    rw [← Int.abs_eq_normalize, Int.natAbs_abs, Int.natAbs_natCast]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ g (f_inv 1) = g 1

Tactic:
← sub_eq_zero,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
⊢ g (f_inv 1) - g 1 = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ g (f_inv (x * y)) = g (f_inv x * f_inv y)

Tactic:
← sub_eq_zero,

Goal state after:
A : Type u_1
B : Type u_2
C : Type u_3
inst✝² : Ring A
inst✝¹ : Ring B
inst✝ : Ring C
f : A →+* B
f_inv : B → A
hf : Function.RightInverse f_inv ⇑f
g : A →+* C
hg : ker f ≤ ker g
x y : B
⊢ g (f_inv (x * y)) - g (f_inv x * f_inv y) = 0
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f g : β → α
hs : ∃ x ∈ s, f x ≠ 0
hg : ∀ b ∈ s, f b = s.gcd f * g b
⊢ s.gcd g = 1

Tactic:
rw [← normalize_gcd, normalize_eq_one, ← associated_one_iff_isUnit]
  refine .of_mul_left (.symm <| .trans ?_ (gcd_mul_left' ..)) .rfl (a := s.gcd f) ?_
  · simp [← gcd_congr rfl hg]
  contrapose! hs
  exact s.gcd_eq_zero_iff.1 hs

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: ι : Type u_1
α : Type u_2
inst✝³ : CommMonoidWithZero α
inst✝² : NormalizedGCDMonoid α
inst✝¹ : Div α
inst✝ : MulDivCancelClass α
f : ι → α
s : Finset ι
i : ι
his : i ∈ s
hfi : f i ≠ 0
⊢ (s.gcd fun j ↦ f j / s.gcd f) = 1

Tactic:
obtain ⟨g, he, hg⟩ := Finset.extract_gcd f ⟨i, his⟩
  refine (Finset.gcd_congr rfl fun a ha ↦ ?_).trans hg
  rw [he a ha, mul_div_cancel_left₀]
  exact mt Finset.gcd_eq_zero_iff.1 fun h ↦ hfi <| h i his

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ m * n
⊢ k ∣ m * gcd k n

Tactic:
rw [mul_comm] at H ⊢

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
m n k : α
H : k ∣ n * m
⊢ k ∣ gcd k n * m
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I P : Ideal R
hP : P.IsPrime
n : ℕ
hn : n ≠ 0
⊢ I ^ n ≤ P ↔ I ≤ P

Tactic:
have h : (Multiset.replicate n I).prod ≤ P ↔ _ := hP.multiset_prod_le
  simp_rw [Multiset.prod_replicate, Multiset.mem_replicate, ne_eq, hn, not_false_eq_true,
    true_and, exists_eq_left] at h
  exact h

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b = gcd a c

Tactic:
apply dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _) <;>
    rw [dvd_gcd_iff] <;>
    refine ⟨gcd_dvd_left _ _, ?_⟩

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a b ∣ c

case hba
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c : α
h : a ∣ b - c
⊢ gcd a c ∣ b
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
⊢ Associated (gcd a b * if a = 0 then 0 else Classical.choose ⋯) (a * b)

Tactic:
split_ifs with a0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * Classical.choose ⋯) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
⊢ (if a = 0 then 0 else Classical.choose ⋯) = 0

Tactic:
split_ifs with a0

Goal state after:
case pos
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
a0 : a = 0
⊢ 0 = 0

case neg
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
a : α
a0 : ¬a = 0
⊢ Classical.choose ⋯ = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
⊢ Associated (gcd a b * if a = 0 then 0 else normalize (Classical.choose ⋯)) (a * b)

Tactic:
split_ifs with a0

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : a = 0
⊢ Associated (gcd a b * 0) (a * b)

case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a b : α
a0 : ¬a = 0
⊢ Associated (gcd a b * normalize (Classical.choose ⋯)) (a * b)
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
⊢ (if a = 0 then 0 else normalize (Classical.choose ⋯)) = 0

Tactic:
split_ifs with a0

Goal state after:
case pos
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
a0 : a = 0
⊢ 0 = 0

case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
gcd : α → α → α
gcd_dvd_left : ∀ (a b : α), gcd a b ∣ a
gcd_dvd_right : ∀ (a b : α), gcd a b ∣ b
dvd_gcd : ∀ {a b c : α}, a ∣ c → a ∣ b → a ∣ gcd c b
normalize_gcd : ∀ (a b : α), normalize (gcd a b) = gcd a b
a : α
a0 : ¬a = 0
⊢ normalize (Classical.choose ⋯) = 0
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : R ∙ a * b < R ∙ a
⊢ IsUnit a

Tactic:
refine (of_irreducible_mul hp).resolve_right (mt (fun hb => ?_) (not_le_of_gt hI))

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
a b : R
hp : Irreducible (a * b)
hI : R ∙ a * b < R ∙ a
hb : IsUnit b
⊢ R ∙ a ≤ R ∙ a * b
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsCoprime p n ↔ ¬p ∣ n

Tactic:
← isRelPrime_iff_isCoprime,

Goal state after:
R : Type u
inst✝¹ : CommRing R
inst✝ : IsBezout R
p n : R
hp : Irreducible p
⊢ IsRelPrime p n ↔ ¬p ∣ n
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, z = x * a + y * b

Tactic:
@eq_comm _ z,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
a b z : R
⊢ gcd a b ∣ z ↔ ∃ x y, x * a + y * b = z
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ ↑(toNat (Module.rank R ↥N)) = Module.rank R ↥N

Tactic:
Cardinal.cast_toNat_of_lt_aleph0

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N = Module.rank R ↥N

R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
inst✝ : Module.Finite R M
N : Submodule R M
⊢ Module.rank R ↥N < ℵ₀
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i

Tactic:
have heq : ⋃ i ∈ s, f i = ⋃ i ∈ t, (f i : Set R) := by
    ext
    simpa using exists_congr (fun i ↦ (and_congr_left fun a ↦ ht i).symm)

Goal state after:
R : Type u_2
ι : Type u_3
inst✝ : CommRing R
s : Set ι
hs : s.Finite
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, i ≠ a → i ≠ b → (f i).IsPrime
I : Ideal R
t : Finset ι
ht : ∀ (a : ι), a ∈ t ↔ a ∈ s
heq : ⋃ i ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)
⊢ ↑I ⊆ ⋃ i ∈ s, ↑(f i) ↔ ∃ i ∈ s, I ≤ f i
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
⊢ M * 1 = M

Tactic:
ext
  rw [← diagonal_one, mul_diagonal, mul_one]

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

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ ¬Ideal.span {r} = ⊥ ↔ r ≠ 0

Tactic:
Ideal.span_singleton_eq_bot

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
r : R
⊢ ¬r = 0 ↔ r ≠ 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: R : Type u_1
ι₁ : Type u_2
ι₂ : Type u_3
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Finite ι₁
inst✝ : Finite ι₂
⊢ Module.Finite R (Matrix ι₁ ι₂ M)

Tactic:
by
  cases nonempty_fintype ι₁
  cases nonempty_fintype ι₂
  exact Module.Finite.of_basis <| (Free.chooseBasis _ _).matrix _ _

Goal state after:
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ ((b.smulTower c).reindex (Equiv.prodComm ι ι')) ij = b ij.2 • c ij.1

Tactic:
reindex_apply,

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
ij : ι' × ι
⊢ (b.smulTower c) ((Equiv.prodComm ι ι').symm ij) = b ij.2 • c ij.1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (reindex e e) (A * B) = (reindex e e) 1 ↔ B * A = 1

Tactic:
reindex_apply,

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = (reindex e e) 1 ↔ B * A = 1
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = (reindex e e) 1 ↔ B * A = 1

Tactic:
reindex_apply,

Goal state after:
m : Type u_10
n : Type u_11
R : Type u_12
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : MulOne R
inst✝¹ : AddCommMonoid R
inst✝ : IsStablyFiniteRing R
A : Matrix m n R
B : Matrix n m R
e : m ≃ n
⊢ (A * B).submatrix ⇑e.symm ⇑e.symm = submatrix 1 ⇑e.symm ⇑e.symm ↔ B * A = 1
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α →₀ ℕ
g : α → β
⊢ Multiset.map g (toMultiset f) = toMultiset (mapDomain g f)

Tactic:
refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.map_zero, mapDomain_zero, toMultiset_zero]
  · intro a n f _ _ ih
    rw [toMultiset_add, Multiset.map_add, ih, mapDomain_add, mapDomain_single,
      toMultiset_single, toMultiset_add, toMultiset_single, ← Multiset.coe_mapAddMonoidHom,
      (Multiset.mapAddMonoidHom g).map_nsmul]
    rfl

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
⊢ ∀ (a : α) (b : ℕ) (f : α →₀ ℕ),
    a ∉ f.support →
      b ≠ 0 → (toMultiset f).toFinset = f.support → (toMultiset (single a b + f)).toFinset = (single a b + f).support

Tactic:
· intro a n f ha hn ih
    rw [toMultiset_add, Multiset.toFinset_add, ih, toMultiset_single, support_add_eq,
      support_single _ hn, Multiset.toFinset_nsmul _ _ hn, Multiset.toFinset_singleton]
    refine Disjoint.mono_left support_single_subset ?_
    rwa [Finset.disjoint_singleton_left]

Goal state after:
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
inst✝⁴ : Semiring α
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : Fintype m
r : α
M : Matrix m n α
⊢ (scalar m) r * M = M * (scalar n) r ↔ r • M = MulOpposite.op r • M

Tactic:
by
  simp_rw [scalar_apply, ← smul_eq_diagonal_mul, ← op_smul_eq_mul_diagonal]

Goal state after:
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ count a✝ {a} = (Finsupp.single a 1) a✝

Tactic:
count_singleton,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (if a✝ = a then 1 else 0) = (Finsupp.single a 1) a✝
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} (Module.rank K A)) =
    lift.{v, w} (Module.rank F A)

Tactic:
← c.mk_eq_rank,

Goal state after:
F : Type u
K : Type v
A : Type w
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : AddCommMonoid A
inst✝⁷ : Module F K
inst✝⁶ : Module K A
inst✝⁵ : Module F A
inst✝⁴ : IsScalarTower F K A
inst✝³ : StrongRankCondition F
inst✝² : StrongRankCondition K
inst✝¹ : Free F K
inst✝ : Free K A
b : Basis (Free.ChooseBasisIndex F K) F K := Free.chooseBasis F K
c : Basis (Free.ChooseBasisIndex K A) K A := Free.chooseBasis K A
⊢ lift.{w, v} (lift.{v, v} #(Free.ChooseBasisIndex F K)) * lift.{v, w} (lift.{w, w} #(Free.ChooseBasisIndex K A)) =
    lift.{v, w} (Module.rank F A)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
B✝ : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B✝
inst✝¹ : Algebra R B✝
S T U : Subalgebra R A
inst✝ : Subsingleton A
B C : Subalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

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

Goal state before:
pp: R : Type u
A : Type v
B✝ : Type w
inst✝³ : CommSemiring R
inst✝² : NonUnitalNonAssocSemiring A
inst✝¹ : Module R A
S : NonUnitalSubalgebra R A
inst✝ : Subsingleton A
B C : NonUnitalSubalgebra R A
x : A
⊢ x ∈ B ↔ x ∈ C

Tactic:
simp only [Subsingleton.elim x 0, zero_mem B, zero_mem C]

Goal state after:
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inl
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
j' : J
l' : L
hj : j ≠ j'
⊢ single i j (single k l r) i j' k' l' = single (i, k) (j, l) r (i, k') (j', l')

pp: case inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
· rw [single_apply_of_col_ne _ _ hj,
      single_apply_of_col_ne _ _ (ne_of_apply_ne Prod.fst hj), Matrix.zero_apply]

Goal state after:
case inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ single i j (single k l r) i j k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
rw [single_apply_same]

Goal state after:
case inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
k' : K
l' : L
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (star ↑u)⁻¹ʳ = star (↑u)⁻¹ʳ

Tactic:
Ring.inverse_unit,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (star ↑u)⁻¹ʳ = star ↑u⁻¹
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ (↑(star u))⁻¹ʳ = star ↑u⁻¹

Tactic:
Ring.inverse_unit,

Goal state after:
case pos
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
u : Rˣ
⊢ ↑(star u)⁻¹ = star ↑u⁻¹
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : Monoid R
inst✝³ : StarMul R
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint ↑r
hrx : IsSelfAdjoint (↑r • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)

Tactic:
replace hr : IsSelfAdjoint r := Units.ext hr.star_eq

Goal state after:
R : Type u_1
A : Type u_2
inst✝⁴ : Monoid R
inst✝³ : StarMul R
inst✝² : Star A
inst✝¹ : MulAction R A
inst✝ : StarModule R A
x : A
r : Rˣ
hrx : IsSelfAdjoint (↑r • x)
hr : IsSelfAdjoint r
⊢ IsSelfAdjoint (r⁻¹ • r • x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ Commute (star (a + b)) (a + b)

Tactic:
simp only [star_add, commute_iff_eq, mul_add, add_mul]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocSemiring R
inst✝ : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ (M.updateCol j c).map f i✝ j✝ = (M.map f).updateCol j (f ∘ c) i✝ j✝

Tactic:
rw [updateCol_apply, map_apply, map_apply, updateCol_apply]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
M : Matrix m n α
j : n
c : m → α
inst✝ : DecidableEq n
f : α → β
i✝ : m
j✝ : n
⊢ f (if j✝ = j then c i✝ else M i✝ j✝) = if j✝ = j then (f ∘ c) i✝ else f (M i✝ j✝)