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

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
x : Matrix n n α
⊢ r • x = ((scalar n).comp (algebraMap R α)) r * x

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
inst✝⁴ : CommSemiring R
inst✝³ : Semiring α
inst✝² : Semiring β
inst✝¹ : Algebra R α
inst✝ : Algebra R β
r : R
x : Matrix n n α
i✝ j✝ : n
⊢ (r • x) i✝ j✝ = (((scalar n).comp (algebraMap R α)) r * x) i✝ j✝
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
⊢ toMultiset (f ⊔ g) = toMultiset f ∪ toMultiset g

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊔ g)) = Multiset.count a✝ (toMultiset f ∪ toMultiset g)
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
⊢ toMultiset (f ⊓ g) = toMultiset f ∩ toMultiset g

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
f g : α →₀ ℕ
a✝ : α
⊢ Multiset.count a✝ (toMultiset (f ⊓ g)) = Multiset.count a✝ (toMultiset f ∩ toMultiset g)
Module: Mathlib.Data.Finsupp.Multiset

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

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
a a✝ : α
⊢ (toFinsupp {a}) a✝ = (Finsupp.single a 1) a✝
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∪ t) = toFinsupp s ⊔ toFinsupp t

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∪ t)) a✝ = (toFinsupp s ⊔ toFinsupp t) a✝
Module: Mathlib.Data.Finsupp.Multiset

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∩ t) = toFinsupp s ⊓ toFinsupp t

Tactic:
ext

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∩ t)) a✝ = (toFinsupp s ⊓ toFinsupp t) a✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop))

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α✝ : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁶ : Fintype m
inst✝⁵ : DecidableEq m
inst✝⁴ : NonAssocSemiring α✝
inst✝³ : NonAssocSemiring β
inst✝² : NonAssocSemiring γ
α : Type ?u.30
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
x✝¹ x✝ : Matrix m m αᵐᵒᵖ
i✝ j✝ : m
⊢ unop (op ((x✝¹ * x✝)ᵀ.map unop)) i✝ j✝ = unop (op (x✝¹ᵀ.map unop) * op (x✝ᵀ.map unop)) i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) =
    { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
      { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝

Tactic:
ext

Goal state after:
α : Type u_14
inst✝¹ : MulOne α
inst✝ : AddCommMonoid α
x✝² : IsStablyFiniteRing αᵐᵒᵖ
n : ℕ
x✝¹ x✝ : Matrix (Fin n) (Fin n) α
i✝ j✝ : Fin n
⊢ { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun (x✝¹ * x✝) i✝ j✝ =
    ({ toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝¹ *
        { toFun := fun M ↦ M.map (op ∘ op), map_one' := ⋯ }.toFun x✝)
      i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝)

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β : Type u_12
γ : Type u_13
inst✝⁸ : Fintype m
inst✝⁷ : DecidableEq m
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring α
inst✝⁴ : Semiring β
inst✝³ : Semiring γ
inst✝² : Algebra R α
inst✝¹ : Algebra R β
inst✝ : Algebra R γ
x✝ : R
i✝ j✝ : m
⊢ MulOpposite.unop (RingEquiv.mopMatrix.toFun ((algebraMap R (Matrix m m αᵐᵒᵖ)) x✝)) i✝ j✝ =
    MulOpposite.unop ((algebraMap R (Matrix m m α)ᵐᵒᵖ) x✝) i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β✝ : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → Mul (β i)
inst✝ : Fintype n
x✝¹ x✝ : Matrix n n ((i : ι) → β i)
⊢ piAddEquiv.toFun (x✝¹ * x✝) = piAddEquiv.toFun x✝¹ * piAddEquiv.toFun x✝

Tactic:
ext

Goal state after:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
m' : o → Type u_5
n' : o → Type u_6
R : Type u_7
S : Type u_8
T : Type u_9
A : Type u_10
α : Type u_11
β✝ : Type u_12
γ : Type u_13
ι : Type u_14
β : ι → Type u_15
inst✝² : (i : ι) → AddCommMonoid (β i)
inst✝¹ : (i : ι) → Mul (β i)
inst✝ : Fintype n
x✝² x✝¹ : Matrix n n ((i : ι) → β i)
x✝ : ι
i✝ j✝ : n
⊢ piAddEquiv.toFun (x✝² * x✝¹) x✝ i✝ j✝ = (piAddEquiv.toFun x✝² * piAddEquiv.toFun x✝¹) x✝ i✝ j✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
⊢ (∑ i ∈ s, x i) *ᵥ y = ∑ i ∈ s, x i *ᵥ y

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → Matrix m n α
y : n → α
x✝ : m
⊢ ((∑ i ∈ s, x i) *ᵥ y) x✝ = (∑ i ∈ s, x i *ᵥ y) x✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
⊢ x *ᵥ ∑ i ∈ s, y i = ∑ i ∈ s, x *ᵥ y i

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : Matrix m n α
s : Finset ι
y : ι → n → α
x✝ : m
⊢ (x *ᵥ ∑ i ∈ s, y i) x✝ = (∑ i ∈ s, x *ᵥ y i) x✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
⊢ (∑ i ∈ s, x i) ᵥ* y = ∑ i ∈ s, x i ᵥ* y

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
s : Finset ι
x : ι → n → α
y : Matrix n m α
x✝ : m
⊢ ((∑ i ∈ s, x i) ᵥ* y) x✝ = (∑ i ∈ s, x i ᵥ* y) x✝
Module: Mathlib.Data.Matrix.Basic

Goal state before:
pp: m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
⊢ x ᵥ* ∑ i ∈ s, y i = ∑ i ∈ s, x ᵥ* y i

Tactic:
ext

Goal state after:
m : Type u_2
n : Type u_3
α : Type u_11
ι : Type u_14
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
x : n → α
s : Finset ι
y : ι → Matrix n m α
x✝ : m
⊢ (x ᵥ* ∑ i ∈ s, y i) x✝ = (∑ i ∈ s, x ᵥ* y i) x✝
Module: Mathlib.GroupTheory.Congruence.Opposite

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : M}, c x y → d x y

Tactic:
constructor

Goal state after:
case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) →
    ∀ {x y : M}, c x y → d x y

case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
⊢ (∀ {x y : M}, c x y → d x y) →
    ∀ {x y : Mᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
Module: Mathlib.RingTheory.Congruence.Opposite

Goal state before:
pp: R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) ↔
    ∀ {x y : R}, c x y → d x y

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y) →
    ∀ {x y : R}, c x y → d x y

case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
⊢ (∀ {x y : R}, c x y → d x y) →
    ∀ {x y : Rᵐᵒᵖ},
      ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } c) x y →
        ({ toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } d) x y
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
inst✝ : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Module.rank R M = #M

Tactic:
have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
  have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩
  simp only [mk_finsupp_lift_of_infinite', ← rank_eq_card_chooseBasisIndex, lift_max,
    lift_lift] at h
  refine lift_inj.mp ((max_eq_iff.mp h.symm).resolve_right <| not_and_of_not_left _ ?_).left
  exact (lift_umax.{v, u}.symm ▸ h_lt).ne

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y ↔ I.ringCon (x - y) 0

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon x y → I.ringCon (x - y) 0

case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
⊢ I.ringCon (x - y) 0 → I.ringCon x y
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R : Type u
S : Type u_1
M : Type v
inst✝¹² : Semiring R
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : Module R M
inst✝⁹ : StrongRankCondition R
inst✝⁸ : Semiring S
inst✝⁷ : StrongRankCondition S
inst✝⁶ : Module S M
inst✝⁵ : Module R S
inst✝⁴ : FaithfulSMul R S
inst✝³ : Module.Finite R S
inst✝² : IsScalarTower R S S
inst✝¹ : IsScalarTower R S M
inst✝ : Free S M
⊢ finrank S M ≤ finrank R M

Tactic:
by_cases H : Module.Finite S M
  · have := Module.Finite.trans (R := R) S M
    exact finrank_top_le_finrank_of_isScalarTower R S M
  · rw [finrank, Cardinal.toNat_eq_zero.mpr (.inr _)]
    · exact zero_le
    · rwa [← not_lt, Module.rank_lt_aleph0_iff]

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
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
constructor

Goal state after:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J
Module: Mathlib.RingTheory.TwoSidedIdeal.Kernel

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_3
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
f : F
⊢ Equivalence fun x y ↦ f x = f y

Tactic:
constructor

Goal state after:
case refl
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
⊢ ∀ (x : R), f x = f x

case symm
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
⊢ ∀ {x y : R}, f x = f y → f y = f x

case trans
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
⊢ ∀ {x y z : R}, f x = f y → f y = f z → f x = f z
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
⊢ (c + d) • LinearMap.id = c • LinearMap.id + d • LinearMap.id

Tactic:
ext

Goal state after:
R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c + d) • LinearMap.id) x✝ = (c • LinearMap.id + d • LinearMap.id) x✝
Module: Mathlib.LinearAlgebra.Dimension.Free

Goal state before:
pp: R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
⊢ (c • d) • LinearMap.id = (RingHom.id R) c • d • LinearMap.id

Tactic:
ext

Goal state after:
R✝ : Type u
S : Type u_1
M✝ M₁ : Type v
M' : Type v'
inst✝¹⁵ : Semiring R✝
inst✝¹⁴ : AddCommMonoid M✝
inst✝¹³ : Module R✝ M✝
inst✝¹² : Free R✝ M✝
inst✝¹¹ : AddCommMonoid M'
inst✝¹⁰ : Module R✝ M'
inst✝⁹ : Free R✝ M'
inst✝⁸ : AddCommMonoid M₁
inst✝⁷ : Module R✝ M₁
inst✝⁶ : Free R✝ M₁
inst✝⁵ : StrongRankCondition R✝
R : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : StrongRankCondition R
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
d1 : finrank R M = 1
c d : R
x✝ : M
⊢ ((c • d) • LinearMap.id) x✝ = ((RingHom.id R) c • d • LinearMap.id) x✝
Module: Mathlib.RingTheory.SimpleRing.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ I = ⊥ ∨ I = ⊤

Tactic:
rw [or_iff_not_imp_left, ← I.one_mem_iff]

Goal state after:
R : Type u_1
inst✝¹ : NonUnitalNonAssocRing R
A : Type u_2
inst✝ : DivisionRing A
I : TwoSidedIdeal A
⊢ ¬I = ⊥ → 1 ∈ I
Module: Mathlib.RingTheory.TwoSidedIdeal.Lattice

Goal state before:
pp: 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

Tactic:
ext

Goal state after:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
ι : Type u_2
I : ι → TwoSidedIdeal R
x✝ : RingCon R
⊢ (x✝ ∈ ringCon '' Set.range fun i ↦ I i) ↔ x✝ ∈ Set.range fun i ↦ (I i).ringCon
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
⊢ Submodule.restrictScalars R 1 = toSubmodule S

Tactic:
ext

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ Submodule.restrictScalars R 1 ↔ x✝ ∈ toSubmodule S
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
⊢ (↑(toAlgHom R (↥S) A)).range = toSubmodule S

Tactic:
ext

Goal state after:
R : Type u
A : Type w
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
S : Subalgebra R A
x✝ : A
⊢ x✝ ∈ (↑(toAlgHom R (↥S) A)).range ↔ x✝ ∈ toSubmodule S
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: F : Type v'
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
φ : F
⊢ ↑(NonUnitalAlgHom.range φ) = Set.range ⇑φ

Tactic:
ext

Goal state after:
F : Type v'
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
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ
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)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lequivCongrLeft R h).symm ((lof R κ (fun k ↦ M (h.symm k)) k) x) = (lof R ι M (h.symm k)) x

Tactic:
rw [LinearEquiv.symm_apply_eq]

Goal state after:
R : Type u
inst✝⁴ : Semiring R
ι : Type v
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
κ : Type u_1
inst✝¹ : DecidableEq ι
inst✝ : DecidableEq κ
h : ι ≃ κ
k : κ
x : M (h.symm k)
⊢ (lof R κ (fun k ↦ M (h.symm k)) k) x = (lequivCongrLeft R h) ((lof R ι M (h.symm k)) x)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: case refine_4
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 : R),
    ∀ x ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s),
      x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s) →
        a • x * b ∈ Submodule.span R ↑(NonUnitalSubsemiring.closure s)

Tactic:
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.Basic

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ (e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r) = (algebraMap R ↥(Subalgebra.map (↑e) S)) r

Tactic:
ext

Goal state after:
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Semiring B
inst✝¹ : Algebra R A
inst✝ : Algebra R B
e : A ≃ₐ[R] B
S : Subalgebra R A
r : R
⊢ ↑((e.toRingEquiv.subsemiringMap S.toSubsemiring).toFun ((algebraMap R ↥S) r)) =
    ↑((algebraMap R ↥(Subalgebra.map (↑e) S)) r)
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
⊢ S.equivOfEq S ⋯ = AlgEquiv.refl

Tactic:
ext

Goal state after:
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✝)
Module: Mathlib.Algebra.Algebra.NonUnitalSubalgebra

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
s : Set A
x✝⁴ x✝³ y✝ : A
hx✝ : x✝³ ∈ adjoin R s
hy✝ : y✝ ∈ adjoin R s
hpx : x✝³ ∈ span R ↑(Subsemigroup.closure s)
hpy : y✝ ∈ span R ↑(Subsemigroup.closure s)
x y z : A
x✝² : x ∈ span R ↑(Subsemigroup.closure s)
x✝¹ : y ∈ span R ↑(Subsemigroup.closure s)
x✝ : z ∈ span R ↑(Subsemigroup.closure s)
hxz : x * z ∈ span R ↑(Subsemigroup.closure s)
hyz : y * z ∈ span R ↑(Subsemigroup.closure s)
⊢ (x + y) * z ∈ span R ↑(Subsemigroup.closure s)

Tactic:
by simpa [add_mul] using add_mem hxz hyz

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
⊢ ⊥.toSubmodule = ⊥

Tactic:
ext

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
x✝ : A
⊢ x✝ ∈ ⊥.toSubmodule ↔ x✝ ∈ ⊥
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
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
⊢ ⊤.prod ⊤ = ⊤

Tactic:
ext

Goal state after:
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✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : IsScalarTower R B B
inst✝ : SMulCommClass R B B
x✝ : A × B
⊢ x✝ ∈ ⊤.prod ⊤ ↔ x✝ ∈ ⊤