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

Goal state before:
pp: case refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ x ∈ s • restrictScalars S N

Tactic:
refine set_smul_inductionOn x x_in ?_ ?_ (fun _ _ _ _ h h' ↦ add_mem h h') (zero_mem _)

Goal state after:
case refine_1.refine_1
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ ∀ ⦃r : R⦄ ⦃n : M⦄, r ∈ ⇑(algebraMap S R) '' s → n ∈ N → r • n ∈ s • restrictScalars S N

case refine_1.refine_2
R : Type u
inst✝⁶ : CommSemiring R
S : Type u_1
M : Type u_2
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
s : Set S
N : Submodule R M
x : M
x_in : x ∈ ⇑(algebraMap S R) '' s • N
⊢ ∀ (r : R) ⦃m : M⦄, m ∈ ⇑(algebraMap S R) '' s • N → m ∈ s • restrictScalars S N → r • m ∈ s • restrictScalars S N
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:
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.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case neg.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ z * (x * gcdA x y)

Tactic:
rw [mul_left_comm]

Goal state after:
case neg.h₁
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
x y z : R
hxz : x ∣ z
hyz : y ∣ z
hxy : ¬gcd x y = 0
r : R
hr : x = gcd x y * r
s : R
hs : y = gcd x y * s
⊢ x * y ∣ x * (z * gcdA x y)
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝ : Semiring R
I J : Ideal R
⊢ 1 ∈ I ⊔ J ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1

Tactic:
Submodule.mem_sup

Goal state after:
R : Type u
inst✝ : Semiring R
I J : Ideal R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = 1) ↔ ∃ i ∈ I, ∃ j ∈ J, i + j = 1
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ r ∈ annihilator R (Π₀ (i : ι), M i) ↔ r ∈ ⨅ i, annihilator R (M i)

Tactic:
simp only [mem_annihilator, Ideal.mem_iInf]

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : Π₀ (i : ι), M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ r ∈ annihilator R ((i : ι) → M i) ↔ r ∈ ⨅ i, annihilator R (M i)

Tactic:
simp only [mem_annihilator, Ideal.mem_iInf]

Goal state after:
R : Type u_1
inst✝² : Semiring R
ι : Type u_4
M : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (M i)
inst✝ : (i : ι) → Module R (M i)
r : R
⊢ (∀ (m : (i : ι) → M i), r • m = 0) ↔ ∀ (i : ι) (m : M i), r • m = 0
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : 1 ∈ I ⊔ J
i : R
hi : i ∈ I ⊔ K
⊢ i ∈ I ⊔ J * K

Tactic:
Submodule.mem_sup

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : I.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ J, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ K, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.Algebra.EuclideanDomain.Basic

Goal state before:
pp: case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ z * (x / (y * z)) = x / y

Tactic:
← EuclideanDomain.mul_div_assoc z h2,

Goal state after:
case inr
R : Type u
inst✝ : EuclideanDomain R
x y z : R
h1 : y ∣ x
h2 : y * z ∣ x
hz : z ≠ 0
⊢ z * x / (y * z) = x / y
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : 1 ∈ I ⊔ K
i : R
hi : i ∈ I ⊔ J
⊢ i ∈ I ⊔ J * K

Tactic:
Submodule.mem_sup

Goal state after:
R : Type u
inst✝¹ : Semiring R
I J K : Ideal R
inst✝ : J.IsTwoSided
h : ∃ y ∈ I, ∃ z ∈ K, y + z = 1
i : R
hi : ∃ y ∈ I, ∃ z ∈ J, y + z = i
⊢ ∃ y ∈ I, ∃ z ∈ J * K, y + z = i
Module: Mathlib.RingTheory.Ideal.Maps

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
g : M
r : R
⊢ r ∈ (R ∙ g).annihilator ↔ r • g = 0

Tactic:
simp [mem_annihilator_span]

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

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ : R
⊢ x✝ ∈ (span R s).annihilator ↔ x✝ ∈ ⨅ g, (toSpanSingleton R M ↑g).ker

Tactic:
simp [mem_annihilator_span]

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = ↑I • restrictScalars S N
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N

Tactic:
rw [coe_set_smul] at this

Goal state after:
R : Type u_1
inst✝⁶ : CommSemiring R
S : Type u_3
M : Type u_4
inst✝⁵ : CommSemiring S
inst✝⁴ : Algebra S R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module S M
inst✝ : IsScalarTower S R M
I : Ideal S
N : Submodule R M
this : restrictScalars S (⇑(algebraMap S R) '' ↑I • N) = I • restrictScalars S N
⊢ restrictScalars S (Ideal.map (algebraMap S R) I • N) = I • restrictScalars S N
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ 1 ∈ span {x} ⊔ span {y} ↔ IsCoprime x y

Tactic:
Submodule.mem_sup

Goal state after:
R : Type u_2
inst✝ : CommSemiring R
x y : R
⊢ (∃ y_1 ∈ span {x}, ∃ z ∈ span {y}, y_1 + z = 1) ↔ IsCoprime x y
Module: Mathlib.Algebra.GCDMonoid.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ normalize (gcd x y) = 1

Tactic:
NormalizedGCDMonoid.normalize_gcd

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
x y : α
hx : Irreducible x
⊢ gcd x y = 1 ↔ gcd x y = 1
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:
exact congr_arg _ (map_add ..)

Goal state after:
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 {x, y}

Tactic:
rw [← span_gcd]; apply Ideal.subset_span; simp

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomain

Goal state before:
pp: R : Type u
M : Type v
inst✝ : EuclideanDomain R
S : Ideal R
h : ¬{x | x ∈ S ∧ x ≠ 0}.Nonempty
a : R
⊢ a ∈ S ↔ a ∈ R ∙ 0

Tactic:
rw [← @Submodule.bot_coe R R _ _ _, span_eq, Submodule.mem_bot]
            exact ⟨fun haS => by_contra fun ha0 => h ⟨a, ⟨haS, ha0⟩⟩,
              fun h₁ => h₁.symm ▸ S.zero_mem⟩

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

Goal state before:
pp: case f
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)
⊢ (ι →₀ R) →ₗ[R] ↑w →₀ R

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)
⊢ Injective ⇑?f

Tactic:
· apply Finsupp.linearCombination
    exact fun i => Span.repr R w ⟨v i, s (mem_range_self i)⟩

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)
⊢ Injective ⇑(linearCombination R fun i ↦ Span.repr R w ⟨v i, ⋯⟩)
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
  apply neg_dotProduct

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_7
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
a : l
b : n
h : a ≠ i
M : Matrix m n α
⊢ (single i j c * M) a b = 0

Tactic:
simp [mul_apply, h.symm]

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

Goal state before:
pp: n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonUnitalNonAssocSemiring R
v : n → R
j : n
x : R
⊢ diagonal v *ᵥ Pi.single j x = Pi.single j (v j * x)

Tactic:
by
  ext i
  rw [mulVec_diagonal]
  exact Pi.apply_single (fun i x => v i * x) (fun i => mul_zero _) j x i

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✝² : NonUnitalSemiring α
inst✝¹ : Fintype n
inst✝ : Fintype o
v : o → α
M : Matrix m n α
N : Matrix n o α
⊢ M *ᵥ N *ᵥ v = (M * N) *ᵥ v

Tactic:
by
  ext
  symm
  apply dotProduct_assoc

Goal state after:
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
s : Set R
N : Submodule R M
⊢ Ideal.span s • N = s • N

Tactic:
by
  rw [← coe_set_smul, coe_span_smul]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype m
v : m → α
A : Matrix m n α
⊢ -v ᵥ* A = -(v ᵥ* A)

Tactic:
ext
  apply neg_dotProduct

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocRing α
inst✝ : Fintype n
v : n → α
A : Matrix m n α
⊢ -A *ᵥ v = -(A *ᵥ v)

Tactic:
ext
  apply neg_dotProduct

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

Goal state before:
pp: α : Type u_1
f : α →₀ ℕ
⊢ (toMultiset f).card = f.sum fun x ↦ id

Tactic:
by
  simp [toMultiset_apply, Function.id_def]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
a : R
ha : a ∈ I
b : R
hb : b ∈ J
⊢ x + a + (y + b) = x + y + (a + b)

Tactic:
by abel

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

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

Tactic:
by abel

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

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ ker f = ⊥ → Function.Injective ⇑f

pp: case mpr
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Function.Injective ⇑f → ker f = ⊥

Tactic:
· intro h x y hxy
    simpa [h, rel_iff, mem_bot, sub_eq_zero] using show (ker f).ringCon x y from hxy

Goal state after:
case mpr
R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Function.Injective ⇑f → ker f = ⊥
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 : Set (Subalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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

Goal state before:
pp: F : Type v'
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✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
φ : F
⊢ ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ

Tactic:
ext
  rw [SetLike.mem_coe, mem_range, Set.mem_range]

Goal state after:
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 : Set A
⊢ centralizer R s.centralizer.centralizer = centralizer R s

Tactic:
apply SetLike.coe_injective
  simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
S : Subring R
i✝ : ℤ
i : ℕ
ih : (algebraMap ℤ R) (-↑i) ∈ S.carrier
⊢ ↑(-↑i) - 1 ∈ S

Tactic:
exact S.sub_mem ih S.one_mem

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
L : List (List A)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod L).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
induction L with

Goal state after:
case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).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
S : Set (NonUnitalSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

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

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ S ⊔ adjoin R (⇑f ⁻¹' {0})

Tactic:
rw [← Algebra.adjoin_eq S, ← Algebra.adjoin_union, ← add_sub_cancel y x]

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ adjoin R (↑S ∪ ⇑f ⁻¹' {0})
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ map f S ⊔ adjoin R (⇑f '' ⇑f ⁻¹' {0}) = map f S

Tactic:
sup_eq_left,

Goal state after:
case a
R : Type uR
A : Type uA
B : Type uB
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
⊢ adjoin R (⇑f '' ⇑f ⁻¹' {0}) ≤ map f S
Module: Mathlib.LinearAlgebra.TensorProduct.Basis

Goal state before:
pp: R : Type u_1
M : Type u_3
N : Type u_4
ι : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq ι
ℬ : Basis ι R M
m : M
n : N
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) (m ⊗ₜ[R] n)) i = (ℬ.repr m) i • n

Tactic:
by
  simp only [equivFinsuppOfBasisLeft_apply_tmul, Finsupp.mapRange_apply]

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

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

Tactic:
simp only [finsuppLeft_apply_tmul_apply, rTensor_tmul, Finsupp.lapply_apply]

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

Goal state before:
pp: case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
Ring.inverse_non_unit _ ha,

Goal state after:
case neg
R : Type u
inst✝¹ : Semiring R
inst✝ : StarRing R
a : R
ha : ¬IsUnit a
⊢ (star a)⁻¹ʳ = star 0
Module: Mathlib.Algebra.Star.Module

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁷ : Semiring R
inst✝⁶ : StarMul R
inst✝⁵ : TrivialStar R
inst✝⁴ : AddCommGroup A
inst✝³ : Module R A
inst✝² : StarAddMonoid A
inst✝¹ : StarModule R A
inst✝ : Invertible 2
r : R
x : A
⊢ ⟨⅟2 • (r • x + star (r • x)), ⋯⟩ = (RingHom.id R) r • ⟨⅟2 • (x + star x), ⋯⟩

Tactic:
ext
    simp [← mul_smul, show ⅟2 * r = r * ⅟2 from Commute.invOf_left <| (2 : ℕ).cast_commute r]

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

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

Tactic:
rw [updateCol_self, Pi.single_eq_of_ne hjk]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : DecidableEq n
inst✝ : Mul α
u : m → α
v : n → α
j : n
a : α
⊢ vecMulVec u (Function.update v j a) = (vecMulVec u v).updateCol j (MulOpposite.op a • u)

Tactic:
ext i j'
  obtain rfl | hi := eq_or_ne j' j
  · simp [vecMulVec_apply]
  · simp [vecMulVec_apply, hi]

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

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝² : DecidableEq o
R : Type u_14
inst✝¹ : Zero α
inst✝ : SMulZeroClass R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (x • M) = x • blockDiagonal' M

Tactic:
ext
  simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]
  split_ifs <;> simp

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

Goal state before:
pp: α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 2
⊢ 1 i j = !![1, 0; 0, 1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 2
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0; 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : Zero α
inst✝ : One α
i j : Fin 3
⊢ 1 i j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨0, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨1, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type u
inst✝¹ : Zero α
inst✝ : One α
j : Fin 3
⊢ 1 ((fun i ↦ i) ⟨2, ⋯⟩) j = !![1, 0, 0; 0, 1, 0; 0, 0, 1] ((fun i ↦ i) ⟨2, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 2
⊢ ↑n i j = !![↑n, 0; 0, ↑n] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 2
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0; 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
i j : Fin 3
⊢ ↑n i j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨0, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨1, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type u
inst✝ : AddMonoidWithOne α
n : ℕ
j : Fin 3
⊢ ↑n ((fun i ↦ i) ⟨2, ⋯⟩) j = !![↑n, 0, 0; 0, ↑n, 0; 0, 0, ↑n] ((fun i ↦ i) ⟨2, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
A : Matrix (Fin 2) (Fin 2) α
i j : Fin 2
⊢ A i j = !![A 0 0, A 0 1; A 1 0, A 1 1] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
A : Matrix (Fin 2) (Fin 2) α
j : Fin 2
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1; A 1 0, A 1 1] ((fun i ↦ i) ⟨1, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
A : Matrix (Fin 3) (Fin 3) α
i j : Fin 3
⊢ A i j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨0, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨0, ⋯⟩) j

case «1»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨1, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨1, ⋯⟩) j

case «2»
α : Type u
A : Matrix (Fin 3) (Fin 3) α
j : Fin 3
⊢ A ((fun i ↦ i) ⟨2, ⋯⟩) j = !![A 0 0, A 0 1, A 0 2; A 1 0, A 1 1, A 1 2; A 2 0, A 2 1, A 2 2] ((fun i ↦ i) ⟨2, ⋯⟩) j
Module: Mathlib.LinearAlgebra.Matrix.Notation

Goal state before:
pp: α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
i j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) i j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] i j

Tactic:
fin_cases i

Goal state after:
case «0»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨0, ⋯⟩) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨0, ⋯⟩)
      j

case «1»
α : Type u
inst✝¹ : AddCommMonoid α
inst✝ : Mul α
a₁₁ a₁₂ a₂₁ a₂₂ b₁₁ b₁₂ b₂₁ b₂₂ : α
j : Fin 2
⊢ (!![a₁₁, a₁₂; a₂₁, a₂₂] * !![b₁₁, b₁₂; b₂₁, b₂₂]) ((fun i ↦ i) ⟨1, ⋯⟩) j =
    !![a₁₁ * b₁₁ + a₁₂ * b₂₁, a₁₁ * b₁₂ + a₁₂ * b₂₂; a₂₁ * b₁₁ + a₂₂ * b₂₁, a₂₁ * b₁₂ + a₂₂ * b₂₂] ((fun i ↦ i) ⟨1, ⋯⟩)
      j