mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ≤ #(α →₀ β)

Tactic:
← lift_id #(α →₀ β),

Goal state after:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.SetTheory.Cardinal.Finsupp

Goal state before:
pp: case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≤ #(α →₀ β)

Tactic:
← lift_id #(α →₀ β),

Goal state after:
case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = uβ (iUnionLift S f hf (iUnion S) ⋯ x)

Tactic:
rw [iUnionLift_of_mem x hi, ← h i]

Goal state after:
α : Type u_1
ι : Sort u_2
β : Sort u_3
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⟩
ui : (i : ι) → ↑(S i) → ↑(S i)
uβ : β → β
h : ∀ (i : ι) (x : ↑(S i)), f i (ui i x) = uβ (f i x)
u : ↑(iUnion S) → ↑(iUnion S)
hui : ∀ (i : ι) (x : ↑(S i)), u (inclusion ⋯ x) = inclusion ⋯ (ui i x)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
⊢ iUnionLift S f hf (iUnion S) ⋯ (u x) = f i (ui i ⟨↑x, hi⟩)
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: ι : Type u_3
m n : ι →₀ ℕ
h : m < n
⊢ toMultiset m < toMultiset n

Tactic:
exact toMultiset_strictMono h

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

Goal state before:
pp: R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
I : Ideal A
⊢ Codisjoint 1 (Submodule.restrictScalars (↥S) I) ↔ Codisjoint (toSubmodule S) (Submodule.restrictScalars R I)

Tactic:
simp [← Submodule.codisjoint_restrictScalars_iff R]

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

Goal state before:
pp: case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
⊢ ↑x = ↑(if j = j then x else 0)

Tactic:
if_pos rfl

Goal state after:
case inl
ι : Type v
M : Type u_1
S : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid M
inst✝¹ : SetLike S M
inst✝ : AddSubmonoidClass S M
A : ι → S
j : ι
x : ↥(A j)
⊢ ↑x = ↑x
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b : S
⊢ a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
⟨m, hm, ha⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
⊢ b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a * b ∈ {x | ∃ m ∈ M, m * x ∈ s}
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b : S
⊢ a ∈ {x | ∃ m ∈ M, m * x ∈ s} → b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}

Tactic:
⟨m, hm, ha⟩

Goal state after:
R : Type u_1
S : Type u_2
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s✝ : Subalgebra R S
M✝ : Submonoid S
H✝ : M✝ ≤ s✝.toSubmonoid
s : Subalgebra R S
M : Submonoid S
H : M ≤ s.toSubmonoid
a b m : S
hm : m ∈ M
ha : m * a ∈ s
⊢ b ∈ {x | ∃ m ∈ M, m * x ∈ s} → a + b ∈ {x | ∃ m ∈ M, m * x ∈ s}
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_1
F : Type u_1
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
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
a b : A
ha : a ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
hb : b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)
⊢ ∀ x ∈ ↑(NonUnitalSubsemiring.closure s), x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ hb
          · exact fun x (hx : x ∈ NonUnitalSubsemiring.closure s) y
              (hy : y ∈ NonUnitalSubsemiring.closure s) => Submodule.subset_span (mul_mem hy hx)
          · exact fun x _hx => (mul_zero x).symm ▸ Submodule.zero_mem _
          · exact fun x y _ _ hx hy z hz => (mul_add z x y).symm ▸ add_mem (hx z hz) (hy z hz)
          · exact fun r x _ hx y hy =>
              (mul_smul_comm r y x).symm ▸ SMulMemClass.smul_mem r (hx y hy)

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

Goal state before:
pp: case right
R : Type u
inst✝¹⁶ : CommSemiring R
S : Type ?u.6
inst✝¹⁵ : Semiring S
inst✝¹⁴ : Algebra R S
ι₁ : Type v₁
ι₂ : Type v₂
inst✝¹³ : DecidableEq ι₁
inst✝¹² : DecidableEq ι₂
M₁ : ι₁ → Type w₁
M₁' : Type w₁'
M₂ : ι₂ → Type w₂
M₂' : Type w₂'
inst✝¹¹ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝¹⁰ : AddCommMonoid M₁'
inst✝⁹ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝⁸ : AddCommMonoid M₂'
inst✝⁷ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝⁶ : Module R M₁'
inst✝⁵ : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝⁴ : Module R M₂'
inst✝³ : (i₁ : ι₁) → Module S (M₁ i₁)
inst✝² : ∀ (i₁ : ι₁), IsScalarTower R S (M₁ i₁)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
⊢ (toModule S (ι₁ × ι₂) ((⨁ (i₁ : ι₁), M₁ i₁) ⊗[R] ⨁ (i₂ : ι₂), M₂ i₂) fun i ↦
        AlgebraTensorModule.map (lof S ι₁ M₁ i.1) (lof R ι₂ M₂ i.2)) ∘ₗ
      AlgebraTensorModule.lift
        (toModule S ι₁ ((⨁ (i₂ : ι₂), M₂ i₂) →ₗ[R] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₁ ↦
          (toModule R ι₂ (M₁ i₁ →ₗ[S] ⨁ (i : ι₁ × ι₂), M₁ i.1 ⊗[R] M₂ i.2) fun i₂ ↦
              (AlgebraTensorModule.curry (lof S (ι₁ × ι₂) (fun i ↦ M₁ i.1 ⊗[R] M₂ i.2) (i₁, i₂))).flip).flip) =
    LinearMap.id

Tactic:
ext i₁ i₂ x₁ x₂ : 5
    simp only [coe_comp, Function.comp_apply, AlgebraTensorModule.curry_apply, curry_apply,
      coe_restrictScalars, AlgebraTensorModule.lift_apply, lift.tmul, toModule_lof, flip_apply,
      AlgebraTensorModule.map_tmul, id_coe, id_eq]

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 j : ι₁
n : M₁ j
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

Tactic:
by_cases hj : j = i

Goal state after:
case pos
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 j : ι₁
n : M₁ j
hj : j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n

case neg
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 j : ι₁
n : M₁ j
hj : ¬j = i
⊢ ((component S ι₁ (fun i ↦ M₁ i ⊗[R] M₂') i ∘ₗ
          ↑(directSumLeft R S M₁ M₂') ∘ₗ (AlgebraTensorModule.mk R S (⨁ (i : ι₁), M₁ i) M₂').flip n✝) ∘ₗ
        lof S ι₁ M₁ j)
      n =
    (((AlgebraTensorModule.mk R S (M₁ i) M₂').flip n✝ ∘ₗ component S ι₁ M₁ i) ∘ₗ lof S ι₁ M₁ j) n
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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i) ∘ₗ lof R ι₂ M₂ j) n

Tactic:
by_cases hj : j = i

Goal state after:
case pos
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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
hj : j = i
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i) ∘ₗ lof R ι₂ M₂ j) n

case neg
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✝⁵ : AddCommMonoid M₁'
inst✝⁴ : (i₂ : ι₂) → AddCommMonoid (M₂ i₂)
inst✝³ : Module R M₁'
inst✝² : (i₂ : ι₂) → Module R (M₂ i₂)
inst✝¹ : Module S M₁'
inst✝ : IsScalarTower R S M₁'
m : M₁'
n✝ : ⨁ (i : ι₂), M₂ i
i j : ι₂
n : M₂ j
hj : ¬j = i
⊢ ((↑R (component S ι₂ (fun i ↦ M₁' ⊗[R] M₂ i) i) ∘ₗ
          ↑R ↑(directSumRight R S M₁' M₂) ∘ₗ (mk R M₁' (⨁ (i : ι₂), M₂ i)) m) ∘ₗ
        lof R ι₂ M₂ j)
      n =
    (((mk R M₁' (M₂ i)) m ∘ₗ component R ι₂ M₂ i) ∘ₗ lof R ι₂ M₂ j) n
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
S : Type v
f : R → S
inst✝³ : Star R
inst✝² : Mul R
inst✝¹ : Mul S
inst✝ : StarMul S
hf : Injective f
star : ∀ (x : R), f (Star.star x) = Star.star (f x)
mul : ∀ (x y : R), f (x * y) = f x * f y
x y : R
⊢ f (Star.star (x * y)) = f (Star.star y * Star.star x)

Tactic:
rw [star, mul, star_mul, mul, star, star]

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

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ b j = if i = i then b j else M i j

Tactic:
if_pos rfl

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
b : n → α
inst✝ : DecidableEq m
i' : m
h : i' = i
⊢ b j = b j
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ c i = if j = j then c i else M i j

Tactic:
if_pos rfl

Goal state after:
case pos
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
i : m
j : n
c : m → α
inst✝ : DecidableEq n
j' : n
h : j' = j
⊢ c i = c i
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
inst✝² : DecidableEq o
α : Type u_14
inst✝¹ : AddMonoid α
inst✝ : StarAddMonoid α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᴴ = blockDiagonal' fun k ↦ (M k)ᴴ

Tactic:
by
  simp only [conjTranspose, blockDiagonal'_transpose]
  exact blockDiagonal'_map _ star (star_zero α)

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, ⋯⟩
⊢ R ∙ generator (span R {a, ψ ⟨y, ⋯⟩}) = R ∙ generator (ϕ.submoduleImage N)

Tactic:
let ψ' : O →ₗ[R] R := r₁ • ϕ + r₂ • ψ

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

Goal state before:
pp: ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))

Tactic:
have ϕ_max := this.choose_spec

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsPrincipalIdealRing R
inst✝³ : IsDomain R
inst✝² : Finite ι
O : Type u_4
inst✝¹ : AddCommGroup O
inst✝ : Module R O
M N : Submodule R O
b'M : Basis ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
this : ∃ ϕ, ∀ (ψ : ↥M →ₗ[R] R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
ϕ : ↥M →ₗ[R] R := this.choose
ϕ_max : ∀ (ψ : ↥M →ₗ[R] R), ¬this.choose.submoduleImage N < ψ.submoduleImage N
⊢ ∃ y ∈ M,
    ∃ a,
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis (Fin n') R ↥N'),
                    ∃ bN,
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1),
                          ∃ bM,
                            ∀ (as : Fin n' → R),
                              (∀ (i : Fin n'), ↑(bN' i) = as i • ↑(bM' (Fin.castLE hn'm' i))) →
                                ∃ as', ∀ (i : Fin (n' + 1)), ↑(bN i) = as' i • ↑(bM (Fin.castLE hnm i))
Module: Mathlib.LinearAlgebra.TensorProduct.Tower

Goal state before:
pp: R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
e : M ≃ₗ[R] N
⊢ LinearEquiv.baseChange R A N M e.symm = (LinearEquiv.baseChange R A M N e).symm

Tactic:
ext x
  rw [LinearEquiv.eq_symm_apply]
  simp [← LinearEquiv.coe_toLinearMap, LinearEquiv.coe_baseChange,
    baseChange_eq_ltensor, ← lTensor_comp_apply]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
rb sb : R
hb : sb * ↑s₁ = rb * ↑s₂
h : sb * ↑s₁ ∈ S
⊢ add'' r₁ s₁ r₂ s₂ = (sb • r₁ + rb • r₂) /ₒ ⟨sb * ↑s₁, h⟩

Tactic:
by
  simp only [add'']
  have ha := ore_eq (s₁ : R) s₂
  generalize oreNum (s₁ : R) s₂ = ra at *
  generalize oreDenom (s₁ : R) s₂ = sa at *
  rw [oreDiv_eq_iff]
  rcases oreCondition sb sa with ⟨rc, sc, hc⟩
  have : sc * rb * s₂ = rc * ra * s₂ := by
    rw [mul_assoc rc, ← ha, ← mul_assoc, ← hc, mul_assoc, mul_assoc, hb]
  rcases ore_right_cancel _ _ s₂ this with ⟨sd, hd⟩
  use sd * sc
  use sd * rc
  simp only [smul_add, smul_smul, Submonoid.smul_def, Submonoid.coe_mul]
  constructor
  · rw [mul_assoc _ _ rb, hd, mul_assoc, hc, mul_assoc, mul_assoc]
  · rw [mul_assoc, ← mul_assoc (sc : R), hc, mul_assoc, mul_assoc]

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

Goal state before:
pp: R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = add'' r₁ s₁ r₂ s₂

Tactic:
have : sd * sb * s₁ = rd * rc * s₂ := by
      rw [mul_assoc, hb', ← mul_assoc, hd, mul_assoc, hc, ← mul_assoc]

Goal state after:
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddMonoid X
inst✝ : DistribMulAction R X
r₂ : X
s₂ : ↥S
r₁' : X
s₁' : ↥S
r₁ : X
s₁ sb : ↥S
rb : R
hb : sb • r₁ = rb • r₁'
hb' : ↑sb * ↑s₁ = rb * ↑s₁'
rc : R
sc : ↥S
hc : ↑sc * ↑s₁' = rc * ↑s₂
rd : R
sd : ↥S
hd : ↑sd * rb = rd * ↑sc
this : ↑sd * ↑sb * ↑s₁ = rd * rc * ↑s₂
⊢ (↑sc • r₁' + rc • r₂) /ₒ ⟨↑sc * ↑s₁', ⋯⟩ = add'' r₁ s₁ r₂ s₂
Module: Mathlib.Algebra.Field.Subfield.Basic

Goal state before:
pp: K : Type u
inst✝ : DivisionRing K
s : Set K
p : (x : K) → x ∈ closure s → Prop
mem : ∀ (x : K) (hx : x ∈ s), p x ⋯
one : p 1 ⋯
add : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x + y) ⋯
neg : ∀ (x : K) (hx : x ∈ closure s), p x hx → p (-x) ⋯
inv : ∀ (x : K) (hx : x ∈ closure s), p x hx → p x⁻¹ ⋯
mul : ∀ (x y : K) (hx : x ∈ closure s) (hy : y ∈ closure s), p x hx → p y hy → p (x * y) ⋯
x : K
h : x ∈ closure s
a✝ b✝ : K
w✝¹ : a✝ ∈ closure s
hx : p a✝ w✝¹
w✝ : b✝ ∈ closure s
hy : p b✝ w✝
⊢ a✝ + b✝ ∈ {x | ∃ (hx : x ∈ closure s), p x hx}

Tactic:
exact ⟨_, add _ _ _ _ hx hy⟩

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

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

Tactic:
by
      rw [← Matrix.toLinearMapRight'_mul_apply, hM'M, Matrix.toLinearMapRight'_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_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
x✝¹ : n → R
x✝ : m
⊢ Mᵀ.vecMulLinear x✝¹ x✝ = M.mulVecLin x✝¹ x✝

Tactic:
simp [vecMul_transpose]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
m : Type u_3
inst✝¹ : Fintype m
inst✝ : DecidableEq m
b : Basis m R S
x x' : S
h : (leftMulMatrix b) x = (leftMulMatrix b) x'
⊢ ((lmul R S) x) 1 = ((lmul R S) x') 1

Tactic:
rw [(LinearMap.toMatrix b b).injective h]

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
n : ℕ
N : Submodule R M
snf : SmithNormalForm N ι n
i : Fin n
c : Fin n →₀ R
hm : (c.sum fun i x ↦ x • ↑(snf.bN i)) ∈ N
⊢ ↑⟨c.sum fun i t ↦ t • ↑(snf.bN i), hm⟩ = N.subtype (c.sum fun i t ↦ t • ⟨↑(snf.bN i), ⋯⟩)

Tactic:
simp [map_finsuppSum]

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
b✝ : ι → 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 : Basis (Fin o) R ↥O
bN : Basis (Fin n) R ↥N
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
⊢ (o : ℕ) × (n : ℕ) × Basis.SmithNormalForm (comap O.subtype N) (Fin o) n

Tactic:
refine
    ⟨o, n, bO, bN.map (comapSubtypeEquivOfLe N_le_O).symm, (Fin.castLEEmb hno), a,
      fun i ↦ ?_⟩

Goal state after:
ι : Type u_1
R : Type u_2
inst✝⁵ : CommRing R
M : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
b✝ : ι → 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 : Basis (Fin o) R ↥O
bN : Basis (Fin n) R ↥N
a : Fin n → R
snf : ∀ (i : Fin n), ↑(bN i) = a i • ↑(bO (Fin.castLE hno i))
i : Fin n
⊢ ↑((bN.map (comapSubtypeEquivOfLe N_le_O).symm) i) = a i • bO ((Fin.castLEEmb hno) i)
Module: Mathlib.RingTheory.Localization.Basic

Goal state before:
pp: case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) → (algebraMap R S) x = (algebraMap R S) y

Tactic:
← h.symm.commutes,

Goal state after:
case exists_of_eq
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_3
inst✝² : CommSemiring P
inst✝¹ : Algebra R P
inst✝ : IsLocalization M S
h : S ≃ₐ[R] P
x y : R
⊢ h.symm.toEquiv ((algebraMap R P) x) = h.symm.toEquiv ((algebraMap R P) y) →
    h.symm ((algebraMap R P) x) = (algebraMap R S) y
Module: Mathlib.RingTheory.Localization.FractionRing

Goal state before:
pp: A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
⊢ Injective ⇑(ringEquivOfRingEquivHom A K)

Tactic:
intro f g h

Goal state after:
A : Type u_8
K : Type u_9
inst✝³ : CommRing A
inst✝² : CommRing K
inst✝¹ : Algebra A K
inst✝ : IsFractionRing A K
f g : A ≃+* A
h : (ringEquivOfRingEquivHom A K) f = (ringEquivOfRingEquivHom A K) g
⊢ f = g