mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

Tactic:
<;>

Goal state after:
case cons.inl
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = L.prod
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)

case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : R
tl : List R
ih : (∀ y ∈ tl, y ∈ s ∨ y = -1) → ∃ L, (∀ x ∈ L, x ∈ s) ∧ (tl.prod = L.prod ∨ tl.prod = -L.prod)
HL : (hd ∈ s ∨ hd = -1) ∧ ∀ x ∈ tl, x ∈ s ∨ x = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : tl.prod = -L.prod
⊢ ∃ L, (∀ x ∈ L, x ∈ s) ∧ ((hd :: tl).prod = L.prod ∨ (hd :: tl).prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : MonoidWithZero M
a : M
h : a ~ᵤ 0
⊢ a = 0

Tactic:
by
      let ⟨u, h⟩ := h.symm
      simpa using h.symm

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case e'_3
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ (n + 1) = a * a ^ n

pp: case e'_4
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ b ^ (n + 1) = b * b ^ n

Tactic:
<;>

Goal state after:
case e'_3
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ a ^ (n + 1) = a * a ^ n

case e'_4
M : Type u_1
inst✝ : CommMonoid M
a b : M
h : a ~ᵤ b
n : ℕ
ih : a ^ n ~ᵤ b ^ n
⊢ b ^ (n + 1) = b * b ^ n
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
p q : M
h : p ~ᵤ q
hp : Irreducible p
u : Mˣ
hu : p * ↑u = q
a b : M
hab : q = a * b
⊢ q * ↑u⁻¹ = a * (b * ↑u⁻¹)

Tactic:
simp [hab, mul_assoc]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀

pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ b ∈ nonZeroDivisorsRight M₀

Tactic:
<;>

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀

case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ b ∈ nonZeroDivisorsRight M₀
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x = 0

pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x = 0

Tactic:
<;>

Goal state after:
case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x = 0

case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x = 0
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case zero
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk (a ^ 0) = Associates.mk a ^ 0

pp: case succ
M : Type u_1
inst✝ : CommMonoid M
a : M
n✝ : ℕ
a✝ : Associates.mk (a ^ n✝) = Associates.mk a ^ n✝
⊢ Associates.mk (a ^ (n✝ + 1)) = Associates.mk a ^ (n✝ + 1)

Tactic:
<;>

Goal state after:
case zero
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ Associates.mk (a ^ 0) = Associates.mk a ^ 0

case succ
M : Type u_1
inst✝ : CommMonoid M
a : M
n✝ : ℕ
a✝ : Associates.mk (a ^ n✝) = Associates.mk a ^ n✝
⊢ Associates.mk (a ^ (n✝ + 1)) = Associates.mk a ^ (n✝ + 1)
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : ↥M₀⁰
x✝ : a ∣ b
c : ↥M₀⁰
hc : b = a * c
⊢ ↑a ∣ ↑a * ↑c

Tactic:
dvd_mul_right

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ Associates.mk a ∣ Associates.mk b ↔ a ∣ b

Tactic:
simp only [dvd_def, mk_surjective.exists, mk_mul_mk, mk_eq_mk_iff_associated,
    Associated.comm (x := b)]

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) ↔ ∃ c, b = a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) →
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂) →
    ∀ (a_2 a_3 : M), a ∣ a_2 * a_3 → ∃ x x_1, x ∣ a_2 ∧ x_1 ∣ a_3 ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
<;>

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)) →
    ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
⊢ (∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂) →
    ∀ (a_2 a_3 : M), a ∣ a_2 * a_3 → ∃ x x_1, x ∣ a_2 ∧ x_1 ∣ a_3 ∧ Associates.mk a = Associates.mk (x * x_1)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

pp: case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)

Tactic:
<;>

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b c : M
dvd : a ∣ b * c
⊢ ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

case mpr
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂
b c : M
dvd : a ∣ b * c
⊢ ∃ x x_1, x ∣ b ∧ x_1 ∣ c ∧ Associates.mk a = Associates.mk (x * x_1)
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

pp: case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (0 •> ∅)⁻¹ = ∅⁻¹ <• 0⁻¹

case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (0 •> s)⁻¹ = s⁻¹ <• 0⁻¹
Module: Mathlib.Algebra.GroupWithZero.Action.Pointwise.Set

Goal state before:
pp: case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

pp: case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_1
inst✝ : GroupWithZero α
⊢ (∅ <• 0)⁻¹ = 0⁻¹ •> ∅⁻¹

case inl.inr
α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ (s <• 0)⁻¹ = 0⁻¹ •> s⁻¹
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ x ∈ p

pp: case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ⟨x, ?refine_1⟩ ∈ q

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ x ∈ p

case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
x : M
hx : x ∈ map p.subtype q
⊢ ⟨x, ?refine_1⟩ ∈ q
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ p.subtype ⟨val✝, h⟩ ∈ p

pp: case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ ⟨p.subtype ⟨val✝, h⟩, ⋯⟩ ∈ q

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ p.subtype ⟨val✝, h⟩ ∈ p

case refine_2
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
N : Type u_9
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
p : Submodule R M
q : Submodule R ↥p
val✝ : M
h : val✝ ∈ p
left✝ : ⟨val✝, h⟩ ∈ ↑q
⊢ ⟨p.subtype ⟨val✝, h⟩, ⋯⟩ ∈ q
Module: Mathlib.Algebra.Module.Submodule.Equiv

Goal state before:
pp: R : Type u_1
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₁
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M₁ →ₗ[R] M₂
i : M₃ →ₗ[R] M₂
hi : Injective ⇑i
hf : ∀ (x : M₁), f x ∈ i.range
x : M₁
⊢ i ((f.codRestrictOfInjective i hi hf) x) = f x

Tactic:
simp [LinearMap.codRestrictOfInjective]

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y ∈ Submodule.comap O.subtype N, ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

pp: case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y ∈ Submodule.comap O.subtype N, ϕ y = x

Tactic:
<;>

Goal state after:
case refine_1
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y ∈ Submodule.comap O.subtype N, ϕ y = x) → ∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x

case refine_2
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
x : M'
⊢ (∃ y, ∃ (yO : y ∈ O), y ∈ N ∧ ϕ ⟨y, yO⟩ = x) → ∃ y ∈ Submodule.comap O.subtype N, ϕ y = x
Module: Mathlib.Algebra.Module.Submodule.Pointwise

Goal state before:
pp: case smul₀
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : S
n✝ : M
mem₁✝ : r✝ ∈ s
mem₂✝ : n✝ ∈ ⊥
⊢ r✝ • n✝ ∈ ⊥

pp: case smul₁
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : R
m✝ : M
mem✝ : m✝ ∈ s • ⊥
a✝ : m✝ ∈ ⊥
⊢ r✝ • m✝ ∈ ⊥

pp: case add
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x m₁✝ m₂✝ : M
mem₁✝ : m₁✝ ∈ s • ⊥
mem₂✝ : m₂✝ ∈ s • ⊥
a✝¹ : m₁✝ ∈ ⊥
a✝ : m₂✝ ∈ ⊥
⊢ m₁✝ + m₂✝ ∈ ⊥

pp: case zero
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
⊢ 0 ∈ ⊥

Tactic:
<;>

Goal state after:
case smul₀
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : S
n✝ : M
mem₁✝ : r✝ ∈ s
mem₂✝ : n✝ ∈ ⊥
⊢ r✝ • n✝ ∈ ⊥

case smul₁
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
r✝ : R
m✝ : M
mem✝ : m✝ ∈ s • ⊥
a✝ : m✝ ∈ ⊥
⊢ r✝ • m✝ ∈ ⊥

case add
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x m₁✝ m₂✝ : M
mem₁✝ : m₁✝ ∈ s • ⊥
mem₂✝ : m₂✝ ∈ s • ⊥
a✝¹ : m₁✝ ∈ ⊥
a✝ : m₂✝ ∈ ⊥
⊢ m₁✝ + m₂✝ ∈ ⊥

case zero
R : Type u_2
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_4
inst✝¹ : Monoid S
inst✝ : DistribMulAction S M
s : Set S
x : M
⊢ 0 ∈ ⊥
Module: Mathlib.Order.Closure

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
c : ClosureOperator α
x y : α
hy : c.IsClosed y
⊢ c x ≤ y ↔ x ≤ y

Tactic:
rw [← hy.closure_eq, ← le_closure_iff]

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
a b c : α
inst✝² : Lattice α
inst✝¹ : OrderBot α
inst✝ : IsModularLattice α
h : Disjoint a b
hsup : Disjoint (a ⊔ b) c
⊢ Disjoint a (b ⊔ c)

Tactic:
by
  rw [disjoint_iff_inf_le, ← h.eq_bot, sup_comm]
  apply le_inf inf_le_left
  apply (inf_le_inf_right (c ⊔ b) le_sup_right).trans
  rw [sup_comm, IsModularLattice.sup_inf_sup_assoc, hsup.eq_bot, bot_sup_eq]

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.inr
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
p p' : Submodule R M
h✝ : x ∈ span R (↑p ∪ ↑p')
y : M
h : y ∈ ↑p'
⊢ ∃ y_1 ∈ p, ∃ z ∈ p', y_1 + z = y

Tactic:
· exact ⟨0, by simp, y, h, by simp⟩

Goal state after:
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case inl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : a ≤ b
⊢ max a b ∈ s

pp: case inr
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : b ≤ a
⊢ max a b ∈ s

Tactic:
<;>

Goal state after:
case inl
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : a ≤ b
⊢ max a b ∈ s

case inr
α : Type u_3
inst✝ : LinearOrder α
s : Set α
a : α
ha : a ∈ s
b : α
hb : b ∈ s
h✝ : b ≤ a
⊢ max a b ∈ s
Module: Mathlib.Order.SupClosed

Goal state before:
pp: case left
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ latticeClosure s ⊆ f ⁻¹' latticeClosure (f '' s)

pp: case right
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ latticeClosure (f '' s) ⊆ f '' latticeClosure s

Tactic:
<;>

Goal state after:
case left
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ latticeClosure s ⊆ f ⁻¹' latticeClosure (f '' s)

case right
α : Type u_3
β : Type u_4
inst✝¹ : Lattice α
inst✝ : Lattice β
s : Set α
f : α → β
map_sup : ∀ (a b : α), f (a ⊔ b) = f a ⊔ f b
map_inf : ∀ (a b : α), f (a ⊓ b) = f a ⊓ f b
⊢ latticeClosure (f '' s) ⊆ f '' latticeClosure s
Module: Mathlib.Order.Atoms

Goal state before:
pp: case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif false then c else cᶜ) → c = ⊥

pp: case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif true then c else cᶜ) → c = ⊥

Tactic:
<;>

Goal state after:
case false
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif false then c else cᶜ) → c = ⊥

case true
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α✝
α : Type u_4
inst✝ : CompleteAtomicBooleanAlgebra α
b : α
inhabited_h : Inhabited α
g : α → Bool
c : α
hc : c < ⨅ a, b ⊓ bif g a then a else aᶜ
a✝ : Nontrivial α
⊢ (c < bif true then c else cᶜ) → c = ⊥
Module: Mathlib.Order.Atoms

Goal state before:
pp: case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α → IsSimpleOrder αᵒᵈ

pp: case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder αᵒᵈ → IsSimpleOrder α

Tactic:
<;>

Goal state after:
case mp
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder α → IsSimpleOrder αᵒᵈ

case mpr
α : Type u_2
inst✝¹ : LE α
inst✝ : BoundedOrder α
⊢ IsSimpleOrder αᵒᵈ → IsSimpleOrder α
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊥ ≠ b
⊢ ⊥ ≠ ⊤

pp: case inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊤ ≠ b
⊢ ⊥ ≠ ⊤

Tactic:
<;>

Goal state after:
case inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊥ ≠ b
⊢ ⊥ ≠ ⊤

case inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
b : α
h : ⊤ ≠ b
⊢ ⊥ ≠ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤

pp: case inl.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊤
⊢ ⊥ ≠ ⊤

pp: case inr.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤

pp: case inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤

Tactic:
<;>

Goal state after:
case inl.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊥
⊢ ⊥ ≠ ⊤

case inl.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊥ ≠ ⊤
⊢ ⊥ ≠ ⊤

case inr.inl
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊥
⊢ ⊥ ≠ ⊤

case inr.inr
α : Type u_2
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
h : ⊤ ≠ ⊤
⊢ ⊥ ≠ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≤ ⊥

pp: case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤

Tactic:
<;>

Goal state after:
case inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊥ ≤ ⊥

case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊥ → ⊤ ≤ ⊥

pp: case inr.inl.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊤ → ⊤ ≤ ⊤

Tactic:
<;>

Goal state after:
case inr.inl.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊥ → ⊤ ≤ ⊥

case inr.inl.inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ ⊤ → ⊤ ≤ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊥ ≤ b ∨ b ≤ ⊥

pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊤ ≤ b ∨ b ≤ ⊤

Tactic:
<;>

Goal state after:
case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊥ ≤ b ∨ b ≤ ⊥

case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : PartialOrder α
inst✝² : BoundedOrder α
inst✝¹ : IsSimpleOrder α
inst✝ : DecidableEq α
b : α
⊢ ⊤ ≤ b ∨ b ≤ ⊤
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

pp: case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z

Tactic:
<;>

Goal state after:
case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊥ ⊔ y) ⊓ (⊥ ⊔ z) ≤ ⊥ ⊔ y ⊓ z

case inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y z : α
⊢ (⊤ ⊔ y) ⊓ (⊤ ⊔ z) ≤ ⊤ ⊔ y ⊓ z