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

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
rw [pred_eq_iff_isMin.2 ha']

Goal state after:
case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
this : pred^[n + 1] b ∈ s
ha' : IsMin (pred^[n + 1] b)
⊢ f (pred^[n + 1] b) < f b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u
x : List α
⊢ Vector.traverse pure ⟨x, ⋯⟩ = pure ⟨x, ⋯⟩

Tactic:
dsimp [Vector.traverse, cast]

Goal state after:
α : Type u
x : List α
⊢ traverseAux pure x = pure ⟨x, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: α : Type u
⊢ #(Option α) = #α + 1

Tactic:
by
  rw [(Equiv.optionEquivSumPUnit.{u, u} α).cardinal_eq, mk_sum, mk_eq_one PUnit, lift_id, lift_id]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : PartialOrder α
f : α ≤i β
⊢ b < f a → ∃ a' < a, f a' = b

Tactic:
intro h
    obtain ⟨c, hc⟩ := f.mem_range_of_rel h
    refine ⟨c, ?_, hc⟩
    rwa [← hc, f.lt_iff_lt] at h

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
β : Type u_5
a : Part α
inst✝ : Decidable a.Dom
b : β
f : α → β
⊢ a.toOption.elim b f = if h : a.Dom then f (a.get h) else b

Tactic:
by
  split_ifs with h
  · rw [h.toOption]
    rfl
  · rw [Part.toOption_eq_none_iff.2 h]
    rfl

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
⊢ ∀ (b : α), f b ≤ b → ⨆ n, (⇑f)^[n] ⊥ ≤ b

Tactic:
intro a h_a

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h : ωScottContinuous ⇑f
a : α
h_a : f a ≤ a
⊢ ⨆ n, (⇑f)^[n] ⊥ ≤ a
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ¬(⋃₀ s✝ ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝) → False

Tactic:
simp only [sUnion_subset_iff, not_or, not_forall, exists_prop, and_imp, forall_exists_index]

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ∀ x ∈ s✝, ¬x ⊆ c₁ → ¬SuccChain r c₁ ⊆ ⋃₀ s✝ → False
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ∀ (i : ℕ), c i ≤ a

Tactic:
apply h.1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ IsLUB (Set.range ⇑(c.map { toFun := f, monotone' := ⋯ })) (f (ωSup c))

Tactic:
by
  simpa [Set.range_comp]
    using hf (by simp) (Set.range_nonempty _) (isChain_range c).directedOn (isLUB_range_ωSup c)

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
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ x

Tactic:
apply hx i

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
x : Part α
hx : ∀ (i : ℕ), c i ≤ x
a : α
i : ℕ
ha : some a = c i
⊢ a ∈ c i
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ ↑(⇑Equiv.ulift.symm ⁻¹' (fun x ↦ { down := f x.down }) ⁻¹' {{ down := b }}) ≃ ↑(f ⁻¹' {b})

Tactic:
simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_ofPred_eq, coe_ofPred]

Goal state after:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #↑(f ⁻¹' {b}) ≤ c
b : β
⊢ { x // f (Equiv.ulift.symm x).down = b } ≃ { x // f x = b }
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl.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 = f
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
simp [hx, hy]

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

Goal state before:
pp: case inl
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ℵ₀ ≤ c
hd : ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
simp [Cardinal.toNat_apply_of_aleph0_le, hc, hd]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ toENat c < ↑n ↔ c < ↑n

Tactic:
simp [← not_le]

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n < toENat c ↔ ↑n < c

Tactic:
simp [← not_le]

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

Goal state before:
pp: m n : ℕ∞
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
by apply toENat_injOn <;> simp

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y

Tactic:
push Not

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (∀ (x y : M), x = y) ↔ ∀ (x y : M), x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #↑(⋃ i, f i) ≤ lift.{u, v} #ι * ⨆ i, lift.{v, u} #↑(f i)

Tactic:
by
  refine mk_iUnion_le_sum_mk_lift.trans <| Eq.trans_le ?_ (sum_le_lift_mk_mul_iSup _)
  rw [← lift_sum, lift_id'.{_, u}]

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

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
⊢ s.card ≤ n

Tactic:
have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn

Goal state after:
α : Type u
n : ℕ
t : Set α
H : ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n
s : Finset ↑t
u : Finset α := Finset.image Subtype.val s
this : u.card = s.card
⊢ s.card ≤ n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mpr
α : Type u
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) → ∃ t, ↑t = univ ∧ ∃ x y, x ≠ y ∧ t = {x, y}

Tactic:
rintro ⟨x, y, hne, h⟩
    exact ⟨{x, y}, by simpa using h, x, y, hne, rfl⟩

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

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑((insert i s).inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)

Tactic:
Finset.inf_insert,

Goal state after:
case refine_2
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Type u_4
s✝ : Finset ι
p : ι → Submodule R M
this : DecidableEq ι := Classical.decEq ι
i : ι
s : Finset ι
x✝ : i ∉ s
ih : ↑(s.inf p) = ⋂ i ∈ s, ↑(p i)
⊢ ↑(p i ⊓ s.inf p) = ⋂ i_1 ∈ insert i s, ↑(p i_1)
Module: Mathlib.Algebra.Module.ULift

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0

Tactic:
{

Goal state after:
R : Type u
M : Type v
N : Type w
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
c : R
⊢ c • 0 = 0
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ p ⊓ q = map p.subtype ⊥

Tactic:
map_bot,

Goal state after:
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p q : Submodule R M
⊢ Disjoint p q ↔ p ⊓ q = ⊥
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: case refine_1
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
i : ι
x₂ : M
hx₂ : x₂ ∈ S i
⊢ ∃ (hx'' : x₂ ∈ ⨆ i, S i), C x₂ hx''

pp: case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''

Tactic:
· exact ⟨_, mem _ _ hx₂⟩

Goal state after:
case refine_2
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
C : (x : M) → x ∈ ⨆ i, S i → Prop
mem : ∀ (i : ι) (x : M) (hxS : x ∈ S i), C x ⋯
mul : ∀ (x y : M) (hx : x ∈ ⨆ i, S i) (hy : y ∈ ⨆ i, S i), C x hx → C y hy → C (x * y) ⋯
x₁ : M
hx₁ : x₁ ∈ ⨆ i, S i
x₃ y : M
⊢ (∃ (hx'' : x₃ ∈ ⨆ i, S i), C x₃ hx'') →
    (∃ (hx'' : y ∈ ⨆ i, S i), C y hx'') → ∃ (hx'' : x₃ * y ∈ ⨆ i, S i), C (x₃ * y) hx''
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
M : Type u_1
N : Type u_2
inst✝² : Mul M
inst✝¹ : Mul N
ι : Sort u_5
inst✝ : Nonempty ι
f : M →ₙ* N
hf : Function.Injective ⇑f
s : ι → Subsemigroup M
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocSemiring R
inst✝³ : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_2
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
s : Set R
⊢ centralizer s.centralizer.centralizer = centralizer s

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u_1
inst✝ : Semiring R
s : Set R
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
F : Type w
R : Type u
S : Type v
inst✝⁴ : NonUnitalNonAssocRing R
inst✝³ : NonUnitalNonAssocRing S
inst✝² : FunLike F R S
inst✝¹ : NonUnitalRingHomClass F R S
ι : Sort u_1
inst✝ : Nonempty ι
f : F
hf : Function.Injective ⇑f
s : ι → NonUnitalSubring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
M : Submonoid R
⊢ M.subsemiringClosure = Subsemiring.closure ↑M

Tactic:
by
  ext
  refine
    ⟨fun hx => ?_, fun hx =>
      (Subsemiring.mem_closure.mp hx) M.subsemiringClosure fun s sM => ?_⟩
  <;> rintro - ⟨H1, rfl⟩
  <;> rintro - ⟨H2, rfl⟩
  · exact AddSubmonoid.mem_closure.mp hx H1.toAddSubmonoid H2
  · exact H2 sM

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

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u
S : Type v
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subsemiring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ map f (iInf s) = ⨅ i, map f (s i)

Tactic:
apply SetLike.coe_injective

Goal state after:
R : Type u
S : Type v
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
ι : Sort u_1
inst✝ : Nonempty ι
f : R →+* S
hf : Function.Injective ⇑f
s : ι → Subring R
⊢ ↑(map f (iInf s)) = ↑(⨅ i, map f (s i))
Module: Mathlib.Algebra.GroupWithZero.Associated

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

Tactic:
obtain ⟨u, rfl⟩ := h
  rw [← Units.eq_mul_inv_iff_mul_eq, zero_mul]

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ IsUnit b

Tactic:
refine .of_mul_eq_one a ((mul_right_inj' hp).mp ?_)

Goal state after:
M : Type u_1
inst✝¹ : CommMonoidWithZero M
inst✝ : IsCancelMulZero M
p b : M
hp : p ≠ 0
a : Mˣ
ha : p * b * ↑a = p
⊢ p * (b * ↑a) = p * 1
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ p₁ ≤ comap p.subtype (map p.subtype p₂) ↔ p₁ ≤ p₂

Tactic:
comap_map_eq_of_injective (show Injective p.subtype from Subtype.coe_injective) p₂

Goal state after:
R : Type u_1
R₂ : Type u_2
R₃ : Type u_3
K : Type u_4
M : Type u_5
M₂ : Type u_6
M₃ : Type u_7
V : Type u_8
V₂ : Type u_9
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
p : Submodule R M
τ₁₂ : R →+* R₂
p₁ p₂ : Submodule R ↥p
⊢ p₁ ≤ p₂ ↔ p₁ ≤ p₂
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ g ^ 0 • a

Tactic:
pow_zero,

Goal state after:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : a ≤ g • a
⊢ a ≤ 1 • a
Module: Mathlib.Algebra.Order.Group.Action

Goal state before:
pp: case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ g ^ 0 • a ≤ a

Tactic:
pow_zero,

Goal state after:
case zero
G : Type u_4
inst✝³ : Monoid G
α : Type u_5
inst✝² : Preorder α
g : G
a : α
inst✝¹ : MulAction G α
inst✝ : CovariantClass G α HSMul.hSMul LE.le
h : g • a ≤ a
⊢ 1 • a ≤ a
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
ι : Sort u_9
v : ι → M
⊢ span R (range v) = ⨆ i, R ∙ v i

Tactic:
rw [span_eq_iSup_of_singleton_spans, iSup_range]

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) ↔ ¬∀ (g : B), K ≤ H → H ≤ L → g ∉ H → g ∈ L → H = K

Tactic:
push Not

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 ↔ ∃ g, K ≤ H ∧ H ≤ L ∧ g ∉ H ∧ g ∈ L ∧ H ≠ K
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 y z : M
⊢ z ∈ span R {x, y} ↔ ∃ a b, a • x + b • y = z

Tactic:
by
  simp_rw [mem_span_insert, mem_span_singleton, exists_exists_eq_and, eq_comm]

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 (Submodule R M)
m : M
⊢ m ∈ sSup s ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N

Tactic:
sSup_eq_iSup,

Goal state after:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
m : M
⊢ m ∈ ⨆ a ∈ s, a ↔ ∀ (N : Submodule R M), (∀ p ∈ s, p ≤ N) → m ∈ N
Module: Mathlib.Order.Atoms

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

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)

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
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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) x) = x

Tactic:
rcases eq_bot_or_eq_top x 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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊥) = ⊥

case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (fun x ↦ Bool.casesOn x ⊥ ⊤) ((fun x ↦ decide (x = ⊤)) ⊤) = ⊤
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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ (x ⊓ if x = ⊥ then ⊤ else ⊥) ≤ ⊥

Tactic:
rcases eq_bot_or_eq_top x 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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊥ ⊓ if ⊥ = ⊥ then ⊤ else ⊥) ≤ ⊥

case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ (⊤ ⊓ if ⊤ = ⊥ then ⊤ else ⊥) ≤ ⊥
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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x : α
⊢ ⊤ ≤ x ⊔ if x = ⊥ then ⊤ else ⊥

Tactic:
rcases eq_bot_or_eq_top x 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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊥ ⊔ if ⊥ = ⊥ then ⊤ else ⊥

case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
⊢ ⊤ ≤ ⊤ ⊔ if ⊤ = ⊥ then ⊤ else ⊥
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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
x y : α
⊢ (if x = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = x ⊓ if y = ⊥ then ⊤ else ⊥

Tactic:
rcases eq_bot_or_eq_top x 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 α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y : α
⊢ (if ⊥ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊥ ⊓ if y = ⊥ then ⊤ else ⊥

case inr
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁷ : DecidableEq α✝
inst✝⁶ : PartialOrder α✝
inst✝⁵ : BoundedOrder α✝
inst✝⁴ : IsSimpleOrder α✝
α : Type ?u.16
inst✝³ : DecidableEq α
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
y : α
⊢ (if ⊤ = ⊤ ∧ y = ⊥ then ⊤ else ⊥) = ⊤ ⊓ if y = ⊥ then ⊤ else ⊥
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 ⊥

Tactic:
rcases eq_bot_or_eq_top x with (rfl | rfl)

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

case refine_1.inr
ι : Sort u_1
α : Type u_2
β : Type u_3
inst✝² : Lattice α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
s : Set α
h : ⊤ ∈ s
⊢ ⊤ ≤ if ⊤ ∈ s then ⊤ else ⊥
Module: Mathlib.Order.Atoms

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

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

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