mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ a < b ↔ ∃ c < b, a < c

Tactic:
rw [← not_iff_not]

Goal state after:
α : Type u_1
a b : α
inst✝ : LinearOrder α
h : IsSuccPrelimit b
⊢ ¬a < b ↔ ¬∃ c < b, a < c
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : OrderTop α
⊢ succ ⊤ = ⊤

Tactic:
by
  rw [succ_eq_iff_isMax, isMax_iff_eq_top]

Goal state after:
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
b : α
motive : α → Sort u_2
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
isMin : (a : α) → IsMin a → motive a
succ : (a : α) → ¬IsMax a → motive (Order.succ a)
isSuccLimit : (a : α) → IsSuccLimit a → motive a
hb : ¬IsMax b
⊢ isSuccLimitRecOn (Order.succ b) isMin succ isSuccLimit = succ b hb

Tactic:
by
  rw [isSuccLimitRecOn, isSuccPrelimitRecOn_succ_of_not_isMax]

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : Zero α
inst✝² : One α
inst✝¹ : ZeroLEOneClass α
inst✝ : NeZero 1
⊢ ∃ b, 0 < b

Tactic:
exact ⟨1, one_pos⟩

Goal state after:
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : PartialOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
hx : IsSuccLimit x
⊢ ∀ (n : ℕ), ↑n < x

Tactic:
by
  simpa using hx.add_natCast_lt hx.pos

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

Goal state before:
pp: case coe.coe
a✝¹ a✝ : ℕ
⊢ (↑a✝¹ * ↑a✝).toNat = (↑a✝¹).toNat * (↑a✝).toNat

Tactic:
· simp only [toNat_natCast]; rw [← natCast_mul, toNat_natCast]

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

Goal state before:
pp: m : ℕ∞
n : ℕ
h : m ≤ ↑n
⊢ m.toNat ≤ n

Tactic:
by
  lift m to ℕ using ne_top_of_le_ne_top (natCast_ne_top n) h
  simpa using h

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

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ m, n < ↑m

Tactic:
by
  simp_rw [lt_iff_not_ge]
  exact not_forall.mp <| eq_top_iff_forall_ge.2.mt hn

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

Goal state before:
pp: m : Type u_6 → Type u_7
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α : Type u_6
n : ℕ
f : Fin (n + 1) → α
⊢ (mOfFn fun i ↦ pure (f i)) = pure (ofFn f)

Tactic:
rw [mOfFn, @mOfFn_pure m _ _ _ n _, ofFn]
    simp

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable h default n ∈ insert default s

Tactic:
rw [enumerateCountable]

Goal state after:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match decode n with
    | some y => ↑y
    | none => default) ∈
    insert default s
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ lift.{max v w, v} (f a) = lift.{v, max v w} ((fun i ↦ lift.{w, v} (f i)) a)

Tactic:
lift_lift

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
a : ι
⊢ lift.{max v w, v} (f a) = lift.{max w v, v} (f a)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl a) ≤ (Equiv.refl (α ⊕ β)ᵒᵈ) (inl b) ↔ inl a ≤ inl b

Tactic:
change inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)

Goal state after:
case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹⁰ : LE α✝
inst✝⁹ : LE β✝
inst✝⁸ : LE γ
inst✝⁷ : LE α₁
inst✝⁶ : LE α₂
inst✝⁵ : LE β₁
inst✝⁴ : LE β₂
inst✝³ : LE γ₁
inst✝² : LE γ₂
a✝ : α✝
b✝ : β✝
c : γ
α : Type u_10
β : Type u_11
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
a : Part α
ha : a.Dom
b : α
h : a.get ha = b
⊢ a = some b

Tactic:
by simp [h.symm]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, f a = b
⊢ b ∈ c.map f

Tactic:
by
    rcases h with ⟨w, h, h'⟩
    subst b
    apply mem_map c _ h

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind g.toOrderHom).toFun (ωSup c) = ωSup (c.map ↑f) >>= ωSup (c.map g.toOrderHom)

Tactic:
← f.continuous,

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind g.toOrderHom).toFun (ωSup c) = f (ωSup c) >>= ωSup (c.map g.toOrderHom)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind ↑g).toFun (ωSup c) = f (ωSup c) >>= ωSup (c.map ↑g)

Tactic:
← g.continuous

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind ↑g).toFun (ωSup c) = f (ωSup c) >>= g (ωSup c)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
subst y

Goal state after:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x : (i : ι) → β i
hx : x ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) f → x = f
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
inst✝ : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : ⨆ i, f i = ↑n
⊢ ∃ i, f i = ⨆ i, f i

Tactic:
exact exists_eq_ciSup_of_not_isSuccLimit hf (h ▸ not_isSuccLimit_natCast n)

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
exact ⟨x, y, hne, by simpa using ht⟩

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (m • x) = g (m • f (g x))

Tactic:
rw [h₂]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (m • x) = g (m • f (g x))

Tactic:
rw [h₂]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝³ : SetLike S M
inst✝² : Monoid R
inst✝¹ : MulAction R M
inst✝ : SMulMemClass S R M
s : S
r : Rˣ
x : M
hx : x ∈ ↑s
⊢ (fun x ↦ ↑r • x) (r⁻¹ • x) = x

Tactic:
by simp [← Units.smul_def]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
s : Set R
⊢ ↑(closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))

Tactic:
simp [← Submonoid.subsemiringClosure_toAddSubmonoid, Submonoid.subsemiringClosure_eq_closure]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝¹ x✝ x : R
hx : x ∈ s
⊢ ∃ t, (∀ y ∈ t, y ∈ s) ∧ t.prod = x

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp.mem
R : Type u_1
inst✝ : Semiring R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mp
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ x ∈ closure s → ∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x

pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
· intro hx
    rw [mem_closure_iff] at hx
    induction hx using AddSubmonoid.closure_induction with
    | mem x hx =>
      suffices ∃ t : List R, (∀ y ∈ t, y ∈ s) ∧ t.prod = x from
        let ⟨t, ht1, ht2⟩ := this
        ⟨[t], List.forall_mem_singleton.2 ht1, by
          rw [List.map_singleton, List.sum_singleton, ht2]⟩
      induction hx using Submonoid.closure_induction with
      | mem x hx => exact ⟨[x], List.forall_mem_singleton.2 hx, List.prod_singleton⟩
      | one => exact ⟨[], List.forall_mem_nil _, rfl⟩
      | mul x y _ _ ht hu =>
        obtain ⟨⟨t, ht1, ht2⟩, ⟨u, hu1, hu2⟩⟩ := And.intro ht hu
        exact ⟨t ++ u, List.forall_mem_append.2 ⟨ht1, hu1⟩, by rw [List.prod_append, ht2, hu2]⟩
    | zero => exact ⟨[], List.forall_mem_nil _, rfl⟩
    | add x y _ _ hL hM =>
      obtain ⟨⟨L, HL1, HL2⟩, ⟨M, HM1, HM2⟩⟩ := And.intro hL hM
      exact ⟨L ++ M, List.forall_mem_append.2 ⟨HL1, HM1⟩, by
        rw [List.map_append, List.sum_append, HL2, HM2]⟩

Goal state after:
case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: case mem
R : Type u
inst✝ : NonAssocRing R
s : Set R
x✝ x : R
hx : x ∈ ↑(Submonoid.closure s)
⊢ x ∈ closure s

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case refine_1
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y * ↑u = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y = A * B
⊢ IsUnit A ∨ IsUnit B

pp: case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B

Tactic:
· rw [← u.isUnit_mul_units B]
    apply h
    rw [← mul_assoc, ← HAB]

Goal state after:
case refine_2
M : Type u_2
inst✝ : Monoid M
y : M
u : Mˣ
x✝ : ¬IsUnit y
h : ∀ ⦃a b : M⦄, y = a * b → IsUnit a ∨ IsUnit b
A B : M
HAB : y * ↑u = A * B
⊢ IsUnit A ∨ IsUnit B
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f p) = p

Tactic:
apply hinv

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f a
⊢ g (f a) = a

Tactic:
apply hinv

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_3
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f p) = p

Tactic:
apply hinv

Goal state after:
Module: Mathlib.Algebra.Prime.Lemmas

Goal state before:
pp: case e'_4
M : Type u_1
N : Type u_2
inst✝⁵ : CommMonoidWithZero M
inst✝⁴ : CommMonoidWithZero N
F : Type u_3
G : Type u_4
inst✝³ : FunLike F M N
inst✝² : MonoidWithZeroHomClass F M N
inst✝¹ : FunLike G N M
inst✝ : MulHomClass G N M
f : F
g : G
p : M
hinv : ∀ (a : M), g (f a) = a
hp : Prime (f p)
a b : M
h✝ : p ∣ a * b
h : f p ∣ f b
⊢ g (f b) = b

Tactic:
apply hinv

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

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
inst✝ : Subsingleton Mˣ
x✝¹ x✝ : M
⊢ x✝¹ ~ᵤ x✝ ↔ x✝¹ = x✝

Tactic:
rw [associated_iff_eq]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f - id ∘ₗ f = 0

Tactic:
id_comp,

Goal state after:
R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
⊢ f - f = 0
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝¹ : SemilatticeSup α
inst✝ : OrderBot α
s : Finset β
t : Finset γ
f : β × γ → α
⊢ (s ×ˢ t).sup f = t.sup fun i' ↦ s.sup fun i ↦ f (i, i')

Tactic:
by
  rw [sup_product_left, Finset.sup_comm]

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
x✝ x : M
hx : x ∈ s
⊢ x ∈ closure (univ • s)

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L

Tactic:
and_assoc,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H ∧ H ≤ L ∧ ¬H ≤ K ∧ H ≠ L ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ K, x ∈ H ∧ H ≠ L
Module: Mathlib.Order.Atoms

Goal state before:
pp: A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ (K ≤ H ∧ H ≤ L) ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K

Tactic:
and_assoc,

Goal state after:
A : Type u_4
B : Type u_5
inst✝² : PartialOrder A
inst✝¹ : SetLike A B
inst✝ : IsConcreteLE A B
K L : A
x✝ : K < L
H : A
⊢ K ≤ H ∧ H ≤ L ∧ K ≠ H ∧ ¬L ≤ H ↔ K ≤ H ∧ H ≤ L ∧ ∃ x ∉ H, x ∈ L ∧ H ≠ K
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
w x y z : M
a : R
⊢ (∃ z_1, (∃ a b, a • y + b • z = z_1) ∧ w = a • x + z_1) → ∃ b c, a • x + b • y + c • z = w

Tactic:
rintro ⟨u, ⟨b, c, rfl⟩, rfl⟩
    exact ⟨b, c, by rw [add_assoc]⟩

Goal state after:
Module: Mathlib.Order.Atoms

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

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

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: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a : α
⊢ a ≤ a

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

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: ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b c : α
⊢ a ≤ b → b ≤ c → a ≤ c

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

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 α
b c : α
⊢ ⊥ ≤ b → b ≤ c → ⊥ ≤ c

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 α
b c : α
⊢ ⊤ ≤ b → b ≤ c → ⊤ ≤ c
Module: Mathlib.Order.Atoms

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

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

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: ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝³ : DecidableEq α
inst✝² : PartialOrder α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
a b : α
⊢ equivBool a ≤ equivBool b ↔ a ≤ b

Tactic:
rcases eq_bot_or_eq_top a with (rfl | rfl)

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

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

Goal state before:
pp: α : 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
⊢ f '' latticeClosure s = latticeClosure (f '' s)

Tactic:
by
  simp only [subset_antisymm_iff, Set.image_subset_iff]
  constructor <;> apply latticeClosure_sup_inf_induction
  · exact fun a ha ↦ subset_latticeClosure <| Set.mem_image_of_mem _ ha
  · rintro a - b - ha hb
    simpa [map_sup] using isSublattice_latticeClosure.supClosed ha hb
  · rintro a - b - ha hb
    simpa [map_inf] using isSublattice_latticeClosure.infClosed ha hb
  · exact Set.image_mono subset_latticeClosure
  · rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊔ b, isSublattice_latticeClosure.supClosed ha hb, map_sup ..⟩
  · rintro _ - _ - ⟨a, ha, rfl⟩ ⟨b, hb, rfl⟩
    exact ⟨a ⊓ b, isSublattice_latticeClosure.infClosed ha hb, map_inf ..⟩

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
⊢ (s.product t).SupIndep f ↔ (s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')) ∧ t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')

Tactic:
refine ⟨fun h ↦ ⟨fun u _ i _ _ ↦ ?_, fun u _ i _ _ ↦ ?_⟩, fun h ↦ h.1.product h.2⟩
  · suffices Disjoint ((t.image ((i, ·))).sup f) ((u ×ˢ t).sup f) by
      simpa only [sup_image, sup_product_left]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]
  · suffices Disjoint ((s.image ((·, i))).sup f) ((s ×ˢ u).sup f) by
      simpa only [sup_image, sup_product_right]
    grind [Finset.SupIndep.disjoint_sup_sup, = product_eq_sprod, = disjoint_left]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : CompleteLattice α
a b : α
hab : a ≠ b
⊢ Disjoint a b → sSupIndep {a, b}

Tactic:
rintro h c ((rfl : c = a) | (rfl : c = b))

Goal state after:
case mpr.inl
α : Type u_1
inst✝ : CompleteLattice α
b c : α
hab : c ≠ b
h : Disjoint c b
⊢ Disjoint c (sSup ({c, b} \ {c}))

case mpr.inr
α : Type u_1
inst✝ : CompleteLattice α
a c : α
hab : a ≠ c
h : Disjoint a c
⊢ Disjoint c (sSup ({a, c} \ {c}))
Module: Mathlib.LinearAlgebra.Span.Basic

Goal state before:
pp: case mpr.mem
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_8
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
S : Set M
f g : ↥(span R S) →ₗ[R] N
h : ∀ (s : ↑S), f ⟨↑s, ⋯⟩ = g ⟨↑s, ⋯⟩
x✝ x : M
hx : x ∈ S
⊢ f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩

Tactic:
| mem x hx =>

Goal state after:
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (insert a ↑t \ {a}) = ⊥
⊢ a ⊓ sSup ↑t = ⊥

Tactic:
Set.insert_sdiff_self_of_notMem

Goal state after:
case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup ↑t = ⊥
⊢ a ⊓ sSup ↑t = ⊥

case refine_2
α : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : IsCompactlyGenerated α
s : Set α
h : ∀ (t : Finset α), ↑t ⊆ s → sSupIndep ↑t
a : α
ha : a ∈ s
t : Finset α
ht : ↑t ⊆ s \ {a}
h' : a ⊓ sSup (insert a ↑t \ {a}) = ⊥
⊢ a ∉ ↑t
Module: Mathlib.Order.CompactlyGenerated.Basic

Goal state before:
pp: ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
by_cases h : { c : α | IsCompactElement c ∧ c ≤ b } ⊆ {⊥}

Goal state after:
case pos
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : {c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

case neg
ι : Sort u_1
α : Type u_2
inst✝³ : CompleteLattice α
f : ι → α
inst✝² : IsModularLattice α
inst✝¹ : IsCompactlyGenerated α
inst✝ : ComplementedLattice α
b : α
h : ¬{c | IsCompactElement c ∧ c ≤ b} ⊆ {⊥}
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b