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

Goal state before:
pp: case refine_2
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
r : R
⊢ ⟨(algebraMap R A) r, ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

pp: case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

Tactic:
· exact Subalgebra.algebraMap_mem _ r

Goal state after:
case refine_3
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ + x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)

case refine_4
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
x✝⁴ : ↥(adjoin R s)
x : A
hx : x ∈ adjoin R s
x✝³ x✝² : A
x✝¹ : x✝³ ∈ adjoin R s
x✝ : x✝² ∈ adjoin R s
⊢ ⟨x✝³, x✝¹⟩ ∈ adjoin R (Subtype.val ⁻¹' s) →
    ⟨x✝², x✝⟩ ∈ adjoin R (Subtype.val ⁻¹' s) → ⟨x✝³ * x✝², ⋯⟩ ∈ adjoin R (Subtype.val ⁻¹' s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

Tactic:
have : f 1 ∈ adjoin R (f '' (s ∪ {1})) :=
      subset_adjoin ⟨1, ⟨Set.subset_union_right <| Set.mem_singleton 1, rfl⟩⟩
    convert! Subalgebra.smul_mem (adjoin R (f '' (s ∪ { 1 }))) this r
    rw [algebraMap_eq_smul_one]
    exact f.map_smul _ _

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

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ (f ∘ₗ g₁).coprod (f ∘ₗ g₂) = LinearMap.id

Tactic:
hg₁,

Goal state after:
R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ (inl R P Q).coprod (f ∘ₗ g₂) = LinearMap.id
Module: Mathlib.Algebra.Module.Projective

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : Semiring R
P : Type u_2
inst✝⁹ : AddCommMonoid P
inst✝⁸ : Module R P
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
Q : Type u_5
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Projective R P
inst✝ : Projective R Q
f : (P × Q →₀ R) →ₗ[R] P × Q
hf : Function.Surjective ⇑f
g₁ : P →ₗ[R] P × Q →₀ R
hg₁ : f ∘ₗ g₁ = inl R P Q
g₂ : Q →ₗ[R] P × Q →₀ R
hg₂ : f ∘ₗ g₂ = inr R P Q
⊢ f ∘ₗ g₁.coprod g₂ = LinearMap.id

Tactic:
rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]

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 0

Tactic:
Ring.inverse_non_unit _ (mt isUnit_star.mp ha),

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

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
inst✝ : StarMul R
a u : R
hu : IsUnit u
⊢ IsSelfAdjoint (star u * a * u) ↔ IsSelfAdjoint a

Tactic:
simpa using hu.star.isSelfAdjoint_conjugate_iff

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

Goal state before:
pp: R✝ : Type u_1
A : Type u_2
F : Type u_3
R : Type u_4
S : Type u_5
inst✝⁶ : Mul R
inst✝⁵ : Star R
inst✝⁴ : Mul S
inst✝³ : Star S
inst✝² : FunLike F R S
inst✝¹ : MulHomClass F R S
inst✝ : StarHomClass F R S
f : F
r : R
hr : IsStarNormal r
⊢ Commute (star (f r)) (f r)

Tactic:
simpa [map_star] using! congr(f $(hr.star_comm_self))

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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
⊢ (fromBlocks A B C D)ᵀ = fromBlocks Aᵀ Cᵀ Bᵀ Dᵀ

Tactic:
ext i j
  rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp [fromBlocks]

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

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ Mᴴ.updateRow j (star c) = (M.updateCol j c)ᴴ

Tactic:
rw [conjTranspose, conjTranspose, transpose_map, transpose_map, updateRow_transpose,
    map_updateCol]

Goal state after:
m : Type u_2
n : Type u_3
α : Type v
M : Matrix m n α
j : n
c : m → α
inst✝¹ : DecidableEq n
inst✝ : Star α
⊢ ((M.map star).updateCol j (star c))ᵀ = ((M.map star).updateCol j (star ∘ c))ᵀ
Module: Mathlib.Data.Matrix.Block

Goal state before:
pp: o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
⊢ j' ≠ k → (∑ x, (if h : k = j' then M k i (cast ⋯ x) else 0) * if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0

Tactic:
hj'

Goal state after:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
p' : o → Type u_9
α : Type u_12
inst✝³ : DecidableEq o
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : (i : o) → Fintype (n' i)
inst✝ : Fintype o
M : (i : o) → Matrix (m' i) (n' i) α
N : (i : o) → Matrix (n' i) (p' i) α
k : o
i : m' k
k' : o
j : p' k'
j' : o
hj' : j' ≠ k
⊢ (∑ x, (if h : k = j' then M k i (cast ⋯ x) else 0) * if h : j' = k' then N j' x (cast ⋯ j) else 0) = 0
Module: Mathlib.Algebra.Field.Subfield.Defs

Goal state before:
pp: K : Type u
inst✝¹ : DivisionRing K
S : Type u_1
inst✝ : SetLike S K
h : SubfieldClass S K
s : S
q : ℚ≥0
⊢ ↑q ∈ s

Tactic:
simpa only [NNRat.cast_def] using div_mem (natCast_mem s q.num) (natCast_mem s q.den)

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 r' : X
s s' : ↥S
rb sb : R
h : sb * ↑s = rb * ↑s'
h' : sb * ↑s ∈ S
⊢ r /ₒ s + r' /ₒ s' = (sb • r + rb • r') /ₒ ⟨sb * ↑s, h'⟩

Tactic:
with_unfolding_all exact add''_char r s r' s' rb sb h h'

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
n : Type u_5
inst✝¹ : DecidableEq n
inst✝ : Fintype n
x : R
⊢ toMatrix' ((algebraMap R (End R (n → R))) x) = (scalar n) x

Tactic:
by
  simp [Module.algebraMap_end_eq_smul_id, smul_eq_diagonal_mul]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
M : Submonoid R
hM : Algebra.algebraMapSubmonoid S M ≤ IsUnit.submonoid S
h : Bijective ⇑(algebraMap R S)
y : S
⊢ ∃ x, y * (algebraMap R S) ↑x.2 = (algebraMap R S) x.1

Tactic:
obtain ⟨x, rfl⟩ := h.surjective y
    use ⟨x, 1⟩
    simp

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

Goal state before:
pp: R : Type u_1
α : Type u_2
β : Type u_3
inst✝² : CommSemiring R
e✝ e : α ≃ β
inst✝¹ : Semiring β
inst✝ : Algebra R β
⊢ Sort ?u.17

Tactic:
let semiring := Equiv.semiring e
    let algebra := Equiv.algebra R e
    exact α ≃ₐ[R] β

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocSemiring β
⊢ NonUnitalNonAssocSemiring α

Tactic:
let zero := e.zero
  let add := e.add
  let mul := e.mul
  let nsmul := e.smul ℕ
  apply e.injective.nonUnitalNonAssocSemiring _ <;> intros <;> exact e.apply_symm_apply _

Goal state after:
Module: Mathlib.Algebra.Ring.TransferInstance

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := e.zero
add : Add α := e.add
mul : Mul α := e.mul
neg : Neg α := e.Neg
sub : Sub α := e.sub
nsmul : SMul ℕ α := Equiv.smul ℕ e
zsmul : SMul ℤ α := Equiv.smul ℤ e
⊢ NonUnitalNonAssocRing α

Tactic:
apply e.injective.nonUnitalNonAssocRing _

Goal state after:
case zero
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ e 0 = 0

case add
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x + y) = e x + e y

case mul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x * y) = e x * e y

case neg
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x : α), e (-x) = -e x

case sub
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (x y : α), e (x - y) = e x - e y

case nsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℕ) (x : α), e (n • x) = n • e x

case zsmul
α : Type u_1
β : Type u_2
e : α ≃ β
inst✝ : NonUnitalNonAssocRing β
zero : Zero α := ⋯
add : Add α := ⋯
mul : Mul α := ⋯
neg : Neg α := ⋯
sub : Sub α := ⋯
nsmul : SMul ℕ α := ⋯
zsmul : SMul ℤ α := ⋯
⊢ ∀ (n : ℤ) (x : α), e (n • x) = n • e x
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ quasispectrum R a ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}

Tactic:
quasispectrum

Goal state after:
R : Type u_3
A : Type u_4
inst✝² : CommSemiring R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
r : R
⊢ r ∈ {r | ∀ (hr : IsUnit r), ¬IsQuasiregular (-(hr.unit⁻¹ • a))} ↔ r ∈ spectrum R a ∪ {r | ¬IsUnit r}
Module: Mathlib.Algebra.Algebra.Spectrum.Quasispectrum

Goal state before:
pp: S : Type u_3
R : Type u_4
A : Type u_5
inst✝⁸ : Semifield R
inst✝⁷ : Field S
inst✝⁶ : NonUnitalRing A
inst✝⁵ : Algebra R S
inst✝⁴ : Module S A
inst✝³ : IsScalarTower S A A
inst✝² : SMulCommClass S A A
inst✝¹ : Module R A
inst✝ : IsScalarTower R S A
a : A
r : R
⊢ (algebraMap R S) r ∈ quasispectrum S a ↔ r ∈ quasispectrum R a

Tactic:
by
  simp_rw [Unitization.quasispectrum_eq_spectrum_inr' _ S a, spectrum.algebraMap_mem_iff]

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x✝ y✝ x y : R
hle : x ≤ y
z : R
⊢ x + z ≤ y + z

Tactic:
rw [StarOrderedRing.le_iff] at hle ⊢
    refine hle.imp fun s hs ↦ ?_
    rw [hs.2, add_right_comm]
    exact ⟨hs.1, rfl⟩

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

Goal state before:
pp: R : Type u_1
inst✝³ : Semiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
x : R
⊢ 1 < star x ↔ 1 < x

Tactic:
simpa using star_lt_star_iff (x := 1) (y := x)

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

Goal state before:
pp: R : Type u
ι : Type w
inst✝³ : Semiring R
inst✝² : StrongRankCondition R
inst✝¹ : Finite ι
inst✝ : Nontrivial R
s : Set ι
this : Fintype ι
⊢ (⇑(basisFun R ι) '' s).ncard = s.ncard

Tactic:
exact Set.ncard_image_of_injective s <| (Pi.basisFun R ι).injective

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝¹² : CommSemiring R
inst✝¹¹ : NonUnitalNonAssocSemiring A
inst✝¹⁰ : Module R A
inst✝⁹ : Star A
inst✝⁸ : NonUnitalNonAssocSemiring B
inst✝⁷ : Module R B
inst✝⁶ : Star B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R C
inst✝³ : Star C
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
S✝ : NonUnitalStarSubalgebra R A
f : F
S : NonUnitalStarSubalgebra R A
⊢ ∀ {a : B},
    a ∈ (NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra).carrier →
      star a ∈ (NonUnitalSubalgebra.map (NonUnitalAlgHomClass.toNonUnitalAlgHom f) S.toNonUnitalSubalgebra).carrier

Tactic:
rintro _ ⟨a, ha, rfl⟩; exact ⟨star a, star_mem (s := S) ha, map_star f a⟩

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

Goal state before:
pp: F : Type v'
R' : Type u'
R : Type u
A : Type v
B : Type w
C : Type w'
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : StarModule R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : NonUnitalSubalgebra R A
a : A
ha : a ∈ (S ⊔ star S).carrier
⊢ star a ∈ (S ⊔ star S).carrier

Tactic:
simpa [← mem_star_iff _ a, ← (@NonUnitalAlgebra.gi R A _ _ _ _ _).l_sup_u _ _, star_adjoin_comm,
      Set.union_comm] using ha

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ adjoin R s ≤ centralizer R ↑(centralizer R s)

Tactic:
rw [← toNonUnitalSubalgebra_le_iff, centralizer_toNonUnitalSubalgebra,
    adjoin_toNonUnitalSubalgebra]

Goal state after:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
s : Set A
⊢ NonUnitalAlgebra.adjoin R (s ∪ star s) ≤
    NonUnitalSubalgebra.centralizer R (↑(centralizer R s) ∪ star ↑(centralizer R s))
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = fg ⟨z₁, hz₁⟩ + fg ⟨z₂, hz₂⟩

Tactic:
← add_assoc,

Goal state after:
case w.refine_1
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
f g : E →ₛₗ.[σ] F
h : ∀ (x : ↥f.domain) (y : ↥g.domain), ↑x = ↑y → ↑f x = ↑g y
x : ↥(f.domain ⊔ g.domain) → E
hx : ∀ (z : ↥(f.domain ⊔ g.domain)), x z ∈ f.domain
y : ↥(f.domain ⊔ g.domain) → E
hy : ∀ (z : ↥(f.domain ⊔ g.domain)), y z ∈ g.domain
hxy : ∀ (z : ↥(f.domain ⊔ g.domain)), x z + y z = ↑z
fg : ↥(f.domain ⊔ g.domain) → F := fun z ↦ ↑f ⟨x z, ⋯⟩ + ↑g ⟨y z, ⋯⟩
fg_eq : ∀ (x' : ↥f.domain) (y' : ↥g.domain) (z' : ↥(f.domain ⊔ g.domain)), ↑x' + ↑y' = ↑z' → fg z' = ↑f x' + ↑g y'
z₁ : E
hz₁ : z₁ ∈ f.domain ⊔ g.domain
z₂ : E
hz₂ : z₂ ∈ f.domain ⊔ g.domain
⊢ fg (⟨z₁, hz₁⟩ + ⟨z₂, hz₂⟩) = fg ⟨z₁, hz₁⟩ + ↑f ⟨x ⟨z₂, hz₂⟩, ⋯⟩ + ↑g ⟨y ⟨z₂, hz₂⟩, ⋯⟩
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case refine_1
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Submodule K V
hS : IsAtom S
⊢ finrank K ↥S = 1

Tactic:
obtain ⟨v : V, hv : v ∈ S, hv_ne : v ≠ 0⟩ := S.ne_bot_iff.mp hS.ne_bot
    suffices K ∙ v = S by rw [← this, finrank_span_singleton hv_ne]
    have : K ∙ v ≠ ⊥ := by
      rw [Submodule.ne_bot_iff]
      exact ⟨v, mem_span_singleton_self v, hv_ne⟩
    rwa [← hS.le_iff_eq this, span_le, Set.singleton_subset_iff]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
⊢ ∀ (a : FreeAlgebra R X), a + 0 = a

Tactic:
by
    rintro ⟨⟩
    change Quot.mk _ _ = _
    rw [Quot.sound Rel.add_comm, Quot.sound Rel.zero_add]

Goal state after:
Module: Mathlib.LinearAlgebra.FiniteDimensional.Basic

Goal state before:
pp: case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + (1 + m))) ≤ LinearMap.ker (f ^ (k + m))

Tactic:
← add_assoc,

Goal state after:
case a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
k : ℕ
h : LinearMap.ker (f ^ k) = LinearMap.ker (f ^ k.succ)
m : ℕ
⊢ LinearMap.ker (f ^ (k + 1 + m)) ≤ LinearMap.ker (f ^ (k + m))
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
a✝ : FreeAlgebra R X
a b : Pre R X
h : Rel R X a b
⊢ liftFun R X f a = liftFun R X f b

Tactic:
by
      induction h
      · exact (algebraMap R A).map_add _ _
      · exact (algebraMap R A).map_mul _ _
      · apply Algebra.commutes
      · change _ + _ + _ = _ + (_ + _)
        rw [add_assoc]
      · change _ + _ = _ + _
        rw [add_comm]
      · change algebraMap _ _ _ + liftFun R X f _ = liftFun R X f _
        simp
      · change _ * _ * _ = _ * (_ * _)
        rw [mul_assoc]
      · change algebraMap _ _ _ * liftFun R X f _ = liftFun R X f _
        simp
      · change liftFun R X f _ * algebraMap _ _ _ = liftFun R X f _
        simp
      · change _ * (_ + _) = _ * _ + _ * _
        rw [left_distrib]
      · change (_ + _) * _ = _ * _ + _ * _
        rw [right_distrib]
      · change algebraMap _ _ _ * _ = algebraMap _ _ _
        simp
      · change _ * algebraMap _ _ _ = algebraMap _ _ _
        simp
      repeat
        change liftFun R X f _ + liftFun R X f _ = _
        simp only [*]
        rfl
      repeat
        change liftFun R X f _ * liftFun R X f _ = _
        simp only [*]
        rfl

Goal state after:
Module: Mathlib.Algebra.Polynomial.Eval.Defs

Goal state before:
pp: R : Type u
inst✝¹ : Semiring R
p : R[X]
S : Type u_1
inst✝ : Semiring S
f : R →+* S
r : R
⊢ eval₂ f (f r) p = f (eval r p)

Tactic:
by
  rw [eval₂_eq_sum, eval_eq_sum, sum, sum, map_sum f]
  simp only [f.map_mul, f.map_pow]

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : f0 (ι R x) = 0
hf1 : f1 (ι R x) = 1
⊢ False

Tactic:
rw [h, f0.commutes, Algebra.algebraMap_self_apply] at hf0

Goal state after:
R : Type u_1
X : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
x : X
r : R
h : ι R x = (algebraMap R (FreeAlgebra R X)) r
f0 : FreeAlgebra R X →ₐ[R] R := (lift R) 0
f1 : FreeAlgebra R X →ₐ[R] R := (lift R) 1
hf0 : r = 0
hf1 : f1 (ι R x) = 1
⊢ False
Module: Mathlib.Algebra.FreeAlgebra

Goal state before:
pp: case grade0
R : Type u_1
X : Type u_2
inst✝ : CommSemiring R
S : Subalgebra R (FreeAlgebra R X) := Algebra.adjoin R (Set.range (ι R))
r✝ : R
⊢ (algebraMap R (FreeAlgebra R X)) r✝ ∈ S

Tactic:
exact S.algebraMap_mem _

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: case w.refine_2
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
cne : c.Nonempty
hdir : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (domain '' c)
P : (x : ↥(sSup (domain '' c))) → { p // ↑x ∈ (↑p).domain }
f : ↥(sSup (domain '' c)) → F := fun x ↦ ↑↑↑(P x) ⟨↑x, ⋯⟩
f_eq : ∀ (p : ↑c) (x : ↥(sSup (domain '' c))) (y : ↥(↑p).domain), ↑x = ↑y → f x = ↑↑p y
⊢ ∀ (m : R) (x : ↥(sSup (domain '' c))), f (m • x) = σ m • f x

Tactic:
intro c x
    rw [f_eq (P x).1 (c • x) (c • ⟨x, (P x).2⟩) rfl, ← map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.MonoidAlgebra.Support

Goal state before:
pp: k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : Mul G
inst✝ : IsLeftCancelMul G
f : k[G]
r : k
hr : ∀ (y : k), r * y = 0 ↔ y = 0
x a✝ : G
⊢ a✝ ∈ (single x r * f).coeff.support ↔ a✝ ∈ Finset.map (mulLeftEmbedding x) f.coeff.support

Tactic:
simp [support_coeff_single_mul_eq_image f hr (.all x)]

Goal state after:
Module: Mathlib.LinearAlgebra.LinearPMap

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ x ∈ (LinearPMap.sSup c hc).domain ↔ ∃ f ∈ c, x ∈ f.domain

Tactic:
rw [domain_sSup, Submodule.mem_sSup_of_directed (hnonempty.image _)
    (DirectedOn.mono_comp LinearPMap.domain_mono.monotone hc)]

Goal state after:
R : Type u_1
S : Type u_2
inst✝⁵ : Ring R
inst✝⁴ : Ring S
σ : R →+* S
E : Type u_4
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_5
inst✝¹ : AddCommGroup F
inst✝ : Module S F
c : Set (E →ₛₗ.[σ] F)
hnonempty : c.Nonempty
hc : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) c
x : E
⊢ (∃ y ∈ domain '' c, x ∈ y) ↔ ∃ f ∈ c, x ∈ f.domain
Module: Mathlib.Data.Nat.Prime.Defs

Goal state before:
pp: p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), p = m * b → b < p → False

Tactic:
imp_false,

Goal state after:
p : ℕ
hp : 2 ≤ p
m : ℕ
h : m < p
⊢ (∀ (x : ℕ), p = m * x → m = 1) ↔ ∀ (b : ℕ), p = m * b → ¬b < p
Module: Mathlib.Algebra.CharP.Defs

Goal state before:
pp: case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
⊢ p ∣ c

Tactic:
have := Nat.sub_mod_eq_zero_of_mod_eq h.symm

Goal state after:
case mpr
R✝ : Type u_1
inst✝³ : AddMonoidWithOne R✝
p✝ a✝ b : ℕ
R : Type u_1
inst✝² : AddMonoidWithOne R
p : ℕ
inst✝¹ : CharP R p
a : ℕ
inst✝ : IsLeftCancelAdd R
c : ℕ
hle : a ≤ a + c
h : a % p = (a + c) % p
this : (a + c - a) % p = 0
⊢ p ∣ c