mathlib-initiative/mathlib-tactics huggingface dataset:
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.map (RingHom.fst R S) I).prod (Ideal.map (RingHom.snd R S) I))

Tactic:
← span_singleton_generator (I.map _),

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.prod (R ∙ generator (Ideal.map (RingHom.fst R S) I)) (Ideal.map (RingHom.snd R S) I))
Module: Mathlib.RingTheory.Noetherian.Basic

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {α : Type u_2} [Fintype α],
    (∀ {R : α → Type u_1} [inst : (i : α) → Semiring (R i)] [∀ (i : α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : α) → R i)) →
      ∀ {R : Option α → Type u_1} [inst : (i : Option α) → Semiring (R i)] [∀ (i : Option α), IsNoetherianRing (R i)],
        IsNoetherianRing ((i : Option α) → R i)

Tactic:
exact fun ih ↦ isNoetherianRing_of_ringEquiv _ (.symm .piOptionEquivProd)

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

Goal state before:
pp: ι : Type u_2
inst✝ : Finite ι
⊢ ∀ {R : ι → Type u_1} [inst : (i : ι) → Semiring (R i)] [∀ (i : ι), IsNoetherianRing (R i)],
    IsNoetherianRing ((i : ι) → R i)

Tactic:
by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherianRing_of_ringEquiv _ (.symm .piOptionEquivProd)

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

Goal state before:
pp: ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
⊢ 1 = update 0 i r * x + update 1 i y

Tactic:
ext j

Goal state after:
ι : Type u_4
R : ι → Type u_5
inst✝ : (i : ι) → Semiring (R i)
i : ι
I : Ideal (R i)
h : I.IsMaximal
J : Ideal ((i : ι) → R i)
x : (i : ι) → R i
le : comap (Pi.evalRingHom R i) I ≤ J
hxI : x ∉ comap (Pi.evalRingHom R i) I
hxJ : x ∈ J
r y : R i
hy : y ∈ I
eq : r * (Pi.evalRingHom R i) x + y = 1
j : ι
⊢ 1 j = (update 0 i r * x + update 1 i y) j
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 | map f I ≤ J ∧ J.IsPrime} = map f '' {J | I ≤ J ∧ J.IsPrime}

Tactic:
ext j

Goal state after:
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}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : (factors a).prod * ↑c = a
⊢ a ∈ s

Tactic:
rw [← hc]

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
s : Submonoid R
a : R
ha : a ≠ 0
hfac : ∀ b ∈ factors a, b ∈ s
hunit : ∀ (c : Rˣ), ↑c ∈ s
c : Rˣ
hc : (factors a).prod * ↑c = a
⊢ (factors a).prod * ↑c ∈ s
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝³ : CommMonoidWithZero α
inst✝² : IsCancelMulZero α
inst✝¹ : NormalizationMonoid α
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
normalize_lcm : ∀ (a b : α), normalize (lcm a b) = lcm a b
exists_gcd : ∀ (a b : α), lcm a b ∣ a * b := fun a b ↦ lcm_dvd (Dvd.intro b rfl) (Dvd.intro_left a rfl)
this : GCDMonoid α := gcdMonoidOfLCM lcm dvd_lcm_left dvd_lcm_right ⋯
a b : α
h : ¬a = 0
h_1 : ¬b = 0
⊢ Associated (lcm a b * normalize (Classical.choose ⋯)) (a * b)

Tactic:
exact ((normalize_associated _).mul_left _).trans
        (.of_eq (Classical.choose_spec (exists_gcd a b)).symm)

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
ι : Type w
inst✝ : RankCondition R
J : Set M
v : Basis ι R M
hJ : span R J = ⊤
⊢ #↑(range ⇑v) ≤ #↑J

Tactic:
by
  have := nontrivial_of_invariantBasisNumber R
  cases fintypeOrInfinite J
  · rw [← Cardinal.lift_le, Cardinal.mk_range_eq_of_injective v.injective, Cardinal.mk_fintype J]
    convert! Cardinal.lift_le.{v}.2 (basis_le_span' v hJ)
    simp
  · let S : J → Set ι := fun j => ↑(v.repr j).support
    let S' : J → Set M := fun j => v '' S j
    have hs : range v ⊆ ⋃ j, S' j := by
      intro b hb
      rcases mem_range.1 hb with ⟨i, hi⟩
      have : span R J ≤ comap v.repr.toLinearMap (Finsupp.supported R R (⋃ j, S j)) :=
        span_le.2 fun j hj x hx => ⟨_, ⟨⟨j, hj⟩, rfl⟩, hx⟩
      rw [hJ] at this
      replace : v.repr (v i) ∈ Finsupp.supported R R (⋃ j, S j) := this trivial
      rw [v.repr_self, Finsupp.mem_supported, Finsupp.support_single _ one_ne_zero] at this
      · subst b
        rcases mem_iUnion.1 (this (Finset.mem_singleton_self _)) with ⟨j, hj⟩
        exact mem_iUnion.2 ⟨j, (mem_image _ _ _).2 ⟨i, hj, rfl⟩⟩
    refine le_of_not_gt fun IJ => ?_
    suffices #(⋃ j, S' j) < #(range v) by exact not_le_of_gt this ⟨Set.embeddingOfSubset _ _ hs⟩
    refine lt_of_le_of_lt (le_trans Cardinal.mk_iUnion_le_sum_mk
      (Cardinal.sum_le_sum _ (fun _ => ℵ₀) ?_)) ?_
    · exact fun j => (Cardinal.lt_aleph0_of_finite _).le
    · simpa

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
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ #ι ≤ ↑(Fintype.card ↑w)

Tactic:
rw [Cardinal.mk_fintype]

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type u_2
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
this✝ : Finite ι
this : Fintype ι := Fintype.ofFinite ι
⊢ ↑(Fintype.card ι) ≤ ↑(Fintype.card ↑w)
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_5
S : Type u_6
α : Type u_7
β : Type u_8
inst✝¹¹ : DecidableEq m
inst✝¹⁰ : DecidableEq n
inst✝⁹ : Fintype m
inst✝⁸ : Fintype n
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module R β
inst✝¹ : Module S β
inst✝ : SMulCommClass R S β
f : m → n → α →ₗ[R] β
i : m
j : n
a : α
⊢ ((LinearMap.lsum R (fun i ↦ n → α) S) fun i ↦ (LinearMap.lsum R (fun a ↦ α) S) (f i)) (Pi.single i (Pi.single j a)) =
    (f i j) a

Tactic:
LinearMap.lsum_piSingle

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
⊢ (single i i c).diag = Pi.single i c

Tactic:
ext j

Goal state after:
n : Type u_3
α : Type u_7
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : n
c : α
j : n
⊢ (single i i c).diag j = Pi.single i c j
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
⊢ M *ᵥ Pi.single j 1 = M.col j

Tactic:
by ext; simp

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype m
inst✝¹ : DecidableEq m
inst✝ : NonAssocSemiring R
i : m
M : Matrix m n R
⊢ Pi.single i 1 ᵥ* M = M.row i

Tactic:
by ext; simp

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 n
A : Matrix m n α
⊢ A *ᵥ 1 = ∑ j, Aᵀ j

Tactic:
ext; simp [mulVec, dotProduct]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
A : Matrix m n α
B : Matrix o n α
x : o → α
⊢ A *ᵥ x ᵥ* B = (A * Bᵀ) *ᵥ x

Tactic:
rw [← mulVec_mulVec, mulVec_transpose]

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

Goal state before:
pp: ι : Type u_3
s : Finset ι
n : ℕ
⊢ toMultiset (∑ i ∈ s, single i n) = n • s.val

Tactic:
simp_rw [toMultiset_sum, Finsupp.toMultiset_single, Finset.sum_nsmul, sum_multiset_singleton]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
f : α →₀ ℕ
⊢ (toMultiset f).prod = f.prod fun a n ↦ a ^ n

Tactic:
refine f.induction ?_ ?_
  · rw [toMultiset_zero, Multiset.prod_zero, Finsupp.prod_zero_index]
  · intro a n f _ _ ih
    rw [toMultiset_add, Multiset.prod_add, ih, toMultiset_single, Multiset.prod_nsmul,
      Finsupp.prod_add_index' pow_zero pow_add, Finsupp.prod_single_index, Multiset.prod_singleton]
    exact pow_zero a

Goal state after:
Module: Mathlib.Algebra.Algebra.Subalgebra.Tower

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ (↑(toAlgHom R (↥S) A)).range ↔ x✝ ∈ toSubmodule S

Tactic:
simp [algebraMap_eq]

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

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
k : κ
x : M (e.symm k)
⊢ (lequivCongrLeft R e) ((lof R ι M (e.symm k)) x) = (lof R κ (fun i ↦ M (e.symm i)) k) (cast ⋯ x)

Tactic:
ext j

Goal state after:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
e : ι ≃ κ
k : κ
x : M (e.symm k)
j : κ
⊢ ((lequivCongrLeft R e) ((lof R ι M (e.symm k)) x)) j = ((lof R κ (fun i ↦ M (e.symm i)) k) (cast ⋯ x)) j
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
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
⊢ (mk R M R).compr₂ₛₗ ((mk R M R).flip 1 ∘ₗ lift (LinearMap.lsmul R M).flip) = (mk R M R).compr₂ₛₗ LinearMap.id

Tactic:
by ext; simp

Goal state after:
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
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ LinearMap.id x = x

Tactic:
LinearMap.id_apply

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
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ x = x
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_8
S : Type u_9
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
M : Type u_10
N : Type u_11
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R M
inst✝³ : Module S N
σ : R →+* S
σ' : S →+* R
inst✝² : RingHomInvPair σ σ'
inst✝¹ : RingHomInvPair σ' σ
e₂ : M ≃ₛₗ[σ] N
inst✝ : Projective R M
e₁ : R ≃+* S := RingHomInvPair.toRingEquiv σ σ'
f : M →ₗ[R] M →₀ R
hf : Function.LeftInverse ⇑(linearCombination R id) ⇑f
x y : N
⊢ mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm (x + y)))) =
    mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm x))) +
      mapRange ⇑e₁ ⋯ ((Finsupp.equivCongrLeft ↑e₂) (f (e₂.symm y)))

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b

Tactic:
have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
inst✝ : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
this : b * a = 0
⊢ Commute a b
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ b.repr ((b.prod b') (Sum.inl i)).1 = b.repr (b i)

Tactic:
ext j

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i j : ι
⊢ (b.repr ((b.prod b') (Sum.inl i)).1) j = (b.repr (b i)) j
Module: Mathlib.LinearAlgebra.Basis.Prod

Goal state before:
pp: ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
⊢ b'.repr ((b.prod b') (Sum.inl i)).2 = b'.repr 0

Tactic:
ext j

Goal state after:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_5
M' : Type u_6
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
i : ι
j : ι'
⊢ (b'.repr ((b.prod b') (Sum.inl i)).2) j = (b'.repr 0) j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inl.inr
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
v : n → α
i : n
x : α
j : n
hji : j ≠ i
⊢ (diagonal v).updateCol i (Pi.single i x) j j = Function.update v i x j

Tactic:
rw [updateCol_ne hji, diagonal_apply_eq, Function.update_of_ne hji]

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

Goal state before:
pp: case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ diagonal d (i, k) (j, k) = diagonal (fun i ↦ d (i, k)) i j

Tactic:
diagonal_apply_ne _ hij,

Goal state after:
case inr
m : Type u_2
o : Type u_4
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : DecidableEq m
d : m × o → α
k : o
i j : m
hij : i ≠ j
⊢ diagonal d (i, k) (j, k) = 0
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case inr
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
v : m → α
B : Matrix m n α
j : n
r : m → α
j' : n
hj : j' ≠ j
⊢ (v ᵥ* B.updateCol j r) j' = Function.update (v ᵥ* B) j (v ⬝ᵥ r) j'

Tactic:
· simp [vecMul, hj]

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

Goal state before:
pp: case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ diagonal d ⟨k, i⟩ ⟨k, j⟩ = diagonal (fun i ↦ d ⟨k, i⟩) i j

Tactic:
diagonal_apply_ne _ hij,

Goal state after:
case inr
o : Type u_4
m' : o → Type u_7
α : Type u_12
inst✝² : Zero α
inst✝¹ : DecidableEq o
inst✝ : (i : o) → DecidableEq (m' i)
d : (i : o) × m' i → α
k : o
i j : m' k
hij : i ≠ j
⊢ diagonal d ⟨k, i⟩ ⟨k, j⟩ = 0
Module: Mathlib.Algebra.Star.StarAlgHom

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₙₐ[R] A₂
⊢ (fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom) f) =
    f

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : Monoid R
inst✝¹⁷ : NonUnitalNonAssocSemiring A₁
inst✝¹⁶ : DistribMulAction R A₁
inst✝¹⁵ : Star A₁
inst✝¹⁴ : NonUnitalNonAssocSemiring A₂
inst✝¹³ : DistribMulAction R A₂
inst✝¹² : Star A₂
inst✝¹¹ : NonUnitalNonAssocSemiring A₃
inst✝¹⁰ : DistribMulAction R A₃
inst✝⁹ : Star A₃
inst✝⁸ : NonUnitalNonAssocSemiring A₁'
inst✝⁷ : DistribMulAction R A₁'
inst✝⁶ : Star A₁'
inst✝⁵ : NonUnitalNonAssocSemiring A₂'
inst✝⁴ : DistribMulAction R A₂'
inst✝³ : Star A₂'
inst✝² : NonUnitalNonAssocSemiring A₃'
inst✝¹ : DistribMulAction R A₃'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₙₐ[R] A₂'
⊢ (fun f ↦ (e₂.toNonUnitalStarAlgHom.comp f).comp e₁.symm.toNonUnitalStarAlgHom)
      ((fun f ↦ (e₂.symm.toNonUnitalStarAlgHom.comp f).comp e₁.toNonUnitalStarAlgHom) f) =
    f

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁ →⋆ₐ[R] A₂
⊢ (fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom)
      ((fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom) f) =
    f

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
A₁ : Type u_2
A₂ : Type u_3
A₃ : Type u_4
A₁' : Type u_5
A₂' : Type u_6
A₃' : Type u_7
inst✝¹⁸ : CommSemiring R
inst✝¹⁷ : Semiring A₁
inst✝¹⁶ : Semiring A₂
inst✝¹⁵ : Semiring A₃
inst✝¹⁴ : Semiring A₁'
inst✝¹³ : Semiring A₂'
inst✝¹² : Semiring A₃'
inst✝¹¹ : Algebra R A₁
inst✝¹⁰ : Algebra R A₂
inst✝⁹ : Algebra R A₃
inst✝⁸ : Algebra R A₁'
inst✝⁷ : Algebra R A₂'
inst✝⁶ : Algebra R A₃'
inst✝⁵ : Star A₁
inst✝⁴ : Star A₂
inst✝³ : Star A₃
inst✝² : Star A₁'
inst✝¹ : Star A₂'
inst✝ : Star A₃'
e : A₁ ≃⋆ₐ[R] A₂
e₁ : A₁ ≃⋆ₐ[R] A₁'
e₂ : A₂ ≃⋆ₐ[R] A₂'
f : A₁' →⋆ₐ[R] A₂'
⊢ (fun f ↦ (e₂.toStarAlgHom.comp f).comp e₁.symm.toStarAlgHom)
      ((fun f ↦ (e₂.symm.toStarAlgHom.comp f).comp e₁.toStarAlgHom) f) =
    f

Tactic:
by ext; simp

Goal state after:
Module: Mathlib.LinearAlgebra.FreeModule.PID

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
⊢ generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩

Tactic:
have d_dvd_right : d ∣ ψ ⟨y, hNO yN⟩ :=
    (mem_iff_generator_dvd _).mp (subset_span (mem_insert_of_mem _ (mem_singleton _)))

Goal state after:
R : Type u_2
inst✝⁴ : CommRing R
M : Type u_3
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : ↥O →ₗ[R] R
hϕ : ∀ (ψ : ↥O →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst✝ : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = generator (ϕ.submoduleImage N)
ψ : ↥O →ₗ[R] R
a : R := generator (ϕ.submoduleImage N)
d : R := generator (span R {a, ψ ⟨y, ⋯⟩})
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∣ ψ ⟨y, ⋯⟩
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) =
    LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type uR
S : Type uS
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
P' : Type uP'
Q' : Type uQ'
inst✝²⁶ : CommSemiring R
inst✝²⁵ : CommSemiring A
inst✝²⁴ : Semiring B
inst✝²³ : Algebra R A
inst✝²² : Algebra R B
inst✝²¹ : AddCommMonoid M
inst✝²⁰ : Module R M
inst✝¹⁹ : Module A M
inst✝¹⁸ : Module B M
inst✝¹⁷ : IsScalarTower R A M
inst✝¹⁶ : IsScalarTower R B M
inst✝¹⁵ : SMulCommClass A B M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R N
inst✝¹² : AddCommMonoid P
inst✝¹¹ : Module A P
inst✝¹⁰ : AddCommMonoid P'
inst✝⁹ : Module A P'
inst✝⁸ : AddCommMonoid Q
inst✝⁷ : Module R Q
inst✝⁶ : CommSemiring S
inst✝⁵ : Module S M
inst✝⁴ : Module S P
inst✝³ : Algebra S B
inst✝² : IsScalarTower S B M
inst✝¹ : SMulCommClass R S M
inst✝ : SMulCommClass S R M
⊢ lift (lift (↑lflip ∘ₗ (mk S B M P).compr₂ (mk R B (M ⊗[S] P) Q))) ∘ₗ
      lift (lift (↑lflip ∘ₗ (mk R B M Q).compr₂ (mk S B (M ⊗[R] Q) P))) =
    LinearMap.id

Tactic:
by ext; simp

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
x : R
⊢ (toMatrix v₁ v₁) ((algebraMap R (End R M₁)) x) = (scalar n) x

Tactic:
by
  simp [Module.algebraMap_end_eq_smul_id, LinearMap.toMatrix_id, smul_eq_diagonal_mul]

Goal state after: