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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (x, default)) ((fun x ↦ (ofLex x).1) (toLex (a, b))) = toLex (a, b)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ default = b
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex a) ≤
      { toFun := fun x ↦ (ofLex x).1, invFun := fun x ↦ toLex (x, default), left_inv := ⋯, right_inv := ⋯ } (toLex b) ↔
    toLex a ≤ toLex b

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : PartialOrder α
inst✝¹ : Preorder β
inst✝ : Unique β
a✝ b✝ : Lex (α × β)
a b : α × β
⊢ a.1 ≤ b.1 ↔ a.1 < b.1 ∨ a.1 = b.1
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (default, x)) ((fun x ↦ (ofLex x).2) (toLex (a, b))) = toLex (a, b)

Tactic:
simpa using

Goal state after:
α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ default = a
Module: Mathlib.Order.SuccPred.CompleteLinearOrder

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False

Tactic:
simpa using

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
hx : ¬IsSuccPrelimit (sSup (Iio x))
⊢ False
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
a : Cardinal.{max u v}
f : ι → Cardinal.{max u v}
⊢ a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
simpa using

Goal state after:
ι : Type u
a : Cardinal.{max u v}
f : ι → Cardinal.{max u v}
⊢ a ^ sum f = prod fun i ↦ a ^ f i
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ

Tactic:
simpa using

Goal state after:
α : Type u_1
x✝ : α
⊢ IsFixedPt id x✝
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa using

Goal state after:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.InvOn f g (fixedPoints (g ∘ f)) (fixedPoints (g ∘ f))
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa using

Goal state after:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn f (fixedPoints (g ∘ f)) (fixedPoints (g ∘ f))
Module: Mathlib.Dynamics.FixedPoints.Basic

Goal state before:
pp: α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (f ∘ g)) (fixedPoints (f ∘ g))

Tactic:
simpa using

Goal state after:
α : Type u_1
f g : α → α
h : Function.Commute f g
⊢ Set.BijOn g (fixedPoints (g ∘ f)) (fixedPoints (g ∘ f))
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
a : α
hs : IsUpperSet s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, ∀ c ∈ {a}, b ≤ c → b ∈ {a}

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : LE α
s : Set α
a : α
hs : IsUpperSet s
has : ∀ b ∈ s, b ≤ a → b = a
⊢ ∀ b ∈ s, b ≤ a → b = a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
⊢ ∃ a, f a = x

Tactic:
obtain (rfl | h) := (trichotomous y x).resolve_left hs

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
y : β
hy : y ∈ Set.range ⇑f
IH : ∀ (y_1 : β), s y_1 y → ∃ a, f a = y_1
hs : ¬s y y
⊢ ∃ a, f a = y

case inl.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsLowerSet s
⊢ sᶜ = univᶜ ∨ ∃ a, sᶜ = (Iio a)ᶜ

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsLowerSet s
⊢ s = univ ∨ ∃ a, sᶜ = Ici a
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ b ∈ ⇑f.toRelEmbedding '' Set.univ

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
f : r ≺i s
b : β
h : b ∈ {b | s b f.top}
⊢ ∃ y, f.toRelEmbedding y = b
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Monotone g
⊢ Monotone fun x ↦ map f (g x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Monotone g
⊢ Monotone fun x ↦ (g x).bind fun y ↦ Part.some (f y)
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Antitone g
⊢ Antitone fun x ↦ map f (g x)

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : β → γ
g : α → Part β
hg : Antitone g
⊢ Antitone fun x ↦ (g x).bind fun y ↦ Part.some (f y)
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ o.get ⋯ = a ↔ a ∈ o
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
⊢ lfp (lfp.comp h) = lfp h.onDiag

Tactic:
let a := (lfp.comp h).lfp

Goal state after:
α : Type u
inst✝ : CompleteLattice α
h : α →o α →o α
a : α := lfp (lfp.comp h)
⊢ lfp (lfp.comp h) = lfp h.onDiag
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
inst✝ : Div α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma / mb ∈ a / b

Tactic:
by simp [div_def]; aesop

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
this : ChainClosure r (⋃₀ ∅)
⊢ ChainClosure r ∅
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:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α → β
c : Chain α
hf : ωScottContinuous f
⊢ IsLUB (f '' Set.range ⇑c) (f (ωSup c))
Module: Mathlib.Order.Zorn

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ s, a ∈ s ∧ b ∈ s

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ ∃ s, a ∈ s ∧ b ∈ s
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x ↦ f x a
c : Chain γ
a : α
⊢ f (ωSup c) a = ωSup (c.map { toFun := f, monotone' := ⋯ }) a

Tactic:
apply (hf a).map_ωSup c

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.h₁
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ f (c i) ≤ f (c.toOrderHom (max i j))

Tactic:
apply hf.monotone (c.monotone le_sup_left)

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

Goal state before:
pp: α✝ β✝ : Type u
a b : Cardinal.{u}
α β : Type u
⊢ #α * #β = 0 → #α = 0 ∨ #β = 0

Tactic:
simpa using

Goal state after:
α✝ β✝ : Type u
a b : Cardinal.{u}
α β : Type u
⊢ IsEmpty α ∨ IsEmpty β → IsEmpty α ∨ IsEmpty β
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ a ≤ a ^ b

Tactic:
by
  rcases eq_or_ne a 0 with (rfl | ha)
  · exact zero_le
  · convert! power_le_power_left ha hb
    exact (power_one a).symm

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

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 ↦ x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ c ≤ j

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun x1 x2 ↦ x1 < x2) c
h_1 : (j : ι) → Quotient.out (f ⟨c, hc⟩) ↪ Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun x1 x2 ↦ x1 < x2) j
this : #(Quotient.out (f ⟨c, hc⟩)) ≤ #(Quotient.out (f ⟨j, hj⟩))
⊢ c ≤ j
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
a b : ULift.{u, v} (Quotient.out (f i))
h : (fun a ↦ ⟨i, a.down⟩) a = (fun a ↦ ⟨i, a.down⟩) b
⊢ a = b

Tactic:
simpa using

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
a b : ULift.{u, v} (Quotient.out (f i))
h : (fun a ↦ ⟨i, a.down⟩) a = (fun a ↦ ⟨i, a.down⟩) b
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
i : ι
⊢ f i ≤ sum f

Tactic:
simpa using

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
i : ι
⊢ f i ≤ sum f
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h : ¬∃ i, Surjective fun x ↦ ↑x i
⊢ ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y

Tactic:
simpa using

Goal state after:
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h : ¬∃ i, Surjective fun x ↦ ↑x i
⊢ ∀ (i : ι), ∃ y, ∀ x ∈ s, ¬x i = y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G ⟨i, a⟩ i ≠ C i
⊢ False

Tactic:
let ⟨⟨i, a⟩, h⟩ := sG C

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
x✝ : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) := invFun ⇑F
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G ⟨i, a⟩ i ≠ C i
i : ι
a : Quotient.out (f i)
h : G ⟨i, a⟩ = C
⊢ False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c

Tactic:
simpa using

Goal state after:
c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a

Tactic:
simpa using

Goal state after:
a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a
Module: Mathlib.SetTheory.Cardinal.ToNat

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

Tactic:
simpa using

Goal state after:
case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ ↑(toNat c) ↔ ↑n ≤ ↑(toNat d)
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ x.toENatAux ≠ 0

pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y

Tactic:
· rwa [Ne, toENatAux_eq_zero]

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
rw [← h.comp_eq, MonoidHom.comp_apply]

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

Goal state before:
pp: α β : Type u
a x : Cardinal.{u}
hx : x ∈ Iic #(Quotient.out a)
⊢ ∃ a_1, (fun x ↦ ⟨#↑x, ⋯⟩) a_1 = ⟨x, hx⟩

Tactic:
simpa using

Goal state after:
α β : Type u
a x : Cardinal.{u}
hx : x ∈ Iic #(Quotient.out a)
⊢ ∃ a_1, #↑a_1 = x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x ↦ ↑(e.symm x)

Tactic:
simpa using

Goal state after:
case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x ↦ ↑(e.symm x)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ i, f i

Tactic:
simpa using

Goal state after:
ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{max u v, u} #ι * ⨆ i, f i
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * ⨆ i, f i

Tactic:
simpa using

Goal state after:
ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * ⨆ i, f i
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Tactic:
simpa using

Goal state after:
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Fintype.card α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑(n + 1) ≤ #α

Tactic:
simpa using

Goal state after:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑n < #α
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c < 1 ↔ c = 0
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
simpa using

Goal state after:
c : Cardinal.{u_1}
⊢ c ≤ 1 ↔ c = 0 ∨ c = 1
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ 1 < ℵ₀

Tactic:
simpa using

Goal state after:
⊢ 1 < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 • a < ℵ₀ ↔ 0 = 0 ∨ a < ℵ₀

Tactic:
simpa using

Goal state after:
a : Cardinal.{u_1}
⊢ 0 < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
rw [← Ne, ← Cardinal.one_le_iff_ne_zero] at ha hb

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑s = 0 ↔ s = ∅

Tactic:
mk_eq_zero_iff,

Goal state after:
α : Type u
s : Set α
⊢ IsEmpty ↑s ↔ s = ∅
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s

Tactic:
simpa using

Goal state after:
α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case mp
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ ∃ t, ↑t = ↑s ∧ t.card = n

Tactic:
simpa using

Goal state after:
case mp
α : Type u_1
n : ℕ
s : Finset α
h : #↑↑s = ↑n
⊢ s.card = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n

Tactic:
simpa using

Goal state after:
α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this✝ : Fintype ↑A
this : Fintype ↑B
⊢ #↑A < #↑B

Tactic:
simpa using

Goal state after:
α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
this✝ : Fintype ↑A
this : Fintype ↑B
⊢ Fintype.card ↑A < Fintype.card ↑B
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S : Set α
h : #↑S < #↑univ
⊢ Sᶜ.Nonempty

Tactic:
simpa using

Goal state after:
α : Type u
S : Set α
h : #↑S < #↑univ
⊢ (univ \ S).Nonempty
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α ≃ β
s : Set β
⊢ #↑(⇑f ⁻¹' s) = #↑s

Tactic:
simpa using

Goal state after:
α β : Type u
f : α ≃ β
s : Set β
⊢ #↑(⇑f ⁻¹' s) = #↑s
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
simpa using

Goal state after:
α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ

Tactic:
simpa using

Goal state after:
α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ {x, y} = univ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ↑3 ≤ #α

Tactic:
simpa using

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
⊢ 3 ≤ #α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
simpa using

Goal state after:
α : Type u_1
h : 3 ≤ #α
x y : α
this✝¹ : ↑3 ≤ #α
this✝ : ↑2 < #α
this : ∃ z, z ∉ [x, y]
⊢ ∃ z, ¬z = x ∧ ¬z = y
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : FaithfulSMul M α
inst✝ : Nonempty β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
b : β
a : α
⊢ m₁✝ • a = m₂✝ • a

Tactic:
injection h (a, b)

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : Nonempty α
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
a : α
b : β
⊢ m₁✝ • b = m₂✝ • b

Tactic:
injection h (a, b)

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
x : G
⊢ x • 0 = 0

Tactic:
simpa using

Goal state after:
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
x : G
⊢ x • 0 = 0
Module: Mathlib.GroupTheory.GroupAction.DomAct.Basic

Goal state before:
pp: M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
this : DecidableEq α
h : (c₁ • update (const α x) (mk.symm c₂ • a) y) a = (c₂ • update (const α x) (mk.symm c₂ • a) y) a
⊢ x = y

Tactic:
simpa using

Goal state after:
M : Type u_1
β : Type u_2
α : Type u_3
N : Type u_4
inst✝² : SMul M α
inst✝¹ : FaithfulSMul M α
inst✝ : Nontrivial β
c₁ c₂ : Mᵈᵐᵃ
a : α
x y : β
hne : mk.symm c₁ • a ≠ mk.symm c₂ • a
this : DecidableEq α
h : (c₁ • update (const α x) (mk.symm c₂ • a) y) a = (c₂ • update (const α x) (mk.symm c₂ • a) y) a
⊢ x = y
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
x y : M₂
⊢ g (f (g (x + y))) = g x + g y

Tactic:
← h₁ (g x + g y)

Goal state after:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module S M₂
σ : R →+* S
σ' : S →+* R
inst✝ : RingHomInvPair σ σ'
f : M →ₛₗ[σ] M₂
g : M₂ → M
h₁ : ∀ (x : M), g (f x) = x
h₂ : ∀ (x : M₂), f (g x) = x
x y : M₂
⊢ g (f (g (x + y))) = g (f (g x + g y))