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

Goal state before:
pp: A : Type u_1
B : Type u_2
M : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
inst✝ : Monoid M
ψ : AddChar B M
hψ : Injective ⇑ψ
⊢ Injective fun f ↦ ψ.compAddMonoidHom f

Tactic:
rintro f g h
  rw [DFunLike.ext'_iff] at h ⊢; exact hψ.comp_left h

Goal state after:
Module: Mathlib.LinearAlgebra.LinearIndependent.Lemmas

Goal state before:
pp: R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ x ∈ span K (range v)

Tactic:
rw [(eq_inv_smul_iff₀ hc').mpr (eq_neg_of_add_eq_zero_left heq), smul_neg]

Goal state after:
R : Type u_6
K : Type u_7
M : Type u_8
inst✝⁷ : CommRing R
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup M
inst✝⁴ : Algebra R K
inst✝³ : Module K M
inst✝² : Module R M
inst✝¹ : IsScalarTower R K M
inst✝ : FaithfulSMul R K
n : ℕ
v : Fin n → M
hv : LinearIndependent R v
x : M
hx : x ∉ span K (range v)
c : R
y : M
hcy : y ∈ span R (range v)
heq : (algebraMap R K) c • x + y = 0
hc : ¬c = 0
hc' : (algebraMap R K) c ≠ 0
⊢ -(((algebraMap R K) c)⁻¹ • y) ∈ span K (range v)
Module: Mathlib.Data.Finset.NAry

Goal state before:
pp: α : Type u_1
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝¹ : DecidableEq γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
f : α → γ → δ
g : β → γ
⊢ ↑(image₂ f s (image g t)) = ↑(image₂ (fun a b ↦ f a (g b)) s t)

Tactic:
push_cast
    exact image2_image_right _ _

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Defs

Goal state before:
pp: R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ ∃ b, a * b = 1 ∧ b * a = 1

Tactic:
refine ⟨x.coeff 1, ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ a * x.coeff 1 = 1

case refine_2
R : Type u_1
S : Type u_2
G : Type u_3
M : Type u_4
N : Type u_5
O : Type u_6
ι : Type u_7
inst✝² : Semiring R
x✝ y : R[M]
r r₁ r₂ : R
m m' m₁ m₂ m₁' m₂' : M
inst✝¹ : Monoid M
inst✝ : Monoid N
a : R
x : R[M]
hax : singleOneRingHom a * x = 1
hxa : x * singleOneRingHom a = 1
⊢ x.coeff 1 * a = 1
Module: Mathlib.Data.Finset.Sort

Goal state before:
pp: case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := ⋯
⊢ s.min' H ≤ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩

Tactic:
have : l.get ⟨0, h⟩ ∈ s := (Finset.mem_sort (α := α) (· ≤ ·)).1 (List.get_mem l _)

Goal state after:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (s.sort fun a b ↦ a ≤ b).length
H : s.Nonempty
l : List α := s.sort fun a b ↦ a ≤ b
this : l.get ⟨0, h⟩ ∈ s
⊢ s.min' H ≤ (s.sort fun a b ↦ a ≤ b).get ⟨0, h⟩
Module: Mathlib.Algebra.Group.UniqueProds.Basic

Goal state before:
pp: case refl.inl
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b2 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b = (fun x ↦ a * x) b2
this : b ∈ {b, b2}
hu : UniqueMul {a} {b, b2} a b
⊢ b = b2

pp: case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b

Tactic:
· exact (hu ha (mem_insert_of_mem <| mem_singleton_self b2) he.symm).2.symm

Goal state after:
case refl.inr
G : Type u
inst✝¹ : Mul G
inst✝ : UniqueProds G
a b1 b : G
ha : a ∈ {a}
he : (fun x ↦ a * x) b1 = (fun x ↦ a * x) b
this : b1 ∈ {b1, b}
hu : UniqueMul {a} {b1, b} a b
⊢ b1 = b
Module: Mathlib.Algebra.Polynomial.Basic

Goal state before:
pp: R : Type u
a : R
n : ℕ
inst✝ : Semiring R
h : n ≠ 0
⊢ (C a).coeff n = 0

Tactic:
rw [coeff_C, if_neg h]

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: S : Type u_5
inst✝² : Semiring S
M : Type u_6
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
f : M →ₗ[S] M
⊢ (∃ p, IsProj p f) ↔ IsIdempotentElem f

Tactic:
by
  refine ⟨fun ⟨p, hp⟩ => ?_, fun h => ⟨_, IsIdempotentElem.isProj_range _ h⟩⟩
  ext x
  exact hp.map_id (f x) (hp.map_mem x)

Goal state after:
Module: Mathlib.LinearAlgebra.Projection

Goal state before:
pp: E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    (f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T)) ∧
      f.range ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm ∧
        f.ker ∈ Module.End.invtSubmodule ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm

Tactic:
← hf.commute_iff,

Goal state after:
E : Type u_1
R : Type u_2
inst✝² : Ring R
inst✝¹ : AddCommGroup E
inst✝ : Module R E
f : E →ₗ[R] E
hf : IsIdempotentElem f
T : (E →ₗ[R] E)ˣ
⊢ Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ↔
    Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T) ∧
      Commute f ↑((GeneralLinearGroup.generalLinearEquiv R E) T).symm
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
m : M
_hm : m ∈ p
n : N
hn : n ∈ ⊥
⊢ (f m) n ∈ ⊥

Tactic:
rw [Submodule.mem_bot] at hn
      rw [hn, map_zero]; simp only [mem_bot]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Bilinear

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = span R (image2 (fun m n ↦ (f m) n) ↑p ↑q)

Tactic:
← map₂_span_span,

Goal state after:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = map₂ f (span R ↑p) (span R ↑q)
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
hf : StrictMono f
x : α
p : LTSeries α
hlast : RelSeries.last p = x
⊢ RelSeries.last (p.map f hf) = f x

Tactic:
by simp [hlast]

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: case coe
α✝ : Type u_1
inst✝² : Preorder α✝
α : Type u_1
inst✝¹ : Preorder α
inst✝ : Nonempty α
hnottop : krullDim α < ⊤
a : α
this✝ : height a < ⊤
this : coheight a < ⊤
n : ℕ
hh : height a = ↑n
x✝ : ℕ∞
hch : coheight a = x✝
⊢ ↑n + x✝ ≤ ⨆ p, ↑p.length

Tactic:
cases hch : coheight a with

Goal state after:
Module: Mathlib.Order.KrullDimension

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
⊢ False

Tactic:
have h_lt : n' < n := ENat.natCast_lt_natCast.mp
        (h' ▸ hn' ▸ height_strictMono h'' (hn' ▸ ENat.natCast_lt_top _))

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : PartialOrder β
m : ℕ
f : α →o β
h : ∀ (x : β), krullDim ↑(⇑f ⁻¹' {x}) ≤ ↑m
n : ℕ
ih : ∀ m_1 < n, ∀ (x : α), height (f x) = ↑m_1 → height x ≤ (↑m + 1) * ↑m_1 + ↑m
x : α
h' : height (f x) = ↑n
p : LTSeries α
hp : RelSeries.last p ≤ x
h_len : (↑m + 1) * ↑n + ↑m < ↑p.length
i : Fin (p.length + 1) := ⟨p.length - (m + 1), ⋯⟩
h'' : f (p.toFun i) < f x
n' : ℕ
hn' : ↑n' = height (f (p.toFun i))
h_lt : n' < n
⊢ False
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonUnitalNonAssocRing R
x y : AddSubmonoid R
⊢ x * -y = -(x * y)

Tactic:
refine le_antisymm (mul_le.2 fun m hm n hn => ?_)
      ((AddSubmonoid.neg_le _ _).2 <| mul_le.2 fun m hm n hn => ?_) <;>
        simp only [AddSubmonoid.mem_neg, ← mul_neg] at *
    · exact mul_mem_mul hm hn
    · exact mul_mem_mul hm (neg_mem_neg.2 hn)

Goal state after:
Module: Mathlib.Algebra.Ring.Submonoid.Pointwise

Goal state before:
pp: M✝ : Type u_1
R : Type u_2
A : Type u_3
inst✝ : NonAssocSemiring R
M : AddSubmonoid R
⊢ M * 1 = M

Tactic:
by rw [one_eq_closure_one_set, ← closure_eq M, closure_mul_closure, mul_one]

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

Goal state before:
pp: R : Type u
inst✝⁶ : Semiring R
A : Type v
inst✝⁵ : Semiring A
inst✝⁴ : Module R A
M : Type u_1
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module A M
inst✝ : IsScalarTower R A M
ι : Sort u_2
t✝ : ι → Submodule R A
N : Submodule R M
t : A
ht : t ∈ ⨆ i, t✝ i
s : M
hs : s ∈ N
x y : A
⊢ x • s ∈ ⨆ i, t✝ i • N → y • s ∈ ⨆ i, t✝ i • N → (x + y) • s ∈ ⨆ i, t✝ i • N

Tactic:
simp_rw [add_smul]; apply add_mem

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

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
n : ℕ
⊢ span R s ^ (n + 1) = span R (s ^ (n + 1))

Tactic:
rw [pow_succ, pow_succ, span_pow s n, span_mul_span]

Goal state after:
Module: Mathlib.RingTheory.Noetherian.Orzech

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
⊢ Injective ⇑f

Tactic:
have := isNoetherian_of_injective i hi

Goal state after:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Injective ⇑f
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
| comap f (I • p)

Tactic:
← Submodule.map_comap_eq_self hp,

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type w
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Injective ⇑f
p : Submodule R M'
hp : p ≤ f.range
I : Ideal R
| comap f (I • map f (comap f p))
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u
S : Type v
F : Type u_1
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : FunLike F R S
f : F
I : Ideal R
inst✝ : RingHomClass F R S
hf : Function.Injective ⇑f
⊢ comap f ⊥ ≤ I

Tactic:
refine le_trans (fun x hx => ?_) bot_le
  rw [mem_comap, Submodule.mem_bot, ← map_zero f] at hx
  exact Eq.symm (hf hx) ▸ Submodule.zero_mem ⊥

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

Goal state before:
pp: R : Type u_1
inst✝ : EuclideanDomain R
a b : R
n : ℕ
hab : b ∣ a
⊢ (a / b) ^ n = a ^ n / b ^ n

Tactic:
by
  obtain ⟨c, rfl⟩ := hab
  obtain rfl | hb := eq_or_ne b 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  · simp [hb, mul_pow]

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

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M = ⊥ ↔ FaithfulSMul R M

Tactic:
← le_bot_iff

Goal state after:
R : Type u_4
M : Type u_5
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ annihilator R M ≤ ⊥ ↔ FaithfulSMul R M
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr.inr
R : Type u
inst✝ : EuclideanDomain R
c d : R
hc0 : c ≠ 0
hd0 : d ≠ 0
k1 k2 : R
⊢ c * k1 * (d * k2) / (c * d) = c * k1 / c * (d * k2 / d)

Tactic:
rw [mul_div_cancel_left₀ _ hc0, mul_div_cancel_left₀ _ hd0, mul_mul_mul_comm,
    mul_div_cancel_left₀ _ (mul_ne_zero hc0 hd0)]

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

Goal state before:
pp: case inr
R : Type u
inst✝ : Semiring R
I : Ideal R
n : ℕ
h : n = 0
⊢ I ^ n = ⊤

Tactic:
rw [h, Submodule.pow_zero, one_eq_top]

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

Goal state before:
pp: z : ℤ
h : z ≤ 0
⊢ normalize z = -z

Tactic:
obtain rfl | h := h.eq_or_lt

Goal state after:
case inl
h : 0 ≤ 0
⊢ normalize 0 = -0

case inr
z : ℤ
h✝ : z ≤ 0
h : z < 0
⊢ normalize z = -z
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 : { g // ker f ≤ ker g }
x✝ : A
⊢ ↑((fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g)) x✝ = ↑g x✝

Tactic:
simp only [comp_apply, liftOfRightInverseAux_comp_apply]

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Defs

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a✝ a i : α
ha0 : a ≠ 0
hi : Irreducible i
ih : a ≠ 0 → ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod ~ᵤ a
x✝ : i * a ≠ 0
s : Multiset α
hs : (∀ b ∈ s, Irreducible b) ∧ s.prod ~ᵤ a
⊢ (i ::ₘ s).prod ~ᵤ i * a

Tactic:
by
      rw [s.prod_cons i]
      exact hs.2.mul_left i

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

Goal state before:
pp: case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
⊢ gcd a b ∣ c

Tactic:
rcases gcd_dvd_left a b with ⟨f, hf⟩

Goal state after:
case hab
α : Type u_1
inst✝¹ : CommRing α
inst✝ : NormalizedGCDMonoid α
a b c d : α
hd : b - c = a * d
e : α
he : b = gcd a b * e
f : α
hf : a = gcd a b * f
⊢ gcd a b ∣ c
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case mk.mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
b✝ : Associates α
b : α
⊢ Quotient.map₂ gcd ⋯ (Quot.mk (⇑(Associated.setoid α)) a) (Quot.mk (⇑(Associated.setoid α)) b) ∣
    Quot.mk (⇑(Associated.setoid α)) a

Tactic:
exact mk_le_mk_of_dvd (gcd_dvd_left _ _)

Goal state after:
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
x : M
h : Bijective ⇑(LinearMap.toSpanSingleton R M x)
⊢ finrank R M = 1

Tactic:
by
  rw [← (LinearEquiv.ofBijective _ h).finrank_eq, finrank_self]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
β : Type u_8
inst✝⁵ : DecidableEq m
inst✝⁴ : DecidableEq n
inst✝³ : Finite m
inst✝² : Finite n
inst✝¹ : AddCommMonoid α
inst✝ : AddCommMonoid β
f g : Matrix m n α →+ β
h : ∀ (i : m) (j : n), f.comp (singleAddMonoidHom i j) = g.comp (singleAddMonoidHom i j)
⊢ f = g

Tactic:
cases nonempty_fintype m
  cases nonempty_fintype n
  ext x
  rw [matrix_eq_sum_single x]
  simp_rw [map_sum]
  congr! 2
  exact DFunLike.congr_fun (h _ _) _

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A : Matrix m n α
x✝ : n
⊢ (1 ᵥ* A) x✝ = (∑ i, A i) x✝

Tactic:
simp [vecMul, dotProduct]

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

Goal state before:
pp: m : Type u_2
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
x : α
v : m → α
x✝ : m
⊢ ((diagonal fun x_1 ↦ x) *ᵥ v) x✝ = (x • v) x✝

Tactic:
simp [mulVec_diagonal]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop))

Tactic:
by ext; simp [mul_apply]

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

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) =
    { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
      { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝

Tactic:
by ext; simp [mul_apply]

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Module.rank R M = #M

Tactic:
have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le

Goal state after:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Free R M
inst✝¹ : StrongRankCondition R
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
⊢ Module.rank R M = #M
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
let s : TwoSidedIdeal R := .mk'
      {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
      ⟨0, ⟨zero_mem _, ⟨0, ⟨zero_mem _, zero_add _⟩⟩⟩⟩
      (by rintro _ _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩ ⟨a, ⟨ha, ⟨b, ⟨hb, rfl⟩⟩⟩⟩;
          exact ⟨x + a, ⟨add_mem _ hx ha, ⟨y + b, ⟨add_mem _ hy hb, by abel⟩⟩⟩⟩)
      (by rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨-x, ⟨neg_mem _ hx, ⟨-y, ⟨neg_mem _ hy, by abel⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩)
      (by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_right _ _ _ hx, ⟨_, ⟨mul_mem_right _ _ _ hy, add_mul _ _ _ |>.symm⟩⟩⟩⟩)

Goal state after:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i ↦ A ↑i
⊢ ⨆ i, Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i) = ⊤

Tactic:
simp [iSup_subtype]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
m : M
n : N
a✝ : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) (m ⊗ₜ[R] n)) a✝ = (Finsupp.mapRange (fun x ↦ x • m) ⋯ (𝒞.repr n)) a✝

Tactic:
simp [equivFinsuppOfBasisRight]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
a✝ : κ
x✝ : M
⊢ (↑(equivFinsuppOfBasisRight 𝒞).symm ∘ₗ Finsupp.lsingle a✝) x✝ =
    (((Finsupp.lsum R) fun i ↦ (mk R M N).flip (𝒞 i)) ∘ₗ Finsupp.lsingle a✝) x✝

Tactic:
simp [equivFinsuppOfBasisRight]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
𝒞 : Basis κ R N
x : M ⊗[R] N
⊢ ∃ b, (b.sum fun i m ↦ m ⊗ₜ[R] 𝒞 i) = x

Tactic:
classical simpa using (TensorProduct.equivFinsuppOfBasisRight 𝒞).symm.surjective x

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → MulOneClass (R i)
inst✝ : (i : ι) → StarMul (R i)
i : ι
r : R i
⊢ star (mulSingle i r) = mulSingle i (star r)

Tactic:
by
  ext; exact apply_mulSingle (fun _ ↦ star) (fun _ ↦ star_one _) ..

Goal state after:
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ a • ↑x ∈ selfAdjoint R

Tactic:
Rat.smul_def

Goal state after:
R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ ↑a * ↑x ∈ selfAdjoint R
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : l
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inl val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inl val✝)

Tactic:
simp [vecMul, dotProduct]

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

Goal state before:
pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝² : Fintype n
inst✝¹ : Fintype o
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
x : n ⊕ o → α
val✝ : m
⊢ (x ᵥ* fromBlocks A B C D) (Sum.inr val✝) =
    Sum.elim (x ∘ Sum.inl ᵥ* A + x ∘ Sum.inr ᵥ* C) (x ∘ Sum.inl ᵥ* B + x ∘ Sum.inr ᵥ* D) (Sum.inr val✝)

Tactic:
simp [vecMul, dotProduct]

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

Goal state before:
pp: α : Type u
m : ℕ
ι : Type u_1
x : α
u : Fin m → α
⊢ replicateCol ι (vecCons x u) = of (vecCons (fun x_1 ↦ x) (replicateCol ι u))

Tactic:
by
  ext i j
  refine Fin.cases ?_ ?_ i <;> simp

Goal state after: