mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mk
α : 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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
y : ↑(iUnion S)
i j : ι
hj : ↑y ∈ S j
k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
val✝ : α
property✝ : val✝ ∈ iUnion S
hi : ↑⟨val✝, property✝⟩ ∈ S i
⊢ ⟨val✝, property✝⟩ = inclusion ⋯ ⟨↑⟨val✝, property✝⟩, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Set.UnionLift

Goal state before:
pp: case mk
α : 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⟩
dir : Directed (fun x1 x2 ↦ x1 ⊆ x2) S
opi : (i : ι) → ↑(S i) → ↑(S i) → ↑(S i)
opβ : β → β → β
h : ∀ (i : ι) (x y : ↑(S i)), f i (opi i x y) = opβ (f i x) (f i y)
op : ↑(iUnion S) → ↑(iUnion S) → ↑(iUnion S)
hopi : ∀ (i : ι) (x y : ↑(S i)), inclusion ⋯ (opi i x y) = op (inclusion ⋯ x) (inclusion ⋯ y)
x : ↑(iUnion S)
i : ι
hi : ↑x ∈ S i
j k : ι
hik : S i ⊆ S k
hjk : S j ⊆ S k
hx : x = inclusion ⋯ ⟨↑x, ⋯⟩
val✝ : α
property✝ : val✝ ∈ iUnion S
hj : ↑⟨val✝, property✝⟩ ∈ S j
⊢ ⟨val✝, property✝⟩ = inclusion ⋯ ⟨↑⟨val✝, property✝⟩, ⋯⟩

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a * Multiset.count a {a} = f a

Tactic:
Multiset.count_singleton_self,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f : α →₀ ℕ
a : α
⊢ f a * 1 = f a
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
inst✝ : AddZeroClass α
i : m
j : n
⊢ entryAddMonoidHom α i j =
    ((Pi.evalAddMonoidHom (fun x ↦ α) j).comp (Pi.evalAddMonoidHom (fun i ↦ n → α) i)).comp ↑ofAddEquiv.symm

Tactic:
rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
α : Type u_11
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
i : m
j : n
⊢ entryLinearMap R α i j = LinearMap.proj j ∘ₗ LinearMap.proj i ∘ₗ ↑(ofLinearEquiv R).symm

Tactic:
rfl

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

Goal state before:
pp: m : Type u_2
n : Type u_3
R : Type u_7
S : Type u_8
α : Type u_11
β : Type u_12
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid α
inst✝⁴ : AddCommMonoid β
inst✝³ : Module R α
inst✝² : Module S β
σᵣₛ : R →+* S
σₛᵣ : S →+* R
inst✝¹ : RingHomInvPair σᵣₛ σₛᵣ
inst✝ : RingHomInvPair σₛᵣ σᵣₛ
f : α ≃ₛₗ[σᵣₛ] β
⊢ ↑f.mapMatrix = (↑f).mapMatrix

Tactic:
rfl

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : StrongRankCondition R
n : ℕ
hn : finrank R M = n.succ
⊢ 0 < finrank R M

Tactic:
by rw [hn]; exact n.succ_pos

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
x : RingCon R
⊢ { ringCon := x } = { ringCon := { ringCon := x }.ringCon }

Tactic:
rfl

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

Goal state before:
pp: 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} ⋯ ⋯ ⋯ ⋯ ⋯
this : I.ringCon ⊔ J.ringCon ≤ s.ringCon
h : x ∈ I ⊔ J
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) ↔ x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
rfl

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
x✝ : ι
⊢ ψ.comp (DFinsupp.singleAddHom (fun i ↦ β i) x✝) = ψ.comp (of β x✝)

Tactic:
rfl

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 : ι
f : γ →+ β i
⊢ (AddMonoidHom.compHom (of β i)) f = (of β i).comp f

Tactic:
rfl

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 y : ⨁ (i : ι), M
ihx : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) x) = x
ihy : (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) y) = y
⊢ (of (fun x ↦ M) default) ((toAddMonoid fun x ↦ AddMonoidHom.id M) (x + y)) = x + y

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Algebra.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✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R A
inst✝³ : Module R B
inst✝² : Module R C
S✝ : NonUnitalSubalgebra R A
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
b : B
hb : b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier
⊢ r • b ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier

Tactic:
rcases hb with ⟨a, ha, rfl⟩

Goal state after:
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✝⁶ : NonUnitalNonAssocSemiring B
inst✝⁵ : NonUnitalNonAssocSemiring C
inst✝⁴ : Module R A
inst✝³ : Module R B
inst✝² : Module R C
S✝ : NonUnitalSubalgebra R A
inst✝¹ : FunLike F A B
inst✝ : NonUnitalAlgHomClass F R A B
f : F
S : NonUnitalSubalgebra R A
r : R
a : A
ha : a ∈ ↑S.toNonUnitalSubsemiring
⊢ r • ↑f a ∈ (NonUnitalSubsemiring.map (↑f) S.toNonUnitalSubsemiring).carrier
Module: Mathlib.Algebra.DirectSum.Module

Goal state before:
pp: R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M) ((lof R ι M i) m) = Pi.single i m

Tactic:
rfl

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

Goal state before:
pp: R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ sSup (insert (A i) (A '' {j})) = sSup {A i, A j}

Tactic:
Set.image_singleton

Goal state after:
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ sSup {A i, A j} = sSup {A i, A j}
Module: Mathlib.Algebra.Algebra.Subalgebra.Basic

Goal state before:
pp: R : Type u
A : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
S : Subalgebra R A
a✝ : ↥S
⊢ ↑((S.equivOfEq S ⋯) a✝) = ↑(AlgEquiv.refl a✝)

Tactic:
rfl

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

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
ι : Type u_1
inst✝ : DecidableEq ι
m : ι →₀ M
i : ι
⊢ ((finsuppLEquivDirectSum R M ι) m) i = m i

Tactic:
rfl

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

Goal state before:
pp: R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_1
inst✝² : DecidableEq ι
N : Type u_2
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
ε : M →ₗ[R] N
m : ι →₀ M
i : ι
⊢ ((lmap fun x ↦ ε) ((finsuppLEquivDirectSum R M ι) m)) i = ((finsuppLEquivDirectSum R N ι) (Finsupp.mapRange ⇑ε ⋯ m)) i

Tactic:
rfl

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

Goal state before:
pp: case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toSubsemiring✝ : Subsemiring A
algebraMap_mem'✝ : ∀ (r : R), (algebraMap R A) r ∈ toSubsemiring✝.carrier
⊢ { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }.toNonUnitalSubalgebra.toSubalgebra ⋯ =
    { toSubsemiring := toSubsemiring✝, algebraMap_mem' := algebraMap_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case mk
R : Type u_1
A : Type u_2
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring A
smul_mem'✝ : ∀ (c : R) {x : A}, x ∈ toNonUnitalSubsemiring✝.carrier → c • x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }.toSubalgebra
        h1).toNonUnitalSubalgebra =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, smul_mem' := smul_mem'✝ }

Tactic:
rfl

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

Goal state before:
pp: case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)

Tactic:
| cons hd tl ih =>

Goal state after:
case a.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : List A
tl : List (List A)
ih :
  (∀ t ∈ tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → (List.map List.prod tl).sum ∈ span R ↑(Submonoid.closure s)
HL : ∀ t ∈ hd :: tl, ∀ y ∈ t, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ (List.map List.prod (hd :: tl)).sum ∈ span R ↑(Submonoid.closure s)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : ∀ y ∈ hd :: tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod

Tactic:
| cons hd tl ih =>

Goal state after:
case a.cons.cons
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Algebra R A
s : Set A
hd : A
tl : List A
ih : (∀ y ∈ tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s) → ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = tl.prod
HL : ∀ y ∈ hd :: tl, y ∈ Set.range ⇑(algebraMap R A) ∪ s
⊢ ∃ z r, ∃ (_ : r ∈ Submonoid.closure s), z • r = (hd :: tl).prod
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁷ : CommSemiring R
inst✝⁶ : NonUnitalNonAssocSemiring A
inst✝⁵ : Module R A
S : NonUnitalSubalgebra R A
inst✝⁴ : NonUnitalNonAssocSemiring B
inst✝³ : Module R B
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
ι : Sort u_1
inst✝ : Nonempty ι
K : ι → NonUnitalSubalgebra R A
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₙₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
i j : ι
x : A
hxi : x ∈ ↑(K i)
hxj : x ∈ ↑(K j)
k : ι
hik : (fun x1 x2 ↦ x1 ≤ x2) (K i) (K k)
hjk : (fun x1 x2 ↦ x1 ≤ x2) (K j) (K k)
⊢ ((f k).comp (inclusion hik)) ⟨x, hxi⟩ = ((f k).comp (inclusion hjk)) ⟨x, hxj⟩

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ (((mk R M R).compr₂ₛₗ ↑(TensorProduct.comm R M R ≪≫ₗ TensorProduct.lid R M)) x✝) 1 =
    (((mk R M R).compr₂ₛₗ ↑(TensorProduct.rid R M)) x✝) 1

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
M : Type u_5
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ (((mk R R M).compr₂ₛₗ ↑(TensorProduct.comm R R M ≪≫ₗ TensorProduct.rid R M)) 1) x✝ =
    (((mk R R M).compr₂ₛₗ ↑(TensorProduct.lid R M)) 1) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((mk R N P).compr₂ₛₗ
          (((mk R M (N ⊗[R] P)).compr₂ₛₗ
              (lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))) ∘ₗ
                lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P))))
            x✝²))
        x✝¹)
      x✝ =
    (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ LinearMap.id) x✝²)) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝¹⁶ : CommSemiring R
R' : Type u_2
inst✝¹⁵ : Monoid R'
R'' : Type u_3
inst✝¹⁴ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹³ : AddCommMonoid M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : AddCommMonoid P
inst✝¹⁰ : AddCommMonoid Q
inst✝⁹ : AddCommMonoid S
inst✝⁸ : AddCommMonoid T
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : Module R Q
inst✝⁴ : Module R S
inst✝³ : Module R T
inst✝² : DistribMulAction R' M
inst✝¹ : Module R'' M
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              (lift (uncurry (RingHom.id R) N P (M ⊗[R] N ⊗[R] P) ∘ₗ curry (mk R (M ⊗[R] N) P)) ∘ₗ
                lift (lift (lcurry (RingHom.id R) N P (M ⊗[R] (N ⊗[R] P)) ∘ₗ mk R M (N ⊗[R] P))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ (((mk R N P).compr₂ₛₗ (((mk R M (N ⊗[R] P)).compr₂ₛₗ ↑(leftComm R M N P)) x✝²)) x✝¹) x✝ =
    (((mk R N P).compr₂ₛₗ
          (((mk R M (N ⊗[R] P)).compr₂ₛₗ
              ↑((TensorProduct.assoc R M N P).symm ≪≫ₗ congr (TensorProduct.comm R M N) (LinearEquiv.refl R P) ≪≫ₗ
                  TensorProduct.assoc R N M P))
            x✝²))
        x✝¹)
      x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝² : M
x✝¹ : P
x✝ : N
⊢ ((((mk R M P).compr₂ₛₗ
            ((mk R (M ⊗[R] P) N).compr₂ₛₗ
              (lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M P).compr₂ₛₗ ((mk R (M ⊗[R] P) N).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝²⁰ : CommSemiring R
R' : Type u_2
inst✝¹⁹ : Monoid R'
R'' : Type u_3
inst✝¹⁸ : Semiring R''
A : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
Q : Type u_8
S : Type u_9
T : Type u_10
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : AddCommMonoid N
inst✝¹⁵ : AddCommMonoid P
inst✝¹⁴ : AddCommMonoid Q
inst✝¹³ : AddCommMonoid S
inst✝¹² : AddCommMonoid T
inst✝¹¹ : Module R M
inst✝¹⁰ : Module R N
inst✝⁹ : Module R Q
inst✝⁸ : Module R S
inst✝⁷ : Module R T
inst✝⁶ : DistribMulAction R' M
inst✝⁵ : Module R'' M
inst✝⁴ : Module R P
P' : Type u_11
Q' : Type u_12
inst✝³ : AddCommMonoid P'
inst✝² : Module R P'
inst✝¹ : AddCommMonoid Q'
inst✝ : Module R Q'
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              (lift (lift (↑lflip ∘ₗ (mk R M N).compr₂ (mk R (M ⊗[R] N) P))) ∘ₗ
                lift (lift (↑lflip ∘ₗ (mk R M P).compr₂ (mk R (M ⊗[R] P) N))))))
          x✝²)
        x✝¹)
      x✝ =
    ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ LinearMap.id)) x✝²) x✝¹) x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
x✝² : M
x✝¹ : N
x✝ : P
⊢ ((((mk R M N).compr₂ₛₗ ((mk R (M ⊗[R] N) P).compr₂ₛₗ ↑(rightComm R M N P))) x✝²) x✝¹) x✝ =
    ((((mk R M N).compr₂ₛₗ
            ((mk R (M ⊗[R] N) P).compr₂ₛₗ
              ↑(TensorProduct.assoc R M N P ≪≫ₗ congr (LinearEquiv.refl R M) (TensorProduct.comm R N P) ≪≫ₗ
                  (TensorProduct.assoc R M P N).symm)))
          x✝²)
        x✝¹)
      x✝

Tactic:
rfl

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
e : A →ₐ[R] B
x : A
⊢ adjoin R (⇑e '' {x}) = R[e x]

Tactic:
Set.image_singleton

Goal state after:
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
e : A →ₐ[R] B
x : A
⊢ R[e x] = R[e x]
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ center.instNonUnitalCommSemiring.toNonUnitalSemiring = NonUnitalSubsemiringClass.toNonUnitalSemiring (center R A)

Tactic:
rfl

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

Goal state before:
pp: case e'_2
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✝¹⟩ + ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_3
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✝¹⟩ + ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_2
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✝¹⟩ * ⟨x✝², x✝⟩)

Tactic:
rfl

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

Goal state before:
pp: case e'_3
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✝¹⟩ * ⟨x✝², x✝⟩)

Tactic:
rfl

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✝³ : Ring A
inst✝² : Algebra R A
inst✝¹ : Ring B
inst✝ : Algebra R B
f : A →ₐ[R] B
S : Subalgebra R A
x y : A
hy : y ∈ S
hxy : f y = f x
⊢ x - y ∈ ⇑f ⁻¹' {0}

Tactic:
simp [hxy]

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
⊢ Projective R (P × Q)

Tactic:
by
  refine .of_lifting_property'' fun f hf ↦ ?_
  rcases projective_lifting_property f (.inl _ _ _) hf with ⟨g₁, hg₁⟩
  rcases projective_lifting_property f (.inr _ _ _) hf with ⟨g₂, hg₂⟩
  refine ⟨coprod g₁ g₂, ?_⟩
  rw [LinearMap.comp_coprod, hg₁, hg₂, LinearMap.coprod_inl_inr]

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

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsRegular (star x) ↔ IsRegular x

Tactic:
isRegular_iff,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsRegular x
Module: Mathlib.Algebra.Star.Basic

Goal state before:
pp: R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsRegular x

Tactic:
isRegular_iff,

Goal state after:
R : Type u
inst✝¹ : Mul R
inst✝ : StarMul R
x : R
⊢ IsLeftRegular (star x) ∧ IsRightRegular (star x) ↔ IsLeftRegular x ∧ IsRightRegular x
Module: Mathlib.Algebra.Star.SelfAdjoint

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℕ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : CommRing R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
A : Type u_2
inst✝¹ : Field R
inst✝ : StarRing R
n✝ : ℤ
x✝ : ↥(selfAdjoint R)
⊢ ↑(n✝ • x✝) = n✝ • ↑x✝

Tactic:
rfl

Goal state after: