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

Goal state before:
pp: case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ upperBounds (Set.range ⇑c)

pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))

Tactic:
· simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
      Set.mem_ofPred_eq]
    exact fun a ↦ le_ωSup c a

Goal state after:
case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ωSup c ∈ lowerBounds (upperBounds (Set.range ⇑c))
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ IsAdmissible x f {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}

Tactic:
· apply IsAdmissible.mk
    · constructor
      · constructor
        · exact (bot_isAdmissible le_map).base_isLeast.1
        · exact Or.inl ((bot_isAdmissible le_map).base_isLeast.2 hy.mem_bot)
      · exact fun y h ↦ (bot_isAdmissible le_map).base_isLeast.2 h.1
    · rintro _ ⟨z, ⟨hz, (hzy | hyz)⟩, rfl⟩ <;>
        refine ⟨map_mem_bot le_map hz, ?_⟩
      · rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)
        · left; exact hy.map_le_of_mem_of_lt hz hzy
        · right; exact le_refl _
      · right; exact le_trans hyz (le_map z)
    · intro c hc
      refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (sep_subset _ _)), ?_⟩
      · by_cases! h : ∀ z ∈ c, z ≤ y
        · left; apply cSup_le c y h
        · rcases h with ⟨z, hz, hzy⟩
          have h' := Or.resolve_left (hc hz).2 hzy
          right
          apply le_trans h' (le_cSup _ _ hz)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
y : α
hy : IsExtremePt x f y
z : α
a✝ : y ≠ z
left✝ : z ∈ bot x f
hz : f y ≤ z
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z

Tactic:
exact le_trans (le_map y) hz

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ g' '' sᶜ = (f '' s)ᶜ

Tactic:
← hns,

Goal state after:
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
⊢ g' '' g '' (f '' s)ᶜ = (f '' s)ᶜ
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ (i : ℕ), (c.map (f.partBind g)) i ≤ x
b : β
i : ℕ
y : γ
j : ℕ
hb : b ∈ f (c (max i j))
hy : y ∈ g (c (max i j)) b
⊢ ∃ a ∈ f (c (max i j)), y ∈ g (c (max i j)) a

Tactic:
exact ⟨_, hb, hy⟩

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

Goal state before:
pp: case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
· exact mem_range_self (⊤ : ℕ∞)

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

Goal state before:
pp: c' : Cardinal.{u}
c : ℕ∞
⊢ toENat ↑c ≤ toENat c' ↔ ↑c ≤ c'

Tactic:
simp_rw [toENat_ofENat, enat_gc _]

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
by
  rw [← h.comp_eq, Function.comp_apply]

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

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) ∈ upperBounds (lift.{u, u_1} '' s)

Tactic:
rintro i ⟨j, hj, rfl⟩

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
j : Cardinal.{u_1}
hj : j ∈ s
⊢ lift.{u, u_1} j ≤ lift.{u, u_1} (sSup s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 1 ≤ c ↔ 0 < c

Tactic:
by
  rw [← succ_zero, succ_le_iff]

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

Goal state before:
pp: b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (range fun y ↦ a ^ ↑y)

Tactic:
← image_eq_range

Goal state after:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
← image_eq_range

Goal state after:
case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ x * r • 1 = r • x

Tactic:
h₂,

Goal state after:
R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • (x * 1) = r • x
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial R
h : ∀ (r : R) (m : M), r • m = 0 → r = 0 ∨ m = 0
r : R
hr : IsRegular r
m₁ m₂ : M
hm : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ m₁ = m₂

Tactic:
by
    simpa [sub_eq_zero, hr.ne_zero] using h r (m₁ - m₂) (by simpa [smul_sub, sub_eq_zero] using hm)

Goal state after:
Module: Mathlib.Algebra.Ring.CharZero

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ϕ : R →+* S
inst✝ : CharZero S
a b : ℕ
h : ↑a = ↑b
⊢ ↑a = ↑b

Tactic:
by
    rw [← map_natCast ϕ, ← map_natCast ϕ, h]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
s : Set R
sg : Subsemigroup R
hg : ↑sg = s
sa : AddSubmonoid R
ha : ↑sa = s
⊢ ∀ {a b : R}, a ∈ s → b ∈ s → a * b ∈ s

Tactic:
by subst hg; exact sg.mul_mem

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ + b✝ ∈ {0}

Tactic:
simp_all

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Defs

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝ : NonUnitalNonAssocSemiring R
a✝ b✝ : R
x✝¹ : a✝ ∈ {0}
x✝ : b✝ ∈ {0}
⊢ a✝ * b✝ ∈ {0}

Tactic:
simp_all

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

Goal state before:
pp: R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (algebraMapSubmonoid B M)

Tactic:
← algebraMapSubmonoid_map_eq M f

Goal state after:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
M : Submonoid R
B : Type w
inst✝¹ : Semiring B
inst✝ : Algebra R B
f : A →ₐ[R] B
⊢ algebraMapSubmonoid A M ≤ Submonoid.comap f.toRingHom (Submonoid.map f (algebraMapSubmonoid A M))
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
x x✝ : R
hx : x✝ ∈ ↑(Submonoid.closure s)
l : List R
hl : ∀ y ∈ l, y ∈ s
h : l.prod = x✝
⊢ (∀ t ∈ [l], ∀ y ∈ t, y ∈ s ∨ y = -1) ∧ (List.map List.prod [l]).sum = x✝

Tactic:
simp_all

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
y : M
ha : Irreducible (y ^ 2)
⊢ False

Tactic:
exact not_irreducible_pow (by decide) ha

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p q : M
hcontra : p = q
hp : p ≠ 0
x : M
hx' : ¬IsUnit x
hx'' : q = p * x
⊢ False

Tactic:
simp_all

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
hx : x ≠ 0
y : M₀
hx' : x = 0 ∨ y = 0
⊢ y = 0

Tactic:
simp_all

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

Goal state before:
pp: M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : NoZeroDivisors M₀
inst✝ : Nontrivial M₀
x : M₀
h : x = 0
⊢ ∃ y, (x = 0 ∨ y = 0) ∧ y ≠ 0

Tactic:
exact ⟨1, Or.inl h, one_ne_zero⟩

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

Goal state before:
pp: case pos
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c d : M
a_eq : a = a * c * d
ha0 : a = 0
⊢ a ~ᵤ a * c

Tactic:
simp_all

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p : M
n : ℕ
hp : Prime (p ^ n)
this : n = 1
⊢ Prime p ∧ n = 1

Tactic:
simp_all

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

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∉ M₀⁰ ↔ {s | r * s = 0 ∧ s ≠ 0}.Nonempty

Tactic:
by
  simp [mem_nonZeroDivisors_iff_left, Set.nonempty_def]

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

Goal state before:
pp: case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ x ∈ s ⊔ closure (⇑f ⁻¹' {0})

Tactic:
rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]

Goal state after:
case a
R : Type u
S : Type v
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R →+* S
s : Subring R
x y : R
hy : y ∈ s
hxy : x - y ∈ ⇑f ⁻¹' {0}
⊢ y + (x - y) ∈ closure (↑s ∪ ⇑f ⁻¹' {0})
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ DvdNotUnit (Associates.mk a) (Associates.mk b) ↔ DvdNotUnit a b

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

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
a b : M
⊢ (a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ a * x ~ᵤ b) ↔ a ≠ 0 ∧ ∃ x, ¬IsUnit x ∧ b = a * x
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
q r : M
u : Mˣ
h' : q * ↑u ~ᵤ q
hp : q * ↑u ≠ 0
x : M
hx : ¬IsUnit x ∧ r = q * ↑u * x
⊢ q ≠ 0

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ s / 0

Tactic:
by simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
simpa [mem_div] using! hs

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : GroupWithZero α
s : Set α
hs : s.Nonempty
⊢ 0 ⊆ 0 / s

Tactic:
by simpa [mem_div] using! hs

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

Goal state before:
pp: R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (fun f ↦ ((↑e₂.symm).comp f).comp ↑e₁) ((fun f ↦ ((↑e₂).comp f).comp ↑e₁.symm) f) = f

Tactic:
simp only [AlgHom.comp_assoc, symm_comp]

Goal state after:
R : Type uR
A₁ : Type uA₁
A₂ : Type uA₂
A₃ : Type uA₃
A₁' : Type uA₁'
A₂' : Type uA₂'
A₃' : Type uA₃'
inst✝¹² : CommSemiring R
inst✝¹¹ : Semiring A₁
inst✝¹⁰ : Semiring A₂
inst✝⁹ : Semiring A₃
inst✝⁸ : Semiring A₁'
inst✝⁷ : Semiring A₂'
inst✝⁶ : Semiring A₃'
inst✝⁵ : Algebra R A₁
inst✝⁴ : Algebra R A₂
inst✝³ : Algebra R A₃
inst✝² : Algebra R A₁'
inst✝¹ : Algebra R A₂'
inst✝ : Algebra R A₃'
e : A₁ ≃ₐ[R] A₂
e₁ : A₁ ≃ₐ[R] A₁'
e₂ : A₂ ≃ₐ[R] A₂'
f : A₁ →ₐ[R] A₂
⊢ (↑e₂.symm).comp ((↑e₂).comp (f.comp (AlgHom.id R A₁))) = f
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
N₁ N₂ N : Submodule R M
h₁ : N₁ ≤ N
h₂ : N₂ ≤ N
⊢ N.subtype.range ⊓ (N₁ ⊔ N₂) = map N.subtype (comap N.subtype N₁ ⊔ comap N.subtype N₂)

Tactic:
simp_all

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

Goal state before:
pp: 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
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
⊢ p x hx

Tactic:
let p' (x : M) (hx : x ∈ ({a} : Set S) • N) : Prop :=
    p x (by rwa [← Submodule.singleton_set_smul])

Goal state after:
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
N : Submodule R M
inst✝ : SMulCommClass S R M
a : S
p : (x : M) → x ∈ a • N → Prop
smul₀ : ∀ (s : M) (hs : s ∈ N), p (a • s) ⋯
x : M
hx : x ∈ a • N
smul₁ : ∀ (r : R) (m : M) (mem : m ∈ {a} • N), p m ⋯ → p (r • m) ⋯
add : ∀ (x y : M) (hx : x ∈ {a} • N) (hy : y ∈ {a} • N), p x ⋯ → p y ⋯ → p (x + y) ⋯
zero : p 0 ⋯
p' : (x : M) → x ∈ {a} • N → Prop := fun x hx ↦ p x ⋯
⊢ p x hx
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝³ : SemilatticeSup α
inst✝² : SemilatticeSup β
inst✝¹ : OrderBot α
inst✝ : OrderBot β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
simp_all

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Prod

Goal state before:
pp: ι : Type u_7
κ : Type u_8
α : Type u_9
β : Type u_10
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
s : Finset ι
t : Finset κ
f : ι → α
g : κ → β
i : α × β
a : ι
ha : a ∈ s
b : κ
hb : b ∈ t
⊢ ((∀ b ∈ s, f b ≤ i.1) ∧ ∀ b ∈ t, g b ≤ i.2) → ∀ (a : ι) (b : κ), a ∈ s → b ∈ t → f a ≤ i.1 ∧ g b ≤ i.2

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Closure

Goal state before:
pp: case e_IsClosed
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
inst✝ : Preorder α
toOrderHom✝ : α →o α
le_closure'✝¹ : ∀ (x : α), x ≤ toOrderHom✝.toFun x
idempotent'✝¹ : ∀ (x : α), toOrderHom✝.toFun (toOrderHom✝.toFun x) = toOrderHom✝.toFun x
IsClosed✝¹ : α → Prop
isClosed_iff✝¹ : ∀ {x : α}, IsClosed✝¹ x ↔ toOrderHom✝.toFun x = x
IsClosed✝ : α → Prop
le_closure'✝ :
  ∀ (x : α),
    x ≤
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
idempotent'✝ :
  ∀ (x : α),
    { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        ({ toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toFun
          x) =
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
            isClosed_iff := isClosed_iff✝¹ }.toFun
        x
isClosed_iff✝ :
  ∀ {x : α},
    IsClosed✝ x ↔
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
              isClosed_iff := isClosed_iff✝¹ }.toFun
          x =
        x
h :
  (fun c ↦ ⇑c.toOrderHom)
      { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹, IsClosed := IsClosed✝¹,
        isClosed_iff := isClosed_iff✝¹ } =
    (fun c ↦ ⇑c.toOrderHom)
      {
        toOrderHom :=
          { toOrderHom := toOrderHom✝, le_closure' := le_closure'✝¹, idempotent' := idempotent'✝¹,
              IsClosed := IsClosed✝¹, isClosed_iff := isClosed_iff✝¹ }.toOrderHom,
        le_closure' := le_closure'✝, idempotent' := idempotent'✝, IsClosed := IsClosed✝, isClosed_iff := isClosed_iff✝ }
x : α
⊢ IsClosed✝¹ x ↔ IsClosed✝ x

Tactic:
simp_all

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

Goal state before:
pp: M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ span ℕ s ≤ AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s)

Tactic:
rw [span_le]

Goal state after:
M : Type u_4
inst✝ : AddCommMonoid M
s : Set M
⊢ s ⊆ ↑(AddSubmonoid.toNatSubmodule.symm.symm (AddSubmonoid.closure s))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ span R (⋃₀ s) ≤ sSup (span R '' s)

Tactic:
rw [span_le]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Set M)
⊢ ⋃₀ s ⊆ ↑(sSup (span R '' s))
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ span R (r • s) ≤ span R s

Tactic:
rw [span_le]

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
r : R
⊢ r • s ⊆ ↑(span R s)
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ R ∙ ↑r • x = R ∙ x

Tactic:
← Units.smul_def

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x : M
r : Rˣ
⊢ R ∙ r • x = R ∙ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
hsb : IsLUB ∅ b
hs : ∀ a ∈ ∅, IsAtom a
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
b : α
⊢ IsLUB {a | IsAtom a ∧ a ≤ b} b

Tactic:
by
  rcases isLUB_atoms b with ⟨s, hsb, hs⟩
  exact ⟨fun c hc ↦ hc.2, fun c hc ↦ hsb.2 fun i hi ↦ hc ⟨hs _ hi, hsb.1 hi⟩⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a = b

Tactic:
le_antisymm_iff,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ a ≤ b ∧ b ≤ a
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderBot α
inst✝ : IsAtomistic α
a b : α
h : ∀ (c : α), IsAtom c → (c ≤ a ↔ c ≤ b)
⊢ (∀ (c : α), IsAtom c → c ≤ a → c ≤ b) ∧ ∀ (c : α), IsAtom c → c ≤ b → c ≤ a

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inl
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : IsCoatomistic α
b : α
hsb : IsGLB ∅ b
hs : ∀ a ∈ ∅, IsCoatom a
⊢ b = ⊤ ∨ ∃ a, IsCoatom a ∧ b ≤ a

Tactic:
simp_all

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

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
a : M
t : Finset M
hat : a ∉ t
IH : ↑t ⊆ ↑(span R s) → ∃ T, ↑T ⊆ s ∧ ↑t ⊆ ↑(span R ↑T)
ht : ↑(insert a t) ⊆ ↑(span R s)
T : Finset M
hTs : ↑T ⊆ s
htT : ↑t ⊆ ↑(span R ↑T)
T' : Finset M
hT's : ↑T' ⊆ s
haT' : a ∈ span R ↑T'
⊢ ↑(T ∪ T') ⊆ s

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case refine_1
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ s
⊢ x ≤ if ⊤ ∈ s then ⊤ else ⊥

pp: case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x

Tactic:
· rcases eq_bot_or_eq_top x with (rfl | rfl)
        · exact bot_le
        · rw [if_pos h]

Goal state after:
case refine_2
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
x : α
h : x ∈ upperBounds s
⊢ (if ⊤ ∈ s then ⊤ else ⊥) ≤ x
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
⊢ x ≤ a

Tactic:
obtain (hbot | h_inf) := (h x hx).bot_covBy.eq_or_eq (c := x ⊓ a) (by simp) (by simp)

Goal state after:
case inl
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
hbot : x ⊓ a = ⊥
⊢ x ≤ a

case inr
α : Type u_2
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsUpperModularLattice α
inst✝ : IsAtomistic α
a b : α
hab : a < b
s : Set α
hsb : IsLUB s b
h : ∀ a ∈ s, IsAtom a
x : α
hx : x ∈ s
hcon : ¬a ⋖ x ⊔ a
h_inf : x ⊓ a = x
⊢ x ≤ a
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝³ : Lattice α
inst✝² : IsModularLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq ι
s t : Finset ι
f : ι → α
hs : s.SupIndep f
ht : t.SupIndep f
h : Disjoint (s.sup f) (t.sup f)
⊢ (s ∪ t).SupIndep f

Tactic:
rw [show s ∪ t = ({s, t} : Finset _).biUnion id by simp]
  grind [SupIndep.biUnion, supIndep_pair]

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a i : α
hi : i ∈ {a}
⊢ Disjoint i (sSup ({a} \ {i}))

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
a i : α
hi : i ∈ {a}
⊢ Disjoint i (sSup ({a} \ {i}))

Tactic:
by
  simp_all

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
β : ι → Type u_5
t : (i : ι) → β i → α
ht : ∀ (i : ι), iSupIndep (t i)
b₁ : (i : ι) → β i
hb₁ : b₁ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
b₂ : (i : ι) → β i
hb₂ : b₂ ∈ {b | ⨅ i, t i (b i) ≠ ⊥}
h_eq : ⨅ i, t i (b₁ i) = ⨅ i, t i (b₂ i)
h_ne : ¬b₁ = b₂
i : ι
hi : b₁ i ≠ b₂ i
this : ⨅ i, t i (b₁ i) ≤ ⊥
⊢ False

Tactic:
simp_all

Goal state after:
Module: Mathlib.Order.SupIndep

Goal state before:
pp: α : Type u_1
ι : Type u_3
inst✝ : CompleteLattice α
t : ι → α
ht : iSupIndep t
h_ne_bot : ∀ (i : ι), t i ≠ ⊥
⊢ univ = {i | t i ≠ ⊥}

Tactic:
simp_all

Goal state after:
Module: Mathlib.Algebra.Notation.Indicator

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
M : Type u_3
inst✝ : One M
s : Set α
f : α → M
a : α
t : Set β
g : β → M
b : β
h1 : a ∈ s ↔ b ∈ t
h2 : f a = g b
h✝ : a ∈ s
⊢ s.mulIndicator f a = t.mulIndicator g b

Tactic:
simp_all

Goal state after: