mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Matrix.Basis

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hkj : k ≠ j
this : (single i j 1 * M) i k = (M * single i j 1) i k
⊢ M j k = 0

Tactic:
simp_all

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j k : n
M : Matrix n n α
hM : Commute (single i j 1) M
hki : k ≠ i
this : (single i j 1 * M) k j = (M * single i j 1) k j
⊢ M k i = 0

Tactic:
simp_all

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

Goal state before:
pp: n : Type u_3
α : Type u_7
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : Semiring α
i j : n
M : Matrix n n α
hM : Commute (single i j 1) M
this : (single i j 1 * M) i j = (M * single i j 1) i j
⊢ M i i = M j j

Tactic:
simp_all

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(Multiset α) = max #α ℵ₀

Tactic:
classical
  exact Multiset.toFinsupp.toEquiv.cardinal_eq.trans (mk_finsupp_nat α)

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
⊢ toFinsupp {a} = Finsupp.single a 1

Tactic:
ext; rw [toFinsupp_apply, count_singleton, Finsupp.single_eq_pi_single, Pi.single_apply]

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
inst✝² : Semiring S
inst✝¹ : Algebra R S
inst✝ : Free R S
⊢ Nonempty (R ≃ₐ[R] S) ↔ finrank R S = 1

Tactic:
rw [← nonempty_linearEquiv_iff_finrank_eq_one]
  exact ⟨fun ⟨e⟩ ↦ ⟨e⟩, fun ⟨e⟩ ↦
    ⟨.ofBijective (Algebra.ofId R S) (bijective_algebraMap_of_linearEquiv e)⟩⟩

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

Goal state before:
pp: 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
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ * y) = f (x * z)

Tactic:
simp_all

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

Goal state before:
pp: 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
w✝ : R
⊢ ∀ {x y z : R}, f w✝ = f x → f y = f z → f (w✝ + y) = f (x + z)

Tactic:
simp_all

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

Goal state before:
pp: ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ (of (fun x ↦ M) p) ((toAddMonoid fun x ↦ AddMonoidHom.id M) ((of (fun i ↦ M) p) x)) = (of (fun i ↦ M) p) x

Tactic:
toAddMonoid_of,

Goal state after:
ι✝ : Type v
β : ι✝ → Type w
inst✝² : (i : ι✝) → AddCommMonoid (β i)
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ : ⨁ (x : ι), M
p : ι
x : M
⊢ (of (fun x ↦ M) p) ((AddMonoidHom.id M) x) = (of (fun i ↦ M) p) x
Module: Mathlib.LinearAlgebra.TensorProduct.Associator

Goal state before:
pp: case add
R : Type u_11
A : Type u_12
A' : Type u_13
B : Type u_14
B' : Type u_15
C : Type u_16
C' : Type u_17
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid A'
inst✝⁴ : AddCommMonoid B'
inst✝³ : AddCommMonoid C'
inst✝² : Module R A'
inst✝¹ : Module R B'
inst✝ : Module R C'
eA : A ≃ A'
eB : B ≃ B'
eC : C ≃ C'
x✝ y✝ : A ⊗[R] B ⊗[R] C
a✝¹ :
  (TensorProduct.assoc R A B C) x✝ =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      x✝
a✝ :
  (TensorProduct.assoc R A B C) y✝ =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      y✝
⊢ (TensorProduct.assoc R A B C) (x✝ + y✝) =
    (TensorProduct.congr (TensorProduct.congr (linearEquiv R eA) (linearEquiv R eB)) (linearEquiv R eC) ≪≫ₗ
        (TensorProduct.assoc R A' B' C' ≪≫ₗ
          TensorProduct.congr (linearEquiv R eA).symm
            (TensorProduct.congr (linearEquiv R eB).symm (linearEquiv R eC).symm)))
      (x✝ + y✝)

Tactic:
| add =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
⊢ ((equivFinsuppOfBasisRight 𝒞) 0) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) 0)

Tactic:
simp_all

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

Goal state before:
pp: case tmul
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ ⊗ₜ[R] y✝))

Tactic:
simp_all

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

Goal state before:
pp: case add
R : Type u_1
M : Type u_3
N : Type u_4
κ : Type u_6
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq κ
𝒞 : Basis κ R N
i : κ
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisRight 𝒞) x✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisRight 𝒞) y✝) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) y✝)
⊢ ((equivFinsuppOfBasisRight 𝒞) (x✝ + y✝)) i = (TensorProduct.rid R M) ((lTensor M (𝒞.coord i)) (x✝ + y✝))

Tactic:
simp_all

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

Goal state before:
pp: case zero
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
i : ι
⊢ ((equivFinsuppOfBasisLeft ℬ) 0) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) 0)

Tactic:
simp_all

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

Goal state before:
pp: case tmul
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
i : ι
x✝ : M
y✝ : N
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ ⊗ₜ[R] y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ ⊗ₜ[R] y✝))

Tactic:
simp_all

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

Goal state before:
pp: case add
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
i : ι
x✝ y✝ : M ⊗[R] N
a✝¹ : ((equivFinsuppOfBasisLeft ℬ) x✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) x✝)
a✝ : ((equivFinsuppOfBasisLeft ℬ) y✝) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) y✝)
⊢ ((equivFinsuppOfBasisLeft ℬ) (x✝ + y✝)) i = (TensorProduct.lid R N) ((rTensor N (ℬ.coord i)) (x✝ + y✝))

Tactic:
simp_all

Goal state after:
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
ℬ : Basis ι R M
x : M ⊗[R] N
⊢ ∃ c, (c.sum fun i n ↦ ℬ i ⊗ₜ[R] n) = x

Tactic:
classical obtain ⟨c, rfl⟩ := (TensorProduct.equivFinsuppOfBasisLeft ℬ).symm.surjective x
  exact ⟨c, (TensorProduct.comm R M N).injective <| by simp [Finsupp.sum]⟩

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

Goal state before:
pp: case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ (if i' = i ∧ k' = k then m ⊗ₜ[R] n else 0) = (if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0

Tactic:
ite_and

Goal state after:
case single.single
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ (if i' = i then if k' = k then m ⊗ₜ[R] n else 0 else 0) = (if i' = i then m else 0) ⊗ₜ[R] if k' = k then n else 0
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_14
inst✝¹ : Zero R
inst✝ : DecidableEq m
d : m → Matrix n n R
⊢ (comp m m n n R) (diagonal d) = (reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (blockDiagonal d)

Tactic:
by
  ext
  simp [diagonal, blockDiagonal, Matrix.ite_apply]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I = Ideal.span {x}

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
I : Ideal R
inst✝ : Submodule.IsPrincipal I
x : R
hx : x ∈ I
⊢ x ∣ generator I ↔ I ≤ Ideal.span {x} ∧ Ideal.span {x} ≤ I
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inl
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
x : M
hx : x ∈ {p | p ∈ Submonoid.closure S ∧ Irreducible p}
b : M
x✝¹ : b ∈ Submonoid.closure S
hb : Irreducible b → b ∈ S
x✝ : 1 ∈ Submonoid.closure S
ha : Irreducible 1 → 1 ∈ S
h : Irreducible (1 * b)
⊢ 1 * b ∈ S

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.AffineMonoid.Irreducible

Goal state before:
pp: case inr
M : Type u_1
inst✝¹ : CommMonoid M
inst✝ : Subsingleton Mˣ
S : Set M
x : M
hx : x ∈ {p | p ∈ Submonoid.closure S ∧ Irreducible p}
a : M
x✝¹ : a ∈ Submonoid.closure S
ha : Irreducible a → a ∈ S
x✝ : 1 ∈ Submonoid.closure S
hb : Irreducible 1 → 1 ∈ S
h : Irreducible (a * 1)
⊢ a * 1 ∈ S

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module A N
f : A ⊗[R] M →ₗ[A] N
⊢ LinearMap.baseChange A f ∘ₗ ↑(cancelBaseChange R A A A M).symm = ↑(TensorProduct.lid A N).symm ∘ₗ f

Tactic:
by
  rw [cancelBaseChange_self_eq_lid]
  ext x
  simp

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

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ 0 * (r /ₒ s) = 0

Tactic:
| _ r s
     => 

Goal state after:
case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ 0 * (r /ₒ s) = 0
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 0 = 0

Tactic:
| _ r s
     => 

Goal state after:
case c
R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
⊢ r /ₒ s * 0 = 0
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
S : Set (Subfield K)
⊢ ∀ x ∈ (sInf (toSubring '' S)).carrier, x⁻¹ ∈ (sInf (toSubring '' S)).carrier

Tactic:
by
        rintro x hx
        apply Subring.mem_sInf.mpr
        rintro _ ⟨p, p_mem, rfl⟩
        exact p.inv_mem (Subring.mem_sInf.mp hx p.toSubring ⟨p, p_mem, rfl⟩)

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommSemiring R
k : Type u_2
l : Type u_3
m : Type u_4
n : Type u_5
inst✝³ : DecidableEq n
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : DecidableEq m
M : Matrix m n R
M' : Matrix n m R
hMM' : M * M' = 1
hM'M : M' * M = 1
x : n → R
⊢ (toLin' M') ((toLin' M) x) = x

Tactic:
by
      rw [← Matrix.toLin'_mul_apply, hM'M, Matrix.toLin'_one, id_apply]

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

Goal state before:
pp: R : Type u_1
inst✝⁷ : CommSemiring R
m : Type u_3
n : Type u_4
inst✝⁶ : Fintype n
inst✝⁵ : Finite m
inst✝⁴ : DecidableEq n
M₁ : Type u_5
M₂ : Type u_6
inst✝³ : AddCommMonoid M₁
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M₁
inst✝ : Module R M₂
v₁ : Basis n R M₁
v₂ : Basis m R M₂
f : M₁ →ₗ[R] M₂
⊢ (toLin v₁ v₂) ((toMatrix v₁ v₂) f) = f

Tactic:
by
  rw [← Matrix.toLin_symm, LinearEquiv.apply_symm_apply]

Goal state after:
Module: Mathlib.RingTheory.OreLocalization.Ring

Goal state before:
pp: case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ f r₃ * f ↑s₂ = ↑(fS ⟨r₃ * ↑s₂, ⋯⟩)

Tactic:
← hf

Goal state after:
case c.c.e_a.e_a
R : Type u_1
inst✝⁴ : Semiring R
S : Submonoid R
inst✝³ : OreSet S
X : Type u_2
inst✝² : AddCommMonoid X
inst✝¹ : Module R X
T : Type u_3
inst✝ : Semiring T
f : R →+* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : R
s₃ : ↥S
h₃ : ↑(s₃ * s₁) = r₃ * ↑s₂
h₃' : s₃ * s₁ = ⟨r₃ * ↑s₂, ⋯⟩
⊢ f r₃ * f ↑s₂ = f ↑⟨r₃ * ↑s₂, ⋯⟩
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ ∑ j, (if ij.1 = j ∧ ij.2 = k then 1 else 0) • b₂ j = if ij.2 = k then b₂ ij.1 else 0

Tactic:
ite_smul,

Goal state after:
R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (∑ x, if ij.1 = x ∧ ij.2 = k then 1 • b₂ x else 0 • b₂ x) = if ij.2 = k then b₂ ij.1 else 0
Module: Mathlib.LinearAlgebra.Matrix.ToLin

Goal state before:
pp: R : Type u_1
M₁ : Type u_3
M₂ : Type u_4
ι₁ : Type u_6
ι₂ : Type u_7
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M₁
inst✝³ : Module R M₂
inst✝² : Fintype ι₁
inst✝¹ : Fintype ι₂
inst✝ : DecidableEq ι₁
b₁ : Basis ι₁ R M₁
b₂ : Basis ι₂ R M₂
ij : ι₂ × ι₁
k : ι₁
this : DecidableEq ι₂
⊢ (if True then if ij.2 = k then b₂ ij.1 else 0 else 0) = if ij.2 = k then b₂ ij.1 else 0

Tactic:
if_true

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : IsDomain R
inst✝¹ : IsPrincipalIdealRing R
inst✝ : Finite ι
b : Basis ι R M
N O : Submodule R M
N_le_O : N ≤ O
⊢ ∃ n o, ∃ (hno : n ≤ o), ∃ bO bN a, ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))

Tactic:
cases nonempty_fintype ι
  induction O using inductionOnRank b generalizing N with | ih M0 ih =>
  obtain ⟨m, b'M⟩ := M0.basisOfPid b
  by_cases N_bot : N = ⊥
  · subst N_bot
    exact ⟨0, m, Nat.zero_le _, b'M, Basis.empty _, finZeroElim, finZeroElim⟩
  obtain ⟨y, hy, a, _, M', M'_le_M, N', _, N'_le_M', y_ortho, _, h⟩ :=
    Submodule.basis_of_pid_aux M0 N b'M N_bot N_le_O
  obtain ⟨n', m', hn'm', bM', bN', as', has'⟩ := ih M' M'_le_M y hy y_ortho N' N'_le_M'
  obtain ⟨bN, h'⟩ := h n' bN'
  obtain ⟨hmn, bM, h''⟩ := h' m' hn'm' bM'
  obtain ⟨as, has⟩ := h'' as' has'
  exact ⟨_, _, hmn, bM, bN, as, has⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : FaithfulSMul R K
surj : ∀ (z : K), ∃ x y, z = (algebraMap R K) x / (algebraMap R K) y
inj : Function.Injective ⇑(algebraMap R K)
this✝ : NoZeroDivisors R
this : Nontrivial R
z : K
⊢ ∃ x, z * (algebraMap R K) ↑x.2 = (algebraMap R K) x.1

Tactic:
by
    have ⟨x, y, eq⟩ := surj z
    obtain rfl | hy := eq_or_ne y 0
    · obtain rfl : z = 0 := by simpa using eq
      exact ⟨(0, 1), by simp⟩
    exact ⟨⟨x, y, mem_nonZeroDivisors_iff_ne_zero.mpr hy⟩,
      (eq_div_iff_mul_eq <| (map_ne_zero_iff _ inj).mpr hy).mp eq⟩

Goal state after:
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
⊢ R⁰ = IsUnit.submonoid R ↔ R⁰ ≤ IsUnit.submonoid R

Tactic:
le_antisymm_iff,

Goal state after:
R : Type u_1
inst✝ : CommRing R
⊢ R⁰ ≤ IsUnit.submonoid R ∧ IsUnit.submonoid R ≤ R⁰ ↔ R⁰ ≤ IsUnit.submonoid R
Module: Mathlib.RingTheory.Adjoin.Basic

Goal state before:
pp: case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a) • r ^ n₁ a • (algebraMap R A) (l a) • ↑a ∈ Subalgebra.toSubmodule B'

Tactic:
smul_smul (r ^ n₁ a),

Goal state after:
case h
R : Type uR
A : Type uA
B : Type uB
inst✝⁶ : CommSemiring R
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
inst✝³ : CommSemiring B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsScalarTower R A B
r : A
s : Set B
B' : Subalgebra R B
hs : r • s ⊆ ↑B'
hr : (algebraMap A B) r ∈ B'
l : ↑↑(Submonoid.closure s) →₀ R
n₁ : ↥(Submonoid.closure s) → ℕ
n₂ : ∀ (x : ↥(Submonoid.closure s)), r ^ n₁ x • ↑x ∈ Submonoid.closure (r • s)
n : ℕ
hn : n ≥ l.support.sup n₁
a : ↑↑(Submonoid.closure s)
ha : a ∈ l.support
this : n ≥ n₁ a
⊢ r ^ (n - n₁ a) • (r ^ n₁ a * (algebraMap R A) (l a)) • ↑a ∈ Subalgebra.toSubmodule B'
Module: Mathlib.Algebra.Star.StarProjection

Goal state before:
pp: R : Type u_1
inst✝² : NonUnitalRing R
inst✝¹ : StarRing R
inst✝ : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p = p * q ∧ p = p * q ↔ p = p * q

Tactic:
and_self

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

Goal state before:
pp: case add
R : Type uR
A : Type uA
B : Type uB
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
C : Type u_3
inst✝ : Semiring C
f g : A ⊗[R] B →+* C
h₁ : f.comp includeLeftRingHom = g.comp includeLeftRingHom
h₂ : f.comp includeRight.toRingHom = g.comp includeRight.toRingHom
x y : A ⊗[R] B
a✝¹ : f x = g x
a✝ : f y = g y
⊢ f (x + y) = g (x + y)

Tactic:
simp_all

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

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (↑r • 1 - ↑a)
⊢ IsUnit (↑r⁻¹ • 1 - ↑a⁻¹)

Tactic:
← Units.smul_def

Goal state after:
R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : Rˣ
a : Aˣ
h : IsUnit (r • 1 - ↑a)
⊢ IsUnit (r⁻¹ • 1 - ↑a⁻¹)
Module: Mathlib.Algebra.Algebra.Spectrum.Pi

Goal state before:
pp: A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ {r | IsUnit ((algebraMap R (A × B)) r - (a, b))} =
    {r | IsUnit ((algebraMap R A) r - a)} ∩ {r | IsUnit ((algebraMap R B) r - b)}

Tactic:
← Set.ofPred_and,

Goal state after:
A : Type u_2
B : Type u_3
R : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Ring A
inst✝² : Ring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
a : A
b : B
⊢ {r | IsUnit ((algebraMap R (A × B)) r - (a, b))} =
    {a_1 | IsUnit ((algebraMap R A) a_1 - a) ∧ IsUnit ((algebraMap R B) a_1 - b)}
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
⊢ b j ∈ centralizer R S

Tactic:
rw [Subalgebra.mem_centralizer_iff]

Goal state after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
⊢ ∀ g ∈ S, g * b j = b j * g
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ x * b j = b j * x

Tactic:
suffices x • b = b.mapRange (· * x) (by simp) from Finsupp.ext_iff.1 this j

Goal state after:
case mp
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
ℬ : Module.Basis (Module.Free.ChooseBasisIndex R B) R B := Module.Free.chooseBasis R B
b : Module.Free.ChooseBasisIndex R B →₀ A
hw : ∀ g ∈ ⇑includeLeft '' S, (g * b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) = (b.sum fun i m ↦ m ⊗ₜ[R] ℬ i) * g
j : Module.Free.ChooseBasisIndex R B
hj : j ∈ b.support
x : A
hx : x ∈ S
⊢ x • b = mapRange (fun x_1 ↦ x_1 * x) ⋯ b
Module: Mathlib.Algebra.Algebra.Subalgebra.Centralizer

Goal state before:
pp: case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
⊢ (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w ∈ centralizer R (⇑includeLeft '' S)

Tactic:
rw [Subalgebra.mem_centralizer_iff]

Goal state after:
case mpr
R : Type u_1
inst✝⁵ : CommSemiring R
A : Type u_2
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
B : Type u_3
inst✝² : Semiring B
inst✝¹ : Algebra R B
S : Set A
inst✝ : Module.Free R B
w : ↥(centralizer R S) ⊗[R] B
⊢ ∀ g ∈ ⇑includeLeft '' S,
    g * (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w =
      (Algebra.TensorProduct.map (centralizer R S).val (AlgHom.id R B)).toRingHom w * g