mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.Dimension.StrongRankCondition

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Fintype ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

pp: case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'

Tactic:
· -- `v` is a finite basis, so by `basis_finite_of_finite_spans` so is `v'`.
    -- haveI : Finite (range v) := Set.finite_range v
    have := basis_finite_of_finite_spans (Set.finite_range v) v.span_eq v'
    cases nonempty_fintype ι'
    -- We clean up a little:
    rw [Cardinal.mk_fintype, Cardinal.mk_fintype]
    simp only [Cardinal.lift_natCast, Nat.cast_inj]
    -- Now we can use invariant basis number to show they have the same cardinality.
    apply card_eq_of_linearEquiv R
    exact
      (Finsupp.linearEquivFunOnFinite R R ι).symm.trans v.repr.symm ≪≫ₗ v'.repr ≪≫ₗ
        Finsupp.linearEquivFunOnFinite R R ι'

Goal state after:
case inr
R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type w
ι' : Type w'
inst✝ : InvariantBasisNumber R
v : Basis ι R M
v' : Basis ι' R M
this : Nontrivial R
val✝ : Infinite ι
⊢ lift.{w', w} #ι = lift.{w, w'} #ι'
Module: Mathlib.LinearAlgebra.Matrix.Defs

Goal state before:
pp: R : Type u_7
m n : ℕ
A : Matrix (Fin m) (Fin n) R
⊢ ofArray (Array.ofFn fun k ↦ A k.divNat k.modNat) ⋯ = A

Tactic:
ext i j
  rw [ofArray_apply, Fin.getElem_fin, Array.getElem_ofFn, Fin.divNat_mkDivMod,
    Fin.modNat_mkDivMod]

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype m
M : Matrix m n α
⊢ 0 * M = 0

Tactic:
by
  ext
  apply zero_dotProduct

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ A *ᵥ w = ∑ j, ∑ i, v i * A i j * w j

Tactic:
dotProduct_mulVec,

Goal state after:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ᵥ* A ⬝ᵥ w = ∑ j, ∑ i, v i * A i j * w j
Module: Mathlib.RingTheory.Ideal.Operations

Goal state before:
pp: R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ↑u = 1

Tactic:
isUnit_iff.mp u.isUnit,

Goal state after:
R : Type u
ι : Type u_1
inst✝ : CommSemiring R
I J K L : Ideal R
u : (Ideal R)ˣ
⊢ ⊤ = 1
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
⊢ (Finsupp.linearCombination R v) (Finsupp.mapRange Subtype.val ⋯ f) = f.sum fun i x ↦ ↑x • v i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_mapRange_index]

Goal state after:
ι : Type u_1
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
v : ι → M
f : ι →₀ ↥I
⊢ ∀ (a : ι), 0 • v a = 0
Module: Mathlib.LinearAlgebra.FreeModule.Finite.Basic

Goal state before:
pp: case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ Finite (ChooseBasisIndex R M)

Tactic:
ChooseBasisIndex

Goal state after:
case inl
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ Finite ↑⋯.choose
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
⊢ (b.repr (b i • if j = j' then 1 else 0)) i' = (single (i, j) 1) (i', j')

Tactic:
split_ifs with hi

Goal state after:
case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ (b.repr (b i • 1)) i' = (single (i, j) 1) (i', j')

case neg
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : ¬j = j'
⊢ (b.repr (b i • 0)) i' = (single (i, j) 1) (i', j')
Module: Mathlib.RingTheory.AlgebraTower

Goal state before:
pp: case pos
R : Type u_1
S : Type u_2
A : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R S
inst✝² : Module S A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
ι : Type u_5
ι' : Type u_6
b : Basis ι R S
c : Basis ι' S A
i : ι
j : ι'
i' : ι
j' : ι'
hi : j = j'
⊢ (b.repr (b i • 1)) i' = (single (i, j) 1) (i', j')

Tactic:
simp [hi, Finsupp.single_apply]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
x : n → α
y : m → α
⊢ x ⬝ᵥ Aᵀ *ᵥ y = y ⬝ᵥ A *ᵥ x

Tactic:
dotProduct_mulVec,

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
inst✝² : NonUnitalCommSemiring α
inst✝¹ : Fintype m
inst✝ : Fintype n
A : Matrix m n α
x : n → α
y : m → α
⊢ x ᵥ* Aᵀ ⬝ᵥ y = y ⬝ᵥ A *ᵥ x
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: n : Type u_3
α : Type u_11
inst✝⁴ : DecidableEq n
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : Preorder α
inst✝ : ZeroLEOneClass α
i j : n
⊢ 0 ≤ 1 i j

Tactic:
by
  by_cases hi : i = j
  · subst hi
    simp
  · simp [hi]

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]

Goal state after:
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) ↔ Nonempty (R ≃ₗ[R] S)
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
h : ker f = ⊥
x : R
⊢ ∀ ⦃a₂ : R⦄, f x = f a₂ → x = a₂

Tactic:
y

Goal state after:
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
h : ker f = ⊥
x y : R
⊢ f x = f y → x = y
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: case mp.refine_1
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ I
⊢ x - y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

pp: case mp.refine_2
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ : R
s : TwoSidedIdeal R := mk' {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} ⋯ ⋯ ⋯ ⋯ ⋯
x y : R
h : x - y ∈ J
⊢ x - y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
exacts [⟨_, ⟨h, ⟨0, ⟨zero_mem _, add_zero _⟩⟩⟩⟩, ⟨0, ⟨zero_mem _, ⟨_, ⟨h, zero_add _⟩⟩⟩⟩]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ sSup (ringCon '' Set.range fun i ↦ I i) = sSup (Set.range fun i ↦ (I i).ringCon)

Tactic:
congr

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
⊢ (ringCon '' Set.range fun i ↦ I i) = Set.range fun i ↦ (I i).ringCon
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x : R
⊢ (∀ x_1 ∈ ringCon '' Set.range I, x_1 x 0) ↔ ∀ (i : ι), x ∈ I i

Tactic:
simp [mem_iff]

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
S : Set (TwoSidedIdeal R)
x : R
⊢ (∀ x_1 ∈ ringCon '' S, x_1 x 0) ↔ ∀ I ∈ S, x ∈ I

Tactic:
simp [mem_iff]

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

Goal state before:
pp: ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ f = (toAddMonoid fun i ↦ ψ.comp (of β i)) f

Tactic:
congr

Goal state after:
ι : Type v
β : ι → Type w
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : DecidableEq ι
γ : Type u₁
inst✝ : AddCommMonoid γ
ψ : (⨁ (i : ι), β i) →+ γ
f : ⨁ (i : ι), β i
⊢ ψ = toAddMonoid fun i ↦ ψ.comp (of β i)
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : Semiring B
inst✝² : Algebra R B
inst✝¹ : Semiring C
inst✝ : Algebra R C
toSubsemiring✝¹ : Subsemiring A
algebraMap_mem'✝¹ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝¹.carrier
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝¹, algebraMap_mem' := algebraMap_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }
⊢ toSubsemiring✝¹ = toSubsemiring✝
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: 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)
⊢ a * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ ha
        · 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)
        · exact (zero_mul b).symm ▸ Submodule.zero_mem _
        · exact fun x y _ _ => (add_mul x y b).symm ▸ add_mem
        · exact fun r x _ hx => (smul_mul_assoc r x b).symm ▸ SMulMemClass.smul_mem r hx

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

Goal state before:
pp: 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
φ₁ φ₂ : ↥(adjoin R s) →ₐ[R] B
h : ∀ (x : A) (hx : x ∈ s), φ₁ ⟨x, ⋯⟩ = φ₂ ⟨x, ⋯⟩
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
h₁ : φ₁ ⟨x✝³, x✝¹⟩ = φ₂ ⟨x✝³, x✝¹⟩
h₂ : φ₁ ⟨x✝², x✝⟩ = φ₂ ⟨x✝², x✝⟩
⊢ φ₁ ⟨x✝³ + x✝², ⋯⟩ = φ₂ ⟨x✝³ + x✝², ⋯⟩

Tactic:
by convert! congr_arg₂ (· + ·) h₁ h₂ <;> rw [← map_add] <;> rfl

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
⊢ map f (S ⊔ adjoin R (⇑f ⁻¹' {0})) ≤ map f S

Tactic:
Algebra.map_sup,

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
⊢ map f S ⊔ map f (adjoin R (⇑f ⁻¹' {0})) ≤ map f S
Module: Mathlib.Data.Matrix.Composition

Goal state before:
pp: case inr.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ single k l r k l = single (i, k) (j, l) r (i, k) (j, l)

Tactic:
single_apply_same,

Goal state after:
case inr.inr.inr.inr
I : Type u_1
J : Type u_2
K : Type u_3
L : Type u_4
R : Type u_5
inst✝⁴ : DecidableEq I
inst✝³ : DecidableEq J
inst✝² : DecidableEq K
inst✝¹ : DecidableEq L
inst✝ : Zero R
i : I
j : J
k : K
l : L
r : R
⊢ r = single (i, k) (j, l) r (i, k) (j, l)
Module: Mathlib.Algebra.Star.StarRingHom

Goal state before:
pp: A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst✝⁷ : NonUnitalNonAssocSemiring A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Star B
inst✝³ : NonUnitalNonAssocSemiring C
inst✝² : Star C
inst✝¹ : NonUnitalNonAssocSemiring D
inst✝ : Star D
f : A → B
map_mul'✝¹ : ∀ (x y : A), f (x * y) = f x * f y
map_zero'✝¹ : { toFun := f, map_mul' := map_mul'✝¹ }.toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    { toFun := f, map_mul' := map_mul'✝¹ }.toFun (x + y) =
      { toFun := f, map_mul' := map_mul'✝¹ }.toFun x + { toFun := f, map_mul' := map_mul'✝¹ }.toFun y
map_star'✝¹ :
  ∀ (a : A),
    { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun (star a) =
      star ({ toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹ }.toFun a)
g : A → B
map_mul'✝ : ∀ (x y : A), g (x * y) = g x * g y
map_zero'✝ : { toFun := g, map_mul' := map_mul'✝ }.toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    { toFun := g, map_mul' := map_mul'✝ }.toFun (x + y) =
      { toFun := g, map_mul' := map_mul'✝ }.toFun x + { toFun := g, map_mul' := map_mul'✝ }.toFun y
map_star'✝ :
  ∀ (a : A),
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun (star a) =
      star ({ toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝ }.toFun a)
h :
  (fun f ↦ f.toFun)
      { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹,
        map_star' := map_star'✝¹ } =
    (fun f ↦ f.toFun)
      { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }
⊢ { toFun := f, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹, map_add' := map_add'✝¹, map_star' := map_star'✝¹ } =
    { toFun := g, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝, map_star' := map_star'✝ }

Tactic:
congr

Goal state after:
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
x y : A
⊢ ↑⟨⅟2 • (x + y - star (x + y)), ⋯⟩ = ↑(⟨⅟2 • (x - star x), ⋯⟩ + ⟨⅟2 • (y - star y), ⋯⟩)

Tactic:
simp only [sub_add, ← smul_add, sub_sub_eq_add_sub, star_add, AddSubgroup.coe_add]

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

Goal state before:
pp: m : Type u_2
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (blockDiagonal fun x ↦ diagonal fun x ↦ 1) = diagonal fun x ↦ 1

Tactic:
blockDiagonal_diagonal

Goal state after:
m : Type u_2
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : Zero α
inst✝¹ : DecidableEq m
inst✝ : One α
⊢ (diagonal fun ik ↦ 1) = diagonal fun x ↦ 1
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
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
⊢ (blockDiagonal' M)ᵀ = blockDiagonal' fun k ↦ (M k)ᵀ

Tactic:
ext ⟨ii, ix⟩ ⟨ji, jx⟩

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝¹ : DecidableEq o
inst✝ : Zero α
M : (i : o) → Matrix (m' i) (n' i) α
ii : o
ix : n' ii
ji : o
jx : m' ji
⊢ (blockDiagonal' M)ᵀ ⟨ii, ix⟩ ⟨ji, jx⟩ = blockDiagonal' (fun k ↦ (M k)ᵀ) ⟨ii, ix⟩ ⟨ji, jx⟩
Module: Mathlib.LinearAlgebra.Matrix.RowCol

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ A * single i j r = updateCol 0 j (A.col i <• r)

Tactic:
single_eq_updateCol_zero,

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type v
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix l m α
i : m
j : n
r : α
⊢ A * updateCol 0 j (Pi.single i r) = updateCol 0 j (A.col i <• r)
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, ⋯⟩
⊢ generator (ϕ.submoduleImage N) ∈ span R {a, ψ ⟨y, ⋯⟩}

Tactic:
· exact subset_span (mem_insert _ _)

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

Goal state before:
pp: 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 b : M
x✝¹ : a ∈ Submonoid.closure S
x✝ : b ∈ Submonoid.closure S
ha : Irreducible a → a ∈ S
hb : Irreducible b → b ∈ S
h : Irreducible (a * b)
⊢ a * b ∈ S

Tactic:
obtain rfl | rfl := h.eq_one_or_eq_one <;> simp_all

Goal state after:
Module: Mathlib.Algebra.Field.Subfield.Defs

Goal state before:
pp: case mk.mk
K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
toSubring✝¹ : Subring K
inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier → x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier → x⁻¹ ∈ toSubring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubring := toSubring✝¹, inv_mem' := inv_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubring := toSubring✝, inv_mem' := inv_mem'✝ }
⊢ { toSubring := toSubring✝¹, inv_mem' := inv_mem'✝¹ } = { toSubring := toSubring✝, inv_mem' := inv_mem'✝ }

Tactic:
congr

Goal state after:
case mk.mk
K : Type u
L : Type v
M : Type w
inst✝² : DivisionRing K
inst✝¹ : DivisionRing L
inst✝ : DivisionRing M
toSubring✝¹ : Subring K
inv_mem'✝¹ : ∀ (x : K), x ∈ toSubring✝¹.carrier → x⁻¹ ∈ toSubring✝¹.carrier
toSubring✝ : Subring K
inv_mem'✝ : ∀ (x : K), x ∈ toSubring✝.carrier → x⁻¹ ∈ toSubring✝.carrier
h :
  (fun s ↦ s.carrier) { toSubring := toSubring✝¹, inv_mem' := inv_mem'✝¹ } =
    (fun s ↦ s.carrier) { toSubring := toSubring✝, inv_mem' := inv_mem'✝ }
⊢ toSubring✝¹ = toSubring✝
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : MonoidWithZero R
S : Submonoid R
inst✝ : OreSet S
s : ↥S
⊢ s • 0 = 1 • 0 ∧ ↑s * ↑1 = 1 * ↑s

Tactic:
simp [Submonoid.smul_def]

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:
rw [OreLocalization.zero_def, oreDiv_mul_char 0 r 1 s 0 1 (by simp), zero_mul, one_mul]

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

Goal state before:
pp: case neg.intro.refine_1.refine_2
ι : 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
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : ϕ ⟨y, ⋯⟩ = a
c : ι → R
hc : ∀ (i : ι), (b'M.coord i) ⟨y, ⋯⟩ = a * c i
val✝ : Fintype ι
y' : O := ∑ i, c i • ↑(b'M i)
y'M : y' ∈ M
mk_y' : ⟨y', y'M⟩ = ∑ i, c i • b'M i
a_smul_y' : a • y' = y
ϕy'_eq : ϕ ⟨y', y'M⟩ = 1
ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis (Fin n') R ↥N'
⊢ ∀ z ∈ N, ∃ c, z + c • y ∈ N'

Tactic:
· intro z zN
      obtain ⟨b, hb⟩ : _ ∣ ϕ ⟨z, N_le_M zN⟩ := generator_submoduleImage_dvd_of_mem N_le_M ϕ zN
      refine ⟨-b, Submodule.mem_map.mpr ⟨⟨_, N.sub_mem zN (N.smul_mem b yN)⟩, ?_, ?_⟩⟩
      · refine LinearMap.mem_ker.mpr (show ϕ (⟨z, N_le_M zN⟩ - b • ⟨y, N_le_M yN⟩) = 0 from ?_)
        rw [map_sub, map_smul, hb, ϕy_eq, smul_eq_mul, mul_comm, sub_self]
      · simp only [sub_eq_add_neg, neg_smul, coe_subtype]

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

Goal state before:
pp: case c.c.c.e_a.e_a
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ ra • r₂ /ₒ (sa * s₁) = ra • r₂ /ₒ ⟨ra * ↑s₂, ⋯⟩

Tactic:
congr

Goal state after:
case e_s
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ sa * s₁ = ⟨ra * ↑s₂, ⋯⟩
Module: Mathlib.RingTheory.OreLocalization.Basic

Goal state before:
pp: case c.c.c.e_a.e_a
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ rc • r₃ /ₒ (sc * (sa * s₁)) = rc • r₃ /ₒ ⟨rc * ↑s₃, ⋯⟩

Tactic:
congr

Goal state after:
case e_s
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₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * ↑s₁ = ra * ↑s₂
rc : R
sc : ↥S
hc : ↑sc * ↑(sa * s₁) = rc * ↑s₃
⊢ sc * (sa * s₁) = ⟨rc * ↑s₃, ⋯⟩