mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Group.Finset

Goal state before:
pp: case empty
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a

pp: case insert
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : fold max ⊥ (fun i ↦ ↑(f i) + a) s✝ = fold max ⊥ (WithBot.some ∘ f) s✝ + a
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) (insert a✝² s✝) = fold max ⊥ (WithBot.some ∘ f) (insert a✝² s✝) + a

Tactic:
<;>

Goal state after:
case empty
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) ∅ = fold max ⊥ (WithBot.some ∘ f) ∅ + a

case insert
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
a : WithBot M
f : ι → M
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : fold max ⊥ (fun i ↦ ↑(f i) + a) s✝ = fold max ⊥ (WithBot.some ∘ f) s✝ + a
⊢ fold max ⊥ (fun i ↦ ↑(f i) + a) (insert a✝² s✝) = fold max ⊥ (WithBot.some ∘ f) (insert a✝² s✝) + a
Module: Mathlib.SetTheory.Cardinal.Finsupp

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

pp: case h'
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≠ 0

Tactic:
<;>

Goal state after:
case h
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ ℵ₀ ≤ lift.{v, u} #α

case h'
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≠ 0
Module: Mathlib.SetTheory.Cardinal.Finsupp

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

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

Tactic:
<;>

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

case h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{u, v} #β ≤ #(α →₀ β)
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
  simp_rw [Multiset.count_union, Finsupp.count_toMultiset, Finsupp.sup_apply]

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

Goal state before:
pp: m : Type u_2
R : Type u_7
α : Type u_11
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
i : m
⊢ LinearMap.proj i ∘ₗ diagLinearMap m R α = entryLinearMap R α i i

Tactic:
simp [LinearMap.ext_iff]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Opposite

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

pp: 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

Tactic:
<;>

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.GroupTheory.Congruence.Opposite

Goal state before:
pp: case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {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
h' : c x✝ y✝
⊢ d x✝ y✝

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

Tactic:
<;>

Goal state after:
case mp
M : Type u_1
inst✝ : Mul M
c d : Con M
h :
  ∀ {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
h' : c x✝ y✝
⊢ d x✝ y✝

case mpr
M : Type u_1
inst✝ : Mul M
c d : Con M
h : ∀ {x y : M}, c x y → d x y
x✝ y✝ : Mᵐᵒᵖ
h' : ({ 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: 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

pp: 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

Tactic:
<;>

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.RingTheory.Congruence.Opposite

Goal state before:
pp: case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {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
h' : c x✝ y✝
⊢ d x✝ y✝

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

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h :
  ∀ {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
h' : c x✝ y✝
⊢ d x✝ y✝

case mpr
R : Type u_1
inst✝¹ : Add R
inst✝ : Mul R
c d : RingCon R
h : ∀ {x y : R}, c x y → d x y
x✝ y✝ : Rᵐᵒᵖ
h' : ({ 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: case e'_2.e'_5
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K = lift.{v, v} (Module.rank F K)

pp: case e'_2.e'_6
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank K A = lift.{v, v} (Module.rank K A)

pp: case e'_3
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F A = lift.{v, v} (Module.rank F A)

Tactic:
<;>

Goal state after:
case e'_2.e'_5
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F K = lift.{v, v} (Module.rank F K)

case e'_2.e'_6
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank K A = lift.{v, v} (Module.rank K A)

case e'_3
F : Type u
K : Type v
inst✝¹⁰ : Semiring F
inst✝⁹ : Semiring K
inst✝⁸ : Module F K
inst✝⁷ : StrongRankCondition F
inst✝⁶ : StrongRankCondition K
inst✝⁵ : Free F K
A : Type v
inst✝⁴ : AddCommMonoid A
inst✝³ : Module K A
inst✝² : Module F A
inst✝¹ : IsScalarTower F K A
inst✝ : Free K A
⊢ Module.rank F A = lift.{v, v} (Module.rank F A)
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ a = a - b + b

pp: case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ b = 0 + b

Tactic:
<;>

Goal state after:
case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ a = a - b + b

case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₁ a b
H' : a - b ∈ {x | { ringCon := t₂ }.ringCon x 0}
⊢ b = 0 + b
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ a = a - b + b

pp: case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ b = 0 + b

Tactic:
<;>

Goal state after:
case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ a = a - b + b

case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
t₁ t₂ : RingCon R
h : {x | { ringCon := t₁ }.ringCon x 0} = {x | { ringCon := t₂ }.ringCon x 0}
a b : R
H : t₂ a b
H' : a - b ∈ {x | { ringCon := t₁ }.ringCon x 0}
⊢ b = 0 + b
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ x = x - y + y

pp: case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ y = 0 + y

Tactic:
<;>

Goal state after:
case e'_3
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ x = x - y + y

case e'_4
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I : TwoSidedIdeal R
x y : R
h : I.ringCon (x - y) 0
⊢ y = 0 + y
Module: Mathlib.RingTheory.TwoSidedIdeal.Basic

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I I' J' : TwoSidedIdeal R
⊢ { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } I' ≤
      { toFun := op, invFun := unop, left_inv := ⋯, right_inv := ⋯ } J' ↔
    I' ≤ J'

Tactic:
simpa [ringCon_le_iff] using RingCon.opOrderIso.map_rel_iff

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

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

pp: 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

pp: 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

Tactic:
<;>

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.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 : I.ringCon x y
⊢ s.ringCon x y

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 : J.ringCon x y
⊢ s.ringCon x y

Tactic:
<;>

Goal state after:
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 : I.ringCon x y
⊢ s.ringCon x y

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 : J.ringCon x y
⊢ s.ringCon 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 ∈ s

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 ∈ s

Tactic:
<;>

Goal state after:
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 ∈ s

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 ∈ s
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: case zero
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
⊢ (of (fun i ↦ M) default) (0 default) = 0

pp: case of
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
i✝ : ι
x✝ : M
⊢ (of (fun i ↦ M) default) (((of (fun x ↦ M) i✝) x✝) default) = (of (fun x ↦ M) i✝) x✝

pp: case add
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ y✝ : ⨁ (i : ι), M
a✝¹ : (of (fun i ↦ M) default) (x✝ default) = x✝
a✝ : (of (fun i ↦ M) default) (y✝ default) = y✝
⊢ (of (fun i ↦ M) default) ((x✝ + y✝) default) = x✝ + y✝

Tactic:
<;>

Goal state after:
case zero
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
⊢ (of (fun i ↦ M) default) (0 default) = 0

case of
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
i✝ : ι
x✝ : M
⊢ (of (fun i ↦ M) default) (((of (fun x ↦ M) i✝) x✝) default) = (of (fun x ↦ M) i✝) x✝

case add
M : Type v
ι : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Unique ι
x✝ y✝ : ⨁ (i : ι), M
a✝¹ : (of (fun i ↦ M) default) (x✝ default) = x✝
a✝ : (of (fun i ↦ M) default) (y✝ default) = y✝
⊢ (of (fun i ↦ M) default) ((x✝ + y✝) default) = x✝ + y✝
Module: Mathlib.Algebra.DirectSum.Basic

Goal state before:
pp: ι : Type u_3
α : ι → Type u_4
β : ι → Type u_5
inst✝¹ : (i : ι) → AddCommMonoid (α i)
inst✝ : (i : ι) → AddCommMonoid (β i)
f : (i : ι) → α i →+ β i
x y : ⨁ (i : ι), α i
⊢ (∀ (i : ι), ((map f) x) i = ((map f) y) i) ↔ ∀ (i : ι), (f i) (x i) = (f i) (y i)

Tactic:
map_apply

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

Goal state before:
pp: case e'_2
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑(x • 1)

pp: case e'_3
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑y = ↑(y • 1)

Tactic:
<;>

Goal state after:
case e'_2
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑x = ↑(x • 1)

case e'_3
R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
S T U : Subalgebra R A
h✝ : S ≤ T
this : Module ↥S ↥T := (inclusion h✝).toModule
x y : ↥S
h : ∀ (a : ↥T), x • a = y • a
⊢ ↑y = ↑(y • 1)
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

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

pp: case a.cons.cons.inr
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 : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r

Tactic:
· refine ⟨hd * z, r, hr, ?_⟩
      rw [Algebra.smul_def, Algebra.smul_def, (algebraMap _ _).map_mul, _root_.mul_assoc]

Goal state after:
case a.cons.cons.inr
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 : hd ∈ Set.range ⇑(algebraMap R A) ∪ s ∧ ∀ x ∈ tl, x ∈ Set.range ⇑(algebraMap R A) ∪ s
z : R
r : A
hr : r ∈ Submonoid.closure s
hzr : z • r = tl.prod
hs : hd ∈ s
⊢ ∃ z_1 r_1, ∃ (_ : r_1 ∈ Submonoid.closure s), z_1 • r_1 = hd * z • r
Module: Mathlib.Algebra.Algebra.Subalgebra.Lattice

Goal state before:
pp: R : Type uR
A : Type uA
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
n : ℤ
s : Set A
⊢ adjoin R (insert (↑n) s) = adjoin R s

Tactic:
simpa using adjoin_insert_algebraMap (n : R) s

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✝⟩

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:
<;>

Goal state after:
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✝⟩

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✝⟩