mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.GCDMonoid.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
a : α
s : Multiset α
⊢ Associated (map (fun x ↦ a * x) s).gcd (a * s.gcd)

Tactic:
refine s.induction_on ?_ fun b s ih ↦ ?_
  · simp_rw [map_zero, gcd_zero, mul_zero, Associated.of_eq]
  · simp_rw [map_cons, gcd_cons]
    exact .trans (.gcd .rfl ih) (gcd_mul_left' ..)

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} ↔ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ {J | map f I ≤ J ∧ J.IsPrime} → j ∈ map f '' {J | I ≤ J ∧ J.IsPrime}

case mpr
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Function.Surjective ⇑f
I : Ideal R
h : RingHom.ker f ≤ I
this : ∀ J ∈ {J | I ≤ J ∧ J.IsPrime}, RingHom.ker f ≤ J
j : Ideal S
⊢ j ∈ map f '' {J | I ≤ J ∧ J.IsPrime} → j ∈ {J | map f I ≤ J ∧ J.IsPrime}
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ s.lcm f ∣ a ↔ ∀ b ∈ s, f b ∣ a

Tactic:
by
  apply Iff.trans Multiset.lcm_dvd
  simp only [Multiset.mem_map, and_imp, exists_imp]
  exact ⟨fun k b hb ↦ k _ _ hb rfl, fun k a' b hb h ↦ h ▸ k _ hb⟩

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 : { g // ker f ≤ ker g }
⊢ (fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g) = g

Tactic:
ext

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 : { g // ker f ≤ ker g }
x✝ : A
⊢ ↑((fun φ ↦ ⟨φ.comp f, ⋯⟩) ((fun g ↦ f.liftOfRightInverseAux f_inv hf ↑g ⋯) g)) x✝ = ↑g x✝
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) ↔ IsCoprime x y

Tactic:
constructor

Goal state after:
case mp
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) → IsCoprime x y

case mpr
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
I : Ideal R
x y : ↥I
⊢ (idealMap S I) (x * y) = (idealMap S I) x * (idealMap S I) y

Tactic:
ext

Goal state after:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
inst✝ : Algebra R S
I : Ideal R
x y : ↥I
⊢ ↑((idealMap S I) (x * y)) = ↑((idealMap S I) x * (idealMap S I) y)
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
⊢ RingHom.ker (algebraMap R A) = ⊥

Tactic:
ext

Goal state after:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : FaithfulSMul R A
x✝ : R
⊢ x✝ ∈ RingHom.ker (algebraMap R A) ↔ x✝ ∈ ⊥
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) ↔ I ⊔ J = ⊤

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ (∃ a b, a * I + b * J = 1) → I ⊔ J = ⊤

case mpr
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ I ⊔ J = ⊤ → ∃ a b, a * I + b * J = 1
Module: Mathlib.Algebra.GCDMonoid.Finset

Goal state before:
pp: case neg
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
⊢ ∃ g, (∀ b ∈ s, f b = s.gcd f * g b) ∧ s.gcd g = 1

Tactic:
refine ⟨fun b ↦ if hb : b ∈ s then g' hb else 0, fun b hb ↦ ?_,
          extract_gcd' f _ h fun b hb ↦ ?_⟩

Goal state after:
case neg.refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * (fun b ↦ if hb : b ∈ s then g' hb else 0) b

case neg.refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
hs : s.Nonempty
h : ∃ x ∈ s, f x ≠ 0
g' : {b : β} → b ∈ s → α
hg : ∀ {b : β} (hb : b ∈ s), f b = s.gcd f * g' hb
b : β
hb : b ∈ s
⊢ f b = s.gcd f * if hb : b ∈ s then g' hb else 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) ↔ IsCoprime x y

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ (∃ a b, y ∣ b ∧ a * x + b = 1) → IsCoprime x y

case mpr
R : Type u
inst✝ : CommSemiring R
x y : R
⊢ IsCoprime x y → ∃ a b, y ∣ b ∧ a * x + b = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
⊢ {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
x✝ : Ideal α
⊢ x✝ ∈ {I | Submodule.IsPrincipal I} ↔ x✝ ∈ (fun a ↦ span {a}) '' Set.univ
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
⊢ (Function.onFun (fun x1 x2 ↦ x1 > x2) fun a ↦ span {a}) = DvdNotUnit

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : CommSemiring α
inst✝¹ : WfDvdMonoid α
inst✝ : IsDomain α
this : {I | Submodule.IsPrincipal I} = (fun a ↦ span {a}) '' Set.univ
x✝¹ x✝ : α
⊢ Function.onFun (fun x1 x2 ↦ x1 > x2) (fun a ↦ span {a}) x✝¹ x✝ ↔ DvdNotUnit x✝¹ x✝
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ WfDvdMonoid α

Tactic:
constructor

Goal state after:
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ WellFounded DvdNotUnit
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Ideal

Goal state before:
pp: α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
⊢ DvdNotUnit = InvImage (fun x1 x2 ↦ x1 > x2) fun a ↦ ⟨Ideal.span {a}, ⋯⟩

Tactic:
ext

Goal state after:
α : Type u_1
inst✝¹ : CommSemiring α
inst✝ : IsDomain α
h : {I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 ↦ x1 > x2
this : WellFounded fun x1 x2 ↦ x1 > x2
x✝¹ x✝ : α
⊢ DvdNotUnit x✝¹ x✝ ↔ InvImage (fun x1 x2 ↦ x1 > x2) (fun a ↦ ⟨Ideal.span {a}, ⋯⟩) x✝¹ x✝
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective ⇑i
⊢ (LinearMap.funLeft R R Fin.castSucc) 0 = (LinearMap.funLeft R R Fin.castSucc) (update 0 (Fin.last n) 1)

Tactic:
ext

Goal state after:
R : Type u
inst✝² : Semiring R
inst✝¹ : Nontrivial R
inst✝ : OrzechProperty R
n : ℕ
i : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hi : Injective ⇑i
x✝ : Fin n
⊢ (LinearMap.funLeft R R Fin.castSucc) 0 x✝ = (LinearMap.funLeft R R Fin.castSucc) (update 0 (Fin.last n) 1) x✝
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) ↔ ∃ n f, Injective ⇑f

Tactic:
constructor

Goal state after:
case mp
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f

case mpr
R : Type u
inst✝ : Semiring R
⊢ (∃ n f, Injective ⇑f) → ∃ n f, Injective ⇑f
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝² : CommMonoidWithZero α
inst✝¹ : IsCancelMulZero α
inst✝ : DecidableEq α
lcm : α → α → α
dvd_lcm_left : ∀ (a b : α), a ∣ lcm a b
dvd_lcm_right : ∀ (a b : α), b ∣ lcm a b
lcm_dvd : ∀ {a b c : α}, c ∣ a → b ∣ a → lcm c b ∣ a
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
a b : α
⊢ (if a = 0 then b else if b = 0 then a else Classical.choose ⋯) ∣ b

Tactic:
split_ifs with h h_1
      · exact dvd_rfl
      · rw [h_1]
        apply dvd_zero
      have h0 : lcm a b ≠ 0 := by
        intro con
        have h := lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
        rw [con, zero_dvd_iff, mul_eq_zero] at h
        cases h
        · exact absurd ‹a = 0› h
        · exact absurd ‹b = 0› h_1
      rw [← mul_dvd_mul_iff_left h0, ← Classical.choose_spec (exists_gcd a b),
        mul_dvd_mul_iff_right h_1]
      apply dvd_lcm_left

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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ M.map id i✝ j✝ = M i✝ j✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
β : Type u_10
γ : Type u_11
f : α → β
g : β → γ
i✝ : m
j✝ : n
⊢ (M.map f).map g i✝ j✝ = M.map (g ∘ f) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
⊢ map 0 f = 0

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
β : Type w
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
i✝ : m
j✝ : n
⊢ map 0 f i✝ j✝ = 0 i✝ j✝
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:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i✝ : m
j✝ : n
⊢ Mᵀᵀ i✝ j✝ = M i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
⊢ (M + N)ᵀ = Mᵀ + Nᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Add α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M + N)ᵀ i✝ j✝ = (Mᵀ + Nᵀ) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
⊢ (M - N)ᵀ = Mᵀ - Nᵀ

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M - N)ᵀ i✝ j✝ = (Mᵀ - Nᵀ) i✝ j✝
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
S : Set α
⊢ S.matrix = ⇑of.symm ⁻¹' univ.pi fun x ↦ univ.pi fun x ↦ S

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
S : Set α
x✝ : Matrix m n α
⊢ x✝ ∈ S.matrix ↔ x✝ ∈ ⇑of.symm ⁻¹' univ.pi fun x ↦ univ.pi fun x ↦ S
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
⊢ (diagonal fun x ↦ 0) = 0

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
i✝ j✝ : n
⊢ diagonal (fun x ↦ 0) i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
⊢ (diagonal d).map f = diagonal fun m ↦ f (d m)

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
β : Type w
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : Zero β
f : α → β
h : f 0 = 0
d : n → α
i✝ j✝ : n
⊢ (diagonal d).map f i✝ j✝ = diagonal (fun m ↦ f (d m)) i✝ j✝
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i : n
⊢ (diagonal d).col i = Pi.single i (d i)

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
i x✝ : n
⊢ (diagonal d).col i x✝ = Pi.single i (d i) x✝
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
j : n
⊢ (diagonal d).row j = Pi.single j (d j)

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
d : n → α
j x✝ : n
⊢ (diagonal d).row j x✝ = Pi.single j (d j) x✝
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
⊢ map 1 f = 1

Tactic:
ext

Goal state after:
n : Type u_3
α : Type v
β : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Zero β
inst✝ : One β
f : α → β
h₀ : f 0 = 0
h₁ : f 1 = 1
i✝ j✝ : n
⊢ map 1 f i✝ j✝ = 1 i✝ j✝
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
⊢ x ∈ span K s ↔ ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x

Tactic:
constructor

Goal state after:
case mp
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
⊢ x ∈ span K s → ∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x

case mpr
K : Type u_2
M : Type u_3
inst✝³ : DivisionRing K
inst✝² : AddCommGroup M
inst✝¹ : Module K M
s : Set M
x : M
inst✝ : Module.Finite K ↥(span K s)
⊢ (∃ c, c.support.card ≤ finrank K ↥(span K s) ∧ ↑c.support ⊆ s ∧ (c.sum fun mi r ↦ r • mi) = x) → x ∈ span K s
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
⊢ (r • of fun i' j' ↦ if i = i' ∧ j = j' then a else 0) = of fun i' j' ↦ if i = i' ∧ j = j' then r • a else 0

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_5
α : Type u_7
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
r : R
i : m
j : n
a : α
i✝ : m
j✝ : n
⊢ (r • of fun i' j' ↦ if i = i' ∧ j = j' then a else 0) i✝ j✝ =
    of (fun i' j' ↦ if i = i' ∧ j = j' then r • a else 0) i✝ j✝
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
⊢ (of fun i' j' ↦ if i = i' ∧ j = j' then 0 else 0) = 0

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
i✝ : m
j✝ : n
⊢ of (fun i' j' ↦ if i = i' ∧ j = j' then 0 else 0) i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
⊢ single i j (a + b) = single i j a + single i j b

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : AddZeroClass α
i : m
j : n
a b : α
i✝ : m
j✝ : n
⊢ single i j (a + b) i✝ j✝ = (single i j a + single i j b) i✝ j✝
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:
ext

Goal state after:
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 α
i✝ : m
j✝ : l
⊢ (a • M * N) i✝ j✝ = (a • (M * N)) i✝ j✝
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✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
⊢ M * a • N = a • (M * N)

Tactic:
ext

Goal state after:
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✝ : SMulCommClass R α α
M : Matrix m n α
a : R
N : Matrix n l α
i✝ : m
j✝ : l
⊢ (M * a • N) i✝ j✝ = (a • (M * N)) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
⊢ M * 0 = 0

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
M : Matrix m n α
i✝ : m
j✝ : o
⊢ (M * 0) i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
i✝ : l
j✝ : n
⊢ (0 * M) i✝ j✝ = 0 i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
j✝ : o
⊢ (L * (M + N)) i✝ j✝ = (L * M + L * N) i✝ j✝
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 ∈ s, ↑(f i) = ⋃ i ∈ t, ↑(f i)

Tactic:
ext

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
x✝ : R
⊢ x✝ ∈ ⋃ i ∈ s, ↑(f i) ↔ x✝ ∈ ⋃ i ∈ t, ↑(f i)
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
⊢ (L + M) * N = L * N + M * N

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
L M : Matrix l m α
N : Matrix m n α
i✝ : l
j✝ : n
⊢ ((L + M) * N) i✝ j✝ = (L * N + M * N) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
⊢ a • M = (diagonal fun x ↦ a) * M

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (a • M) i✝ j✝ = ((diagonal fun x ↦ a) * M) i✝ j✝
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
i j : n
b : α
w : n → α
⊢ single i j b *ᵥ w = (b * w j) • Pi.single i 1

Tactic:
ext

Goal state after:
n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : NonAssocSemiring α
i j : n
b : α
w : n → α
x✝ : n
⊢ (single i j b *ᵥ w) x✝ = ((b * w j) • Pi.single i 1) x✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
⊢ MulOpposite.op a • M = M * diagonal fun x ↦ a

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
a : α
i✝ : m
j✝ : n
⊢ (MulOpposite.op a • M) i✝ j✝ = (M * diagonal fun x ↦ a) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝² : NonUnitalNonAssocSemiring β
F : Type u_10
inst✝¹ : FunLike F α β
inst✝ : NonUnitalRingHomClass F α β
f : F
⊢ (L * M).map ⇑f = L.map ⇑f * M.map ⇑f

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
β : Type w
inst✝⁴ : NonUnitalNonAssocSemiring α
inst✝³ : Fintype n
L : Matrix m n α
M : Matrix n o α
inst✝² : NonUnitalNonAssocSemiring β
F : Type u_10
inst✝¹ : FunLike F α β
inst✝ : NonUnitalRingHomClass F α β
f : F
i✝ : m
j✝ : o
⊢ (L * M).map (⇑f) i✝ j✝ = (L.map ⇑f * M.map ⇑f) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

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

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (1 * M) i✝ j✝ = M i✝ j✝
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

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonAssocSemiring α
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix m n α
i✝ : m
j✝ : n
⊢ (M * 1) i✝ j✝ = M i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
⊢ L * M * N = L * (M * N)

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
L : Matrix l m α
M : Matrix m n α
N : Matrix n o α
i✝ : l
j✝ : o
⊢ (L * M * N) i✝ j✝ = (L * (M * N)) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ -M * N = -(M * N)

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (-M * N) i✝ j✝ = (-(M * N)) i✝ j✝
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
⊢ M * -N = -(M * N)

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
M : Matrix m n α
N : Matrix n o α
i✝ : m
j✝ : o
⊢ (M * -N) i✝ j✝ = (-(M * N)) i✝ j✝