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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
normUnit✝ : α → αˣ
normUnit_zero✝ : normUnit✝ 0 = 1
normUnit_one✝ : normUnit✝ 1 = 1
normUnit_mul_units✝ : ∀ {a : α} (u : αˣ), a ≠ 0 → normUnit✝ (a * ↑u) = u⁻¹ * normUnit✝ a
⊢ normUnit✝ = fun x ↦ 1

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
normUnit✝ : α → αˣ
normUnit_zero✝ : normUnit✝ 0 = 1
normUnit_one✝ : normUnit✝ 1 = 1
normUnit_mul_units✝ : ∀ {a : α} (u : αˣ), a ≠ 0 → normUnit✝ (a * ↑u) = u⁻¹ * normUnit✝ a
⊢ normUnit✝ = fun x ↦ 1
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toNormalizationMonoid✝ : NormalizationMonoid α
normUnit_mul✝ : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units✝ : ∀ (u : αˣ), normUnit ↑u = u⁻¹
⊢ { toNormalizationMonoid := toNormalizationMonoid✝, normUnit_mul := normUnit_mul✝,
      normUnit_coe_units := normUnit_coe_units✝ } =
    inferInstance

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toNormalizationMonoid✝ : NormalizationMonoid α
normUnit_mul✝ : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units✝ : ∀ (u : αˣ), normUnit ↑u = u⁻¹
⊢ { toNormalizationMonoid := toNormalizationMonoid✝, normUnit_mul := normUnit_mul✝,
      normUnit_coe_units := normUnit_coe_units✝ } =
    inferInstance
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toNormalizationMonoid✝ : NormalizationMonoid α
normUnit_mul✝ : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units✝ : ∀ (u : αˣ), normUnit ↑u = u⁻¹
⊢ toNormalizationMonoid✝ = { normUnit := fun x ↦ 1, normUnit_zero := ⋯, normUnit_one := ⋯, normUnit_mul_units := ⋯ }

Tactic:
;

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
toNormalizationMonoid✝ : NormalizationMonoid α
normUnit_mul✝ : ∀ {a b : α}, a ≠ 0 → b ≠ 0 → normUnit (a * b) = normUnit a * normUnit b
normUnit_coe_units✝ : ∀ (u : αˣ), normUnit ↑u = u⁻¹
⊢ toNormalizationMonoid✝ = { normUnit := fun x ↦ 1, normUnit_zero := ⋯, normUnit_one := ⋯, normUnit_mul_units := ⋯ }
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
I : Ideal R
n : ℕ
hn : s.card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i

Tactic:
;

Goal state after:
ι : Type u_1
R : Type u
inst✝ : CommRing R
s : Finset ι
f : ι → Ideal R
a b : ι
hp : ∀ i ∈ s, (f i).IsPrime
I : Ideal R
n : ℕ
hn : s.card = n
⊢ ↑I ⊆ ↑(f a) ∪ ↑(f b) ∪ ⋃ i ∈ ↑s, ↑(f i) → I ≤ f a ∨ I ≤ f b ∨ ∃ i ∈ s, I ≤ f i
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
x✝ : Fin n
⊢ (LinearMap.funLeft R R Fin.castSucc) 0 x✝ = (LinearMap.funLeft R R Fin.castSucc) (update 0 (Fin.last n) 1) x✝

Tactic:
;

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.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ generator S ∈ S

Tactic:
have : generator S ∈ span R {generator S} := subset_span (mem_singleton _)

Goal state after:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
this : generator S ∈ R ∙ generator S
⊢ generator S ∈ S
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
⊢ Fintype.card α ≤ Fintype.card β

Tactic:
by
  let P := Finsupp.linearEquivFunOnFinite R R β
  let Q := (Finsupp.linearEquivFunOnFinite R R α).symm
  exact card_le_of_injective R (P.toLinearMap ∘ₗ f ∘ₗ Q) (P.injective.comp (i.comp Q.injective))

Goal state after:
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: R : Type u
inst✝ : Semiring R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔
    ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
;

Goal state after:
R : Type u
inst✝ : Semiring R
⊢ (¬∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f) ↔
    ¬∀ (n : ℕ) (f : (ℕ →₀ R) →ₗ[R] Fin n → R), ¬Injective ⇑f
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
b : ι → R
⊢ induced_map I (↑e)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a +
        Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b) =
    induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a) +
      induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b)

Tactic:
;

Goal state after:
case mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
a : ι → R
y✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
b : ι → R
⊢ induced_map I (↑e)
      (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a +
        Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b) =
    induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a) +
      induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
m✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
b : ι → R
⊢ induced_map I (↑e)
      (Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b) =
    (RingHom.id (R ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel I)) a) •
      induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b)

Tactic:
;

Goal state after:
case mk.mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
m✝ : R ⧸ I
a : R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
b : ι → R
⊢ induced_map I (↑e)
      (Quot.mk (⇑(Submodule.quotientRel I)) a • Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b) =
    (RingHom.id (R ⧸ I)) (Quot.mk (⇑(Submodule.quotientRel I)) a) •
      induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) b)
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
a : ι → R
⊢ induced_map I (↑e.symm) (induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι → R) ⧸ Ideal.pi fun x ↦ I
a : ι → R
⊢ induced_map I (↑e.symm) (induced_map I (↑e) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a
Module: Mathlib.LinearAlgebra.InvariantBasisNumber

Goal state before:
pp: case mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi fun x ↦ I
a : ι' → R
⊢ induced_map I (↑e) (induced_map I (↑e.symm) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a

Tactic:
;

Goal state after:
case mk
R : Type u
inst✝² : CommRing R
I✝ : Ideal R
ι : Type v
inst✝¹ : Fintype ι
ι' : Type w
inst✝ : Fintype ι'
I : Ideal R
e : (ι → R) ≃ₗ[R] ι' → R
x✝ : (ι' → R) ⧸ Ideal.pi fun x ↦ I
a : ι' → R
⊢ induced_map I (↑e) (induced_map I (↑e.symm) (Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a)) =
    Quot.mk (⇑(Submodule.quotientRel (Ideal.pi fun x ↦ I))) a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ Ideal.span {gcd x y}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : CommRing R
x y : R
inst✝ : IsPrincipal (Ideal.span {x, y})
⊢ gcd x y ∈ {gcd x y}
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : R ∙ p < R ∙ a
⊢ R ∙ a = ⊤

Tactic:
rw [Ideal.submodule_span_eq, Ideal.span_singleton_eq_top]

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : IsPrincipalIdealRing R
p : R
hp : Irreducible p
a : R
hI : R ∙ p < R ∙ a
⊢ IsUnit a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧
    Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a

Tactic:
;

Goal state after:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧
    Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ IsCoprime x y

Tactic:
IsCoprime,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : IsBezout R
inst✝¹ : IsDomain R
inst✝ : GCDMonoid R
x y : R
⊢ IsUnit (gcd x y) ↔ ∃ a b, a * x + b * y = 1
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
n m x : R
⊢ x ∈ Ideal.span {n} ∧ x ∈ Ideal.span {m} ↔ x ∈ Ideal.span {lcm n m}

Tactic:
simp only [Ideal.mem_span_singleton]

Goal state after:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : GCDMonoid R
n m x : R
⊢ n ∣ x ∧ m ∣ x ↔ lcm n m ∣ x
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
x✝ : Matrix m n α
⊢ (fun M ↦ M.map f) ((fun M ↦ M.map f) x✝) = x✝

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
f : α → α
hf : Function.Involutive f
x✝ : Matrix m n α
⊢ (fun M ↦ M.map f) ((fun M ↦ M.map f) x✝) = x✝
Module: Mathlib.LinearAlgebra.Matrix.Defs

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✝ : IsEmpty m
M N : Matrix m n α
i : m
j✝ : n
⊢ M i j✝ = N i j✝

Tactic:
exact isEmptyElim i

Goal state after:
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:
;

Goal state after:
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
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 α)) b

Tactic:
;

Goal state after:
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 α)) b
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
⊢ Quotient.map₂ lcm ⋯ 0 (Quot.mk (⇑(Associated.setoid α)) a) = 0
Module: Mathlib.Algebra.GCDMonoid.Basic

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

Tactic:
;

Goal state after:
case mk
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : GCDMonoid α
a✝ : Associates α
a : α
⊢ Quotient.map₂ lcm ⋯ (Quot.mk (⇑(Associated.setoid α)) a) 0 = 0
Module: Mathlib.Data.Matrix.Diagonal

Goal state before:
pp: n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (if i✝ = j✝ then d i✝ else 0) ∈ S

Tactic:
;

Goal state after:
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
d : n → α
i✝ j✝ : n
| (if i✝ = j✝ then d i✝ else 0) ∈ S
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 w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #ι < #κ
⊢ False

Tactic:
← Cardinal.mk_finset_of_infinite ι

Goal state after:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : StrongRankCondition R
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w
v : κ → M
i : LinearIndependent R v
h : #(Finset ι) < #κ
⊢ False
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b✝ : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ (((linearCombination R fun i ↦ f (single i 1)) ∘ₗ lsingle a) 1) b = ((f ∘ₗ lsingle a) 1) b

Tactic:
;

Goal state after:
R : Type u
inst✝¹ : Semiring R
inst✝ : StrongRankCondition R
α β : Type v
f : (α →₀ R) →ₗ[R] β →₀ R
i : Injective ⇑f
b✝ : Basis β R (β →₀ R) := { repr := 1 }
a : α
b : β
⊢ (((linearCombination R fun i ↦ f (single i 1)) ∘ₗ lsingle a) 1) b = ((f ∘ₗ lsingle a) 1) b
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 α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (if i = i✝ ∧ j = j✝ then a else 0) ∈ S

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_7
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
S : Set α
hS : 0 ∈ S
i : m
j : n
a : α
i✝ : m
j✝ : n
| (if i = i✝ ∧ j = j✝ then a else 0) ∈ S
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: case intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝ : Fintype m
⊢ P M

Tactic:
;

Goal state after:
case intro
m : Type u_2
n : Type u_3
α : Type u_7
inst✝⁴ : DecidableEq m
inst✝³ : DecidableEq n
inst✝² : AddCommMonoid α
inst✝¹ : Finite m
inst✝ : Finite n
P : Matrix m n α → Prop
M : Matrix m n α
h_zero : P 0
h_add : ∀ (p q : Matrix m n α), P p → P q → P (p + q)
h_std_basis : ∀ (i : m) (j : n) (x : α), P (single i j x)
val✝ : Fintype m
⊢ P M
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ (m + 1)) i j

Tactic:
;

Goal state after:
case succ
n : Type u_3
α : Type v
inst✝⁴ : Semiring α
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : PartialOrder α
inst✝ : IsOrderedRing α
A : Matrix n n α
hA : ∀ (i j : n), 0 ≤ A i j
m : ℕ
ih : ∀ (i j : n), 0 ≤ (A ^ m) i j
i j : n
⊢ 0 ≤ (A ^ (m + 1)) i j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
⊢ b ∈ I ^ n

Tactic:
obtain hb := congr($hc * b)

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : I.IsMaximal
a b : R
n : ℕ
h : a * b ∈ I ^ n
ha : a ∉ I
c i : R
hi : i ∈ I ^ n
hc : c * a + i = 1
hb : (c * a + i) * b = 1 * b
⊢ b ∈ I ^ n
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ⟨0, ⋯⟩ = 0

Tactic:
;

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
a : ι →₀ R
ha : ∀ (i : ι), a i ∈ I
⊢ ⟨0, ⋯⟩ = 0
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
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = M.col j x✝

Tactic:
;

Goal state after:
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
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = M.col j x✝
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
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M.row i x✝

Tactic:
;

Goal state after:
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
x✝ : n
⊢ (Pi.single i 1 ᵥ* M) x✝ = M.row i x✝
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
left✝ : r ∈ ↑I
a : A
a✝ : a ∈ M
⊢ Commute ((Algebra.linearMap R A) r) a

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
left✝ : r ∈ ↑I
a : A
a✝ : a ∈ M
⊢ Commute ((Algebra.linearMap R A) r) a
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ (algebraMap R A) r * a ∈
    { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ I
a : A
ha : a ∈ M
⊢ (algebraMap R A) r * a ∈
    { toFun := map (Algebra.linearMap R A), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } I * M
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ (Algebra.linearMap R A) r * a ∈ I • M

Tactic:
;

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
M✝ : Type u_2
inst✝⁵ : AddCommMonoid M✝
inst✝⁴ : Module R M✝
A : Type ?u.13
B : Type ?u.15
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
I : Ideal R
M : Submodule R A
r : R
hr : r ∈ ↑I
a : A
ha : a ∈ M
⊢ (Algebra.linearMap R A) r * a ∈ I • M
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 α
x✝ : m
⊢ (A *ᵥ 1) x✝ = (∑ j, Aᵀ j) x✝

Tactic:
;

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A : Matrix m n α
x✝ : m
⊢ (A *ᵥ 1) x✝ = (∑ j, Aᵀ j) x✝
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:
;

Goal state after:
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✝
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:
;

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

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

Tactic:
;

Goal state after:
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
x : A
ij : ι' × ι
⊢ (b.repr ((c.repr x) ((Equiv.prodComm ι ι').symm ij).2)) ((Equiv.prodComm ι ι').symm ij).1 =
    (b.repr ((c.repr x) ij.1)) ij.2
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
⊢ (v ᵥ* diagonal fun x_1 ↦ x) x✝ = (MulOpposite.op x • v) x✝

Tactic:
;

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