mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Coprime.Lemmas

Goal state before:
pp: case neg
R : Type u
I : Type v
inst✝¹ : CommSemiring R
s : I → R
t✝ : Finset I
inst✝ : DecidableEq I
a : I
t : Finset I
hat : a ∉ t
h : t.Nonempty
ih : (∃ μ, ∑ i ∈ t, μ i * ∏ j ∈ t \ {i}, s j = 1) ↔ Pairwise (IsCoprime on fun i ↦ s ↑i)
mem : ∀ x ∈ t, a ∈ insert a t \ {x}
μ : I → R
hμ✝ : μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x + ∑ x ∈ t, μ x * ∏ j ∈ insert a t \ {x}, s j = 1
hμ :
  ∑ x ∈ t,
      (Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x +
        μ x * ∏ j ∈ insert a t \ {x}, s j) =
    1
x : I
hx✝ : x ∈ t
hx : ¬x = Exists.choose h
⊢ Pi.single (Exists.choose h) (μ a * s (Exists.choose h) * ∏ x ∈ t \ {Exists.choose h}, s x) x =
    Pi.single (Exists.choose h) (μ a * s (Exists.choose h)) x * ∏ j ∈ t \ {x}, s j

Tactic:
· rw [Pi.single_eq_of_ne hx, Pi.single_eq_of_ne hx, zero_mul]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    ((Ideal.span {generator (Ideal.map (RingHom.fst R S) I)}).prod
      (Ideal.span {generator (Ideal.map (RingHom.snd R S) I)}))

Tactic:
← Ideal.span_prod (iff_of_true (by simp) (by simp)),

Goal state after:
R : Type u
S : Type v
inst✝³ : Semiring R
inst✝² : Semiring S
I✝ : Ideal R
J : Ideal S
inst✝¹ : IsPrincipalIdealRing R
inst✝ : IsPrincipalIdealRing S
I : Ideal (R × S)
⊢ Submodule.IsPrincipal
    (Ideal.span ({generator (Ideal.map (RingHom.fst R S) I)} ×ˢ {generator (Ideal.map (RingHom.snd R S) I)}))
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✝ J : Ideal R
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R
inst✝² : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst✝¹ : RingHomSurjective f
I : Ideal R
inst✝ : I.IsTwoSided
a : R
ha : a ∈ ↑I
b : R
⊢ f.toSemilinearMap a * f b ∈ Submodule.map f.toSemilinearMap I

Tactic:
rw [RingHom.coe_toSemilinearMap, ← map_mul]

Goal state after:
R : Type u
S : Type v
F : Type u_1
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : FunLike F R S
f✝ : F
I✝ J : Ideal R
K L : Ideal S
G : Type u_2
inst✝³ : FunLike G S R
inst✝² : RingHomClass F R S
ι : Sort u_3
f : R →+* S
inst✝¹ : RingHomSurjective f
I : Ideal R
inst✝ : I.IsTwoSided
a : R
ha : a ∈ ↑I
b : R
⊢ f (a * b) ∈ Submodule.map f.toSemilinearMap I
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
inst✝ : RingHomClass F R S
hf : Function.Bijective ⇑f
I : Ideal R
⊢ map f I = ⊤ ↔ I = ⊤

Tactic:
by
  rw [eq_top_iff, ← comap_le_iff_le_map f hf, comap_top, top_le_iff]

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

Goal state before:
pp: case inr
R : Type u_1
inst✝ : EuclideanDomain R
b : R
n : ℕ
c : R
hb : b ≠ 0
⊢ (b * c / b) ^ n = (b * c) ^ n / b ^ n

Tactic:
· simp [hb, mul_pow]

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:
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
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Semiring S
inst✝ : Semiring T
g : T →+* R
f : R →+* S
hf : Function.Injective ⇑f
⊢ ker (f.comp g) = ker g

Tactic:
by
  rw [← RingHom.comap_ker, (injective_iff_ker_eq_bot f).mp hf, RingHom.ker]

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

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x : R
⊢ lcm x 0 = 0

Tactic:
rw [lcm, mul_zero, zero_div]

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

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.27

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

Tactic:
gcd_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd ?m.36 = GCDMonoid.gcd s₁.gcd s₂.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁.ndunion s₂ ↔ a ∈ ?m.36
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ (dedup ?m.27).gcd = GCDMonoid.gcd s₁.gcd s₂.gcd

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.27

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

Tactic:
gcd_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ gcd ?m.36 = GCDMonoid.gcd s₁.gcd s₂.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
s₁ s₂ : Multiset α
⊢ ∀ (a : α), a ∈ s₁ ∪ s₂ ↔ a ∈ ?m.36
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ (dedup ?m.24).gcd = GCDMonoid.gcd a s.gcd

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.24

pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

Tactic:
gcd_dedup,

Goal state after:
α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ gcd ?m.33 = GCDMonoid.gcd a s.gcd

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ Multiset α

α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : NormalizedGCDMonoid α
inst✝ : DecidableEq α
a : α
s : Multiset α
⊢ ∀ (a_1 : α), a_1 ∈ ndinsert a s ↔ a_1 ∈ ?m.33
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case hI
R : Type u
inst✝¹ : CommSemiring R
ι : Type u_2
inst✝ : Fintype ι
I : ι → R
hI : ∀ (i j : ι), i ≠ j → IsCoprime (I i) (I j)
⊢ (↑Finset.univ).Pairwise (Function.onFun IsCoprime I)

Tactic:
rwa [Finset.coe_univ, Set.pairwise_univ]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
⊢ x ∈ map f J

Tactic:
rcases Ideal.exists_of_comap_eq_ker_sup _ surj eq hx with ⟨y, mem, hy⟩

Goal state after:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
surj : Function.Surjective ⇑f
I : Ideal B
J : Ideal A
eq : comap f I = RingHom.ker f ⊔ J
x : B
hx : x ∈ I
y : A
mem : y ∈ J
hy : f y = x
⊢ x ∈ map f J
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ IsUnit a ↔ (↑a)⁻¹ ∈ S

Tactic:
isUnit_iff_and,

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
ha : ↑a ≠ 0
⊢ ↑a ≠ 0 ∧ (↑a)⁻¹ ∈ S ↔ (↑a)⁻¹ ∈ S
Module: Mathlib.RingTheory.Ideal.Nonunits

Goal state before:
pp: α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬IsUnit a ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S

Tactic:
isUnit_iff_and,

Goal state after:
α : Type u_2
C : Type u_4
inst✝² : SetLike C α
inst✝¹ : GroupWithZero α
inst✝ : SubmonoidClass C α
S : C
a : ↥S
⊢ ¬(↑a ≠ 0 ∧ (↑a)⁻¹ ∈ S) ↔ ↑a = 0 ∨ (↑a)⁻¹ ∉ S
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
hI : I.IsRadical
hJ : J.IsRadical
⊢ (I ⊓ J).IsRadical

Tactic:
rw [IsRadical, radical_inf]; exact inf_le_inf hI hJ

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

Goal state before:
pp: case a
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
k m n m' n' : α
hm' : m' ∣ m
hn' : n' ∣ n
h : gcd k (m * n) = m' * n'
hm'n' : m' * n' ∣ k
⊢ m' ∣ gcd k m

Tactic:
have hm'k : m' ∣ k := (dvd_mul_right m' n').trans hm'n'
    exact dvd_gcd hm'k hm'

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ gcd d₁ b ^ k ∣ 1

Tactic:
apply IsUnit.dvd

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a b c d₁ d₂ : α
ha : a ≠ 0
hab : IsUnit (gcd a b)
k : ℕ
h : a * b = c ^ k
hc : c = d₁ * d₂
hd₁ : d₁ ∣ a
⊢ IsUnit (gcd d₁ b ^ k)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : a - b ∈ Ideal.pi fun x ↦ I
h : ι'
⊢ (e a - e b) h ∈ (fun x ↦ I) h

Tactic:
rw [← map_sub]

Goal state after:
R : Type u
inst✝¹ : CommRing R
I✝ : Ideal R
ι : Type v
inst✝ : Fintype ι
ι' : Type w
I : Ideal R
e : (ι → R) →ₗ[R] ι' → R
x : (ι → R) ⧸ Ideal.pi fun x ↦ I
a b : ι → R
hab : a - b ∈ Ideal.pi fun x ↦ I
h : ι'
⊢ e (a - b) h ∈ (fun x ↦ I) h
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos.inr.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : f a ≤ f i
h' : ↑I ⊆ ↑(f i) ∪ ↑(f b) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f b
⊢ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inl ih

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

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝ : Fintype ι
this : Finite ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
cases nonempty_fintype ι'

Goal state after:
case inl.intro
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this✝ : Nontrivial R
val✝¹ : Fintype ι
this : Finite ι'
val✝ : Fintype ι'
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: case pos.inl
ι : Type u_1
R : Type u
inst✝ : CommRing R
f : ι → Ideal R
I : Ideal R
n : ℕ
a b i : ι
t : Finset ι
hit : i ∉ t
hn : t.card = n
h : ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i_1 ∈ ↑(insert i t), ↑(f i_1)
hp : (f i).IsPrime ∧ ∀ x ∈ t, (f x).IsPrime
Ht : ¬∃ j ∈ t, f j ≤ f i
Ha : ¬f a ≤ f i
Hb : f b ≤ f i
h' : ↑I ⊆ ↑(f a) ∪ ↑(f i) ∪ ⋃ j ∈ ↑t, ↑(f j)
ih : I ≤ f a
⊢ I ≤ f a ∨ I ≤ f b ∨ ∃ i_1 ∈ insert i t, I ≤ f i_1

Tactic:
exact Or.inl ih

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ M.map id = M

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
⊢ (M.map f).map g = M.map (g ∘ f)

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
⊢ Mᵀᵀ = M

Tactic:
by
  ext
  rfl

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

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
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n✝
inst✝ : AddGroupWithOne α
n : ℕ
⊢ (diagonal fun x ↦ ↑↑n) = diagonal fun x ↦ ↑n

Tactic:
Int.cast_natCast

Goal state after:
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
α : Type v
β : Type w
γ : Type u_9
inst✝¹ : DecidableEq n✝
inst✝ : AddGroupWithOne α
n : ℕ
⊢ (diagonal fun x ↦ ↑n) = diagonal fun x ↦ ↑n
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✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ Subsingleton M ↔ ¬0 < finrank R M

Tactic:
simp [Module.finrank_eq_zero_iff_of_free]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝⁵ : AddCommMonoid α
inst✝⁴ : Mul α
inst✝³ : Fintype n
inst✝² : Monoid R
inst✝¹ : DistribMulAction R α
inst✝ : IsScalarTower R α α
a : R
M : Matrix m n α
N : Matrix n l α
⊢ a • M * N = a • (M * N)

Tactic:
by
  ext
  apply smul_dotProduct a

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

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
x : R
hx : x ∉ I
n : ℕ
⊢ ∃ y, ∃ i ∈ I ^ n, y * x + i = 1

Tactic:
obtain ⟨y, i, hmem, hi⟩ := Ideal.IsMaximal.exists_inv ‹_› hx
  obtain ⟨y, hy⟩ : ∃ y : R, y * x + i ^ n = 1 := by
    induction n with
    | zero => exact ⟨0, by simp⟩
    | succ n ih =>
      obtain ⟨z, hz⟩ := ih
      refine ⟨z * i + y, ?_⟩
      trans z * i * x + i * i ^ n + y * x
      · ring
      · rw [mul_comm z i, mul_assoc, ← mul_add, hz, add_comm]
        simpa
  exact ⟨y, i ^ n, Ideal.pow_mem_pow hmem n, hy⟩

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

Goal state before:
pp: case inr.inl.inr
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
M : Matrix n n α
hM : Pairwise fun i j ↦ Commute (single i j 1) M
h✝ : Nonempty n
i j : n
hij : i ≠ j
⊢ M i i = M j j

Tactic:
· exact diag_eq_of_commute_single (hM hij)

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

Goal state before:
pp: m : Type u_2
α : Type u_11
inst✝ : AddZeroClass α
i : m
⊢ (Pi.evalAddMonoidHom (fun i ↦ α) i).comp (diagAddMonoidHom m α) = entryAddMonoidHom α i i

Tactic:
simp [AddMonoidHom.ext_iff]

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
hx : x ∈ I
hy : y ∈ I
⊢ x + y ∈ I

Tactic:
by simpa using! I.ringCon.add hx hy

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R}, y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x * y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
by rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩
          exact ⟨_, ⟨mul_mem_left _ _ _ hx, ⟨_, ⟨mul_mem_left _ _ _ hy, mul_add _ _ _ |>.symm⟩⟩⟩⟩

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: 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} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
by
      intro h; convert! this h; rw [rel_iff, sub_zero, mem_mk']; rfl

Goal state after:
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
⊢ 0 = 1

Tactic:
have mem : 1 ∈ TwoSidedIdeal.ker f := h.symm ▸ TwoSidedIdeal.mem_top _

Goal state after:
R : Type u_2
S : Type u_3
inst✝² : NonAssocRing R
inst✝¹ : IsSimpleRing R
inst✝ : NonAssocSemiring S
f : R →+* S
h : TwoSidedIdeal.ker f = ⊤
mem : 1 ∈ TwoSidedIdeal.ker f
⊢ 0 = 1
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ (inl R P Q).coprod (f ∘ₗ g₂) = LinearMap.id

Tactic:
hg₂,

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ (inl R P Q).coprod (inr R P Q) = LinearMap.id
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: case single
R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
n : N
a✝ : ι
b✝ : M
⊢ (finsuppLeft R S M N ι) (Finsupp.single a✝ b✝ ⊗ₜ[R] n) =
    (Finsupp.single a✝ b✝).sum fun i m ↦ Finsupp.single i (m ⊗ₜ[R] n)

Tactic:
simp [finsuppLeft]

Goal state after:
Module: Mathlib.LinearAlgebra.DirectSum.Finsupp

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
M : Type u_3
inst✝⁶ : AddCommMonoid M
inst✝⁵ : Module R M
inst✝⁴ : Module S M
inst✝³ : IsScalarTower R S M
N : Type u_4
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
ι : Type u_5
inst✝ : DecidableEq ι
i : ι
m : M
n : N
⊢ (finsuppLeft R S M N ι).symm (Finsupp.single i (m ⊗ₜ[R] n)) = Finsupp.single i m ⊗ₜ[R] n

Tactic:
simp [finsuppLeft]

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

Goal state before:
pp: case inr.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
l' : L
hk : k ≠ k'
⊢ single k l r k' l' = single (i, k) (j, l) r (i, k') (j, l')

Tactic:
single_apply_of_row_ne hk,

Goal state after:
case inr.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
l' : L
hk : k ≠ k'
⊢ 0 = single (i, k) (j, l) r (i, k') (j, l')
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star (f (r • x)) = f (Star.star r • Star.star x)

Tactic:
smul,

Goal state after:
R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star (r • f x) = f (Star.star r • Star.star x)
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star r • Star.star (f x) = f (Star.star r • Star.star x)

Tactic:
smul,

Goal state after:
R : Type u
S : Type v
f : R → S
𝕜 : Type u_1
inst✝⁵ : Star 𝕜
inst✝⁴ : SMul 𝕜 R
inst✝³ : Star R
inst✝² : SMul 𝕜 S
inst✝¹ : Star S
inst✝ : StarModule 𝕜 S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
smul : ∀ (r : 𝕜) (x : R), f (r • x) = r • f x
r : 𝕜
x : R
⊢ Star.star r • Star.star (f x) = Star.star r • f (Star.star x)
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
inst✝¹ : Group R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
by
  simp [isSelfAdjoint_iff]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : GroupWithZero R
inst✝ : StarMul R
x : R
⊢ IsSelfAdjoint x⁻¹ ↔ IsSelfAdjoint x

Tactic:
by
  simp [isSelfAdjoint_iff]

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

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Star A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : Star B
f : A →⋆ₙ+* B
h₁ : ∀ (x y : A), f (x * y) = f x * f y
h₂ : { toFun := ⇑f, map_mul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_mul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_mul' := h₁ }.toFun x + { toFun := ⇑f, map_mul' := h₁ }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (star a) =
      star ({ toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun a)
⊢ { toFun := ⇑f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ } = f

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
⊢ ∀ (p : Submodule R M), range (w • v) ⊆ ↑p → j ∈ p

Tactic:
refine fun p hp => hj p fun u hu => ?_

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_4
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
G : Type u_5
inst✝³ : Group G
inst✝² : SMul G R
inst✝¹ : MulAction G M
inst✝ : IsScalarTower G R M
v : ι → M
hv : span R (range v) = ⊤
w : ι → G
j : M
hj : ∀ (p : Submodule R M), range v ⊆ ↑p → j ∈ p
p : Submodule R M
hp : range (w • v) ⊆ ↑p
u : M
hu : u ∈ range v
⊢ u ∈ ↑p
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ replicateCol ι (v + w) = replicateCol ι v + replicateCol ι w

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
R : Type u_5
α : Type v
ι : Type u_6
inst✝ : SMul R α
x : R
v : m → α
⊢ replicateCol ι (x • v) = x • replicateCol ι v

Tactic:
by
  ext
  rfl

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

Goal state before:
pp: m : Type u_2
α : Type v
ι : Type u_6
inst✝ : Add α
v w : m → α
⊢ replicateRow ι (v + w) = replicateRow ι v + replicateRow ι w

Tactic:
by
  ext
  rfl

Goal state after: