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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : Subsingleton αˣ
g₁ g₂ : GCDMonoid α
⊢ g₁ = g₂

Tactic:
by
    have hgcd : g₁.gcd = g₂.gcd := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [dvd_gcd, gcd_dvd_left, gcd_dvd_right]
    have hlcm : g₁.lcm = g₂.lcm := by
      ext a b
      refine associated_iff_eq.mp (associated_of_dvd_dvd ?_ ?_) <;>
      apply_rules +allowSynthFailures [lcm_dvd, dvd_lcm_left, dvd_lcm_right]
    cases g₁
    cases g₂
    dsimp only at hgcd hlcm
    simp only [hgcd, hlcm]

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

Goal state before:
pp: case pos
α : 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 : α
h : a = 0
⊢ b ∣ a

Tactic:
h

Goal state after:
case pos
α : 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 : α
h : a = 0
⊢ b ∣ 0
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: case pos
α : 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
⊢ normalize b ∣ a

Tactic:
h

Goal state after:
case pos
α : 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
⊢ normalize b ∣ 0
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
f g : ι →₀ R
⊢ (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g →
    f = g

Tactic:
h

Goal state after:
case i
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : StrongRankCondition R
ι : Type u_2
inst✝¹ : Fintype ι
v : ι → M
i : LinearIndependent R v
w : Set M
inst✝ : Fintype ↑w
s : range v ⊆ ↑(span R w)
f g : ι →₀ R
h : (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
⊢ (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g →
    f = g

Tactic:
h

Goal state after:
case i
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : StrongRankCondition R
ι : Type v
v : ι → M
i : LinearIndependent R v
w : Set M
s : span R w = ⊤
f g : ι →₀ R
h : (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) f = (linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩) g
⊢ f = g
Module: Mathlib.Data.Matrix.Mul

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : NonUnitalNonAssocSemiring α
x y : n → α
e : m ≃ n
⊢ x ∘ ⇑e ⬝ᵥ y ∘ ⇑e = x ⬝ᵥ y

Tactic:
by
  simp [← dotProduct_comp_equiv_symm, Function.comp_def _ e.symm]

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

Goal state before:
pp: case intro.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
val✝ : Fintype n
⊢ P M

Tactic:
rw [matrix_eq_sum_single M, ← Finset.sum_product']

Goal state after:
case intro.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
val✝ : Fintype n
⊢ P (∑ x ∈ Finset.univ ×ˢ Finset.univ, single x.1 x.2 (M x.1 x.2))
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = I

Tactic:
h

Goal state after:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
h : I = ⊤
⊢ ⊤ = ⊤
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
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0

Tactic:
exact fun _ => zero_smul _ _

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

Goal state before:
pp: case h
ι : 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
inst✝ : Fintype ι
f : ι →₀ ↥I
⊢ ∀ (i : ι), ↑0 • v i = 0

Tactic:
exact fun _ => zero_smul _ _

Goal state after:
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
⊢ ∀ (a : ι), ↑0 • v a = 0

Tactic:
exact fun _ => zero_smul _ _

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 B : Matrix m n α
⊢ A.mulVec = B.mulVec → A = B

Tactic:
h

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype n
A B : Matrix m n α
h : A.mulVec = B.mulVec
⊢ A = B
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 B : Matrix m n α
⊢ (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B → A = B

Tactic:
h

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonAssocSemiring α
inst✝ : Fintype m
A B : Matrix m n α
h : (fun x v ↦ v ᵥ* x) A = (fun x v ↦ v ᵥ* x) B
⊢ A = B
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
this : ci i = ⟨↑c, hi⟩
⊢ f i (ci i) = cβ

Tactic:
h

Goal state after:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
c : ↑T
ci : (i : ι) → ↑(S i)
hci : ∀ (i : ι), ↑(ci i) = ↑c
cβ : β
h : ∀ (i : ι), f i (ci i) = cβ
i : ι
hi : ↑c ∈ S i
this : ci i = ⟨↑c, hi⟩
⊢ cβ = cβ
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
a : α
n : ℕ
⊢ toMultiset (single a n) = n • {a}

Tactic:
by
  rw [toMultiset_apply, sum_single_index]; apply zero_nsmul

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ ({a}.prod ^ n * f.prod fun a n ↦ a ^ n) = (single a n).prod HPow.hPow * f.prod HPow.hPow

Tactic:
Finsupp.prod_single_index,

Goal state after:
case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ ({a}.prod ^ n * f.prod fun a n ↦ a ^ n) = a ^ n * f.prod HPow.hPow

case refine_2
α : Type u_1
inst✝ : CommMonoid α
f✝ : α →₀ ℕ
a : α
n : ℕ
f : α →₀ ℕ
a✝¹ : a ∉ f.support
a✝ : n ≠ 0
ih : (toMultiset f).prod = f.prod fun a n ↦ a ^ n
⊢ a ^ 0 = 1
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | t₁ x 0}
⊢ t₂ a b

Tactic:
h

Goal state after:
case refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ t₂ a b
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
⊢ c • LinearMap.id = d • LinearMap.id → d = c

Tactic:
hcd

Goal state after:
case h
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
u : M →ₗ[R] M
e : R ≃ₗ[R] M := ⋯.some
c : R := e.symm (u (e 1))
hc : c = e.symm (u (e 1))
this : u = c • LinearMap.id
d : R
hcd : c • LinearMap.id = d • LinearMap.id
⊢ d = c
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
h

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ S.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring

Tactic:
h

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : NonUnitalNonAssocRing A
inst✝ : Module R A
S T : NonUnitalSubalgebra R A
h : S.toNonUnitalSubring = T.toNonUnitalSubring
x : A
⊢ x ∈ T.toNonUnitalSubring ↔ x ∈ T.toNonUnitalSubring
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)
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ (component R ι M x✝) f = (component R ι M x✝) g

Tactic:
h

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)
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ (component R ι M x✝) g = (component R ι M x✝) g
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring

Tactic:
h

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubsemiring = T.toSubsemiring
x : A
⊢ x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
⊢ x ∈ S.toSubring ↔ x ∈ T.toSubring

Tactic:
h

Goal state after:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
S T : Subalgebra R A
h : S.toSubring = T.toSubring
x : A
⊢ x ∈ T.toSubring ↔ x ∈ T.toSubring
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case algebraMap
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
p : (x y : A) → x ∈ adjoin R s → y ∈ adjoin R s → Prop
mem_mem : ∀ (x y : A) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯
algebraMap_both : ∀ (r₁ r₂ : R), p ((algebraMap R A) r₁) ((algebraMap R A) r₂) ⋯ ⋯
algebraMap_left : ∀ (r : R) (x : A) (hx : x ∈ s), p ((algebraMap R A) r) x ⋯ ⋯
algebraMap_right : ∀ (r : R) (x : A) (hx : x ∈ s), p x ((algebraMap R A) r) ⋯ ⋯
add_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz
add_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y + z) hx ⋯
mul_left :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz
mul_right :
  ∀ (x y z : A) (hx : x ∈ adjoin R s) (hy : y ∈ adjoin R s) (hz : z ∈ adjoin R s),
    p x y hx hy → p x z hx hz → p x (y * z) hx ⋯
x y : A
hx : x ∈ adjoin R s
r : R
⊢ p x ((algebraMap R A) r) hx ⋯

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
r : A
hr : r ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ r ∈ span R ↑(Submonoid.closure s)

Tactic:
rcases Subsemiring.mem_closure_iff_exists_list.1 hr with ⟨L, HL, rfl⟩

Goal state after:
case a
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
hr : (List.map List.prod L).sum ∈ Subalgebra.toSubmodule (adjoin R s)
⊢ (List.map List.prod L).sum ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ x✝ ∈ ⊥.toSubmodule ↔ x✝ ∈ ⊥

Tactic:
simp only [mem_bot, NonUnitalSubalgebra.mem_toSubmodule, Submodule.mem_bot]

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ S

Tactic:
h

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
h : S = ⊤
x : A
⊢ x ∈ ⊤
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case algebraMap
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
s : Set A
x : A
f : A →ₗ[R] B
hf : ∀ (a₁ a₂ : A), f (a₁ * a₂) = f a₁ * f a₂
r : R
⊢ f ((algebraMap R A) r) ∈ adjoin R (⇑f '' (s ∪ {1}))

Tactic:
| algebraMap r =>

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

Goal state before:
pp: case algebraMap
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
a b : A
s : Set A
h : ∀ b ∈ s, Commute a b
r : R
⊢ Commute a ((algebraMap R A) r)

Tactic:
| algebraMap r =>

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

Goal state before:
pp: F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ span E ↑L = span E S

Tactic:
h

Goal state after:
F : Type u_1
E : Type u_2
K : Type u_3
inst✝⁶ : CommSemiring E
inst✝⁵ : Semiring K
inst✝⁴ : SMul F E
inst✝³ : Algebra E K
inst✝² : Semiring F
inst✝¹ : Module F K
inst✝ : IsScalarTower F E K
L : Submonoid K
S : Set K
h : ↑L = ↑(span F S)
⊢ span E ↑(span F S) = span E S
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Algebra R S
b : Basis ι R M
x : S
y : M
i : ι
⊢ ((baseChange S b).repr (x ⊗ₜ[R] y)) i = (b.repr y) i • x

Tactic:
by
  simp [baseChange, tensorProduct]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
ι : Type u_5
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_7
inst✝¹ : Semiring S
inst✝ : Algebra R S
b : Basis ι R M
i : ι
⊢ (baseChange S b) i = 1 ⊗ₜ[R] b i

Tactic:
by
  simp [baseChange, tensorProduct]

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

Goal state before:
pp: R : Type u
inst✝⁹ : CommSemiring R
S : Type u_1
inst✝⁸ : Semiring S
inst✝⁷ : Algebra R S
ι₁ : Type v₁
inst✝⁶ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝⁵ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝⁴ : AddCommMonoid M₂'
inst✝³ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝² : Module R M₂'
inst✝¹ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝ : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
m : ⨁ (i : ι₁), M₁ i
n : M₂'
i : ι₁
this :
  component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
      ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n =
    (AlgebraTensorModule.mk R S (M₁ i) M₂').flip n ∘ₗ component S ι₁ M₁ i
⊢ ((directSumLeft R S M₁ M₂') (m ⊗ₜ[R] n)) i = m i ⊗ₜ[R] n

Tactic:
simpa using! LinearMap.congr_fun this m

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M i✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1

Tactic:
h

Goal state after:
case pos
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : o → Matrix m n α
i✝ : n × o
j✝ : m × o
h : i✝.2 = j✝.2
⊢ M j✝.2 j✝.1 i✝.1 = M j✝.2 j✝.1 i✝.1
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : DecidableEq o
inst✝ : DecidableEq n
A : Matrix m n α
j : o
c : l → α
e : l ≃ m
f : o ≃ n
⊢ (A.submatrix ⇑e ⇑f).updateCol j c = (A.updateCol (f j) fun i ↦ c (e.symm i)).submatrix ⇑e ⇑f

Tactic:
simpa only [← transpose_submatrix, updateRow_transpose] using!
    congr_arg transpose (updateRow_submatrix_equiv Aᵀ j c f e)

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

Goal state before:
pp: case inl
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
r : m → α
B : Matrix m n α
i' : l
j' : n
⊢ (A.updateRow i' r * B) i' j' = (A * B).updateRow i' (r ᵥ* B) i' j'

pp: case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'

Tactic:
· simp [mul_apply, vecMul, dotProduct]

Goal state after:
case inr
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝² : DecidableEq l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : l
r : m → α
B : Matrix m n α
i' : l
j' : n
hi : i' ≠ i
⊢ (A.updateRow i r * B) i' j' = (A * B).updateRow i (r ᵥ* B) i' j'
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
⊢ (blockDiagonal' fun k ↦ M k * N k) = blockDiagonal' M * blockDiagonal' N

Tactic:
ext ⟨k, i⟩ ⟨k', j⟩
  simp only [blockDiagonal'_apply, mul_apply, ← Finset.univ_sigma_univ, Finset.sum_sigma]
  rw [Fintype.sum_eq_single k]
  · simp only [dif_pos]
    split_ifs <;> simp
  · intro j' hj'
    exact Finset.sum_eq_zero fun _ _ => by rw [dif_neg hj'.symm, zero_mul]

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
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ ψ'.submoduleImage N = ϕ.submoduleImage N

Tactic:
apply (le_trans _ this).eq_of_not_lt' (hϕ ψ')

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 := ⋯
d : R := ⋯
d_dvd_left : d ∣ a
d_dvd_right : d ∣ ψ ⟨y, ⋯⟩
r₁ r₂ : R
d_eq : d = r₁ * a + r₂ * ψ ⟨y, ⋯⟩
ψ' : ↥O →ₗ[R] R := ⋯
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ ϕ.submoduleImage N ≤ R ∙ d