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

Goal state before:
pp: case zero
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : SuccOrder X
inst✝¹ : IsSuccArchimedean X
inst✝ : SuccOrder Y
f : X ≃o Y
a : Y
⊢ succ^[0] a = f (succ^[0] (EquivLike.inv f a))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
X : Type u_3
Y : Type u_4
inst✝⁴ : PartialOrder X
inst✝³ : PartialOrder Y
inst✝² : PredOrder X
inst✝¹ : IsPredArchimedean X
inst✝ : PredOrder Y
f : X ≃o Y
b : Y
⊢ pred^[0] b = f (pred^[0] (EquivLike.inv f b))

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
⊢ succ^[0] x = x + ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case h.zero
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[0] c = b
⊢ pred^[0] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
⊢ pred^[0] x = x - ↑0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
hin : ¬IsMax (succ^[0 - 1] i)
⊢ pred^[0] (succ^[0] i) = i

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
hb : succ^[0] a ∈ s
⊢ f a ≤ f (succ^[0] a)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x < 2 ↔ x ≤ 1

Tactic:
← one_add_one_eq_two,

Goal state after:
α : Type u_1
x : α
inst✝³ : LinearOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : NoMaxOrder α
⊢ x < 1 + 1 ↔ x ≤ 1
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case pos
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a ≤ f (succ a)
a : α
ha : a ∈ s
n : ℕ
hn : succ^[n] a ∈ s → f a ≤ f (succ^[n] a)
hb : succ (succ^[n] a) ∈ s
this : succ^[n] a ∈ s
hb' : IsMax (succ^[n] a)
⊢ f a ≤ f (succ^[n] a)

Tactic:
exact hn this

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

Goal state before:
pp: case succ.zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hab : ¬IsMax a
hb : succ^[0 + 1] a ∈ s
⊢ f a < f (succ^[0 + 1] a)

Tactic:
| zero =>

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

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

Tactic:
exact hn this

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

Goal state before:
pp: case zero
α : 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
ha : pred^[0] b ∈ s
⊢ f (pred^[0] b) ≤ f b

Tactic:
| zero =>

Goal state after:
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
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
this : pred^[n] b ∈ s
ha' : IsMin (pred^[n] b)
⊢ f (pred^[n] b) ≤ f b

Tactic:
exact hn this

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

Goal state before:
pp: n : ℕ∞
⊢ n < 2 ↔ n ≤ 1

Tactic:
← one_add_one_eq_two,

Goal state after:
n : ℕ∞
⊢ n < 1 + 1 ↔ n ≤ 1
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ x + n

Tactic:
intro a

Goal state after:
n : ℕ∞
hn : n ≠ ⊤
a : ℕ∞
⊢ ∀ ⦃a₂ : ℕ∞⦄, (fun x ↦ x + n) a = (fun x ↦ x + n) a₂ → a = a₂
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.zero
α : 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
ha : pred^[0 + 1] b ∈ s
⊢ f (pred^[0 + 1] b) < f b

Tactic:
| zero =>

Goal state after:
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^[n + 1] b) < f b

Tactic:
exact hn this

Goal state after:
Module: Mathlib.Data.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ update (∅.piecewise f g) i (f i) = update g i (f i)

Tactic:
piecewise_empty

Goal state after:
ι : Type u_1
π : ι → Sort u_2
f g : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
⊢ update g i (f i) = update g i (f i)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : a = b✝ then b b✝ h else 1) = 1

Tactic:
dif_neg

Goal state after:
case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ 1 = 1

case pos.h₀.hnc
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → a = x → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬a = b✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ (if h : b✝ = a then b b✝ h else 1) = 1

Tactic:
dif_neg

Goal state after:
case pos.h₀
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ 1 = 1

case pos.h₀.hnc
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
a : ι
b : (x : ι) → x = a → M
h✝ : a ∈ s
b✝ : ι
a✝ : b✝ ∈ s
h : b✝ ≠ a
⊢ ¬b✝ = a
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
f : (j : ι) → i = j → M
⊢ (∏ j, if h : i = j then f j h else 1) = f i ⋯

Tactic:
rw [Finset.prod_dite_eq, if_pos (mem_univ _)]

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

Goal state before:
pp: case zero
α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
⊢ Countable (Fin 0 → ℕ)

Tactic:
| zero =>

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

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
m✝ : Fin n
⊢ (ofFn v.get).get m✝ = v.get m✝

Tactic:
apply List.Vector.get_ofFn

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

Goal state before:
pp: case succ.zero
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α (0 + 1)
i : Fin (0 + 1)
⊢ (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
v : Vector α 0
⊢ C v

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
v : Vector α 0
w : Vector β 0
⊢ C v w

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
u : Vector α 0
v : Vector β 0
w : Vector γ 0
⊢ C u v w

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ {x ∈ T | x.length = s} ⊆ image List.ofFn univ

Tactic:
intro a

Goal state after:
α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
a : List α
⊢ a ∈ {x ∈ T | x.length = s} → a ∈ image List.ofFn univ
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
have h := unpair_right_le v

Goal state after:
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (unpair v).2 ≤ v
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤

Tactic:
rcases (Set.countable_iff_exists_surjective hne).1 hSc with ⟨s, hs⟩

Goal state after:
case mpr.inr
α : Type u
inst✝ : CompleteLattice α
p : α → Prop
h : ∃ x, p x
S : Set α
hSc : S.Countable
hps : ∀ s ∈ S, p s
hS : sSup S = ⊤
hne : S.Nonempty
s : ℕ → ↑S
hs : Surjective s
⊢ ∃ s, (∀ (n : ℕ), p (s n)) ∧ ⨆ n, s n = ⊤
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ y = (sumLexIioIci x) (toLex (Sum.inr ⟨y, h⟩))

Tactic:
sumLexIioIci_apply_inr

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
x y : α
h : x ≤ y
⊢ y = ↑⟨y, h⟩
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : LE α
inst✝¹ : LE β
inst✝ : OrderTop β
⊢ ∀ (a : α ⊕ₗ β), a ≤ inr ⊤

Tactic:
by
    rintro (a | b)
    · exact Lex.sep _ _
    · exact Lex.inr le_top

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

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ (f b → α) ≃ Quotient.out #(f b → α)

Tactic:
exact outMkEquiv.symm

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

Goal state before:
pp: case zero
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
⊢ ∀ (a₁ a₂ : α), (⇑f)^[0] (a₁ ⊔ a₂) ≤ (⇑f)^[0] a₁ ⊔ a₂

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB d a
⊢ IsLUB (Prod.fst '' d) a.1

Tactic:
simp only [isLUB_prod] at ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.fst '' d) a.1
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB d a
⊢ IsLUB (Prod.snd '' d) a.2

Tactic:
simp only [isLUB_prod] at ha

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
D : Set (Set (α × β))
d : Set (α × β)
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α × β
ha : IsLUB (Prod.fst '' d) a.1 ∧ IsLUB (Prod.snd '' d) a.2
⊢ IsLUB (Prod.snd '' d) a.2
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
⊢ ∀ (a : α), a ∈ x → f a ≤ y

Tactic:
intro a

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
⊢ a ∈ x → f a ≤ y
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

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

Goal state before:
pp: case neg
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
z : α
hz : z ∈ c
hzy : ¬z ≤ y
h' : f y ≤ z
⊢ f y ≤ cSup c

Tactic:
apply le_trans h' (le_cSup _ _ hz)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ (f x) (g x)

Tactic:
apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
⊢ Monotone fun x ↦ (f x) (g x)

α : 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 α
⊢ (f (ωSup c)) (g (ωSup c)) = ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ?m.25 })
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_1
α β : Type u
⊢ ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
intro a

Goal state after:
case refine_1
α β : Type u
a : Cardinal.{u}
⊢ ∀ (b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_2
α β : Type u
⊢ ∀ (a : Cardinal.{u}),
    ∀ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a,
      b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding

Tactic:
intro a

Goal state after:
case refine_2
α β : Type u
a : Cardinal.{u}
⊢ ∀ b < (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding a,
    b ∈ Set.range ⇑(OrderEmbedding.ofMapLEIff lift.{v, u} ⋯).ltEmbedding
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f

Tactic:
exact ⟨⟨fun a => ⟨i, a.down⟩, fun a b h => by simpa using h⟩⟩

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
ω : Cardinal.{v}
hω : ¬IsSuccPrelimit ω
h : ⨆ i, f i = ω
⊢ ∃ i, f i = ω

Tactic:
by
  subst h
  exact exists_eq_ciSup_of_not_isSuccPrelimit hω

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
⊢ (iterateChain (↑f) x h) 0 ≤ a

Tactic:
| zero =>

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : a ∈ fixedPoints ⇑f
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
mem_fixedPoints

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c = 1 ↔ c = 1

Tactic:
rw [toNat_eq_iff one_ne_zero, Nat.cast_one]

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

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ σ' (σ x) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq]

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ 0)

Tactic:
| zero =>

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

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

Tactic:
intro a

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

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ ↑n < ℵ₀

Tactic:
power_natCast,

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑m ^ n < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(image2 f s t) ≤ #↑s * #↑t

Tactic:
rw [← image_uncurry_prod, ← mk_setProd]

Goal state after:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(uncurry f '' s ×ˢ t) ≤ #↑(s ×ˢ t)
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
rw [← mk_univ (α := α)] at h
  simpa [Set.compl_eq_univ_sdiff] using sdiff_nonempty_of_mk_lt_mk h

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✝⁴ : Monoid M
inst✝³ : Monoid N
inst✝² : MulAction M α
inst✝¹ : MulAction N α
inst✝ : SMulCommClass M N α
x y : M × N
a : α
⊢ (x * y) • a = x • y • a

Tactic:
by
    change (x.1 * y.1) • (x.2 * y.2) • a = x.1 • x.2 • y.1 • y.2 • a
    rw [mul_smul, mul_smul, smul_comm y.1 x.2]

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

Goal state before:
pp: case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = SMul.smul n a

Tactic:
conv_rhs => rw [← hM.one_smul (SMul.smul n a)]

Goal state after:
case e_4.e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
n : N
a : α
⊢ SMul.smul n a = 1 • SMul.smul n a
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: case zero
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✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
module_M : Module R M
module_M₂ : Module S✝ M₂
σ : R →+* S✝
f : M →ₛₗ[σ] M₂
S : Type u_14
inst✝² : Semiring S
inst✝¹ : Module S M
inst✝ : Module S M₂
fₗ : M →ₗ[S] M₂
x : M
⊢ fₗ (0 • x) = 0 • fₗ x

Tactic:
| zero =>

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

Goal state before:
pp: M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
⊢ m₁✝ = m₂✝

Tactic:
cases subsingleton_or_nontrivial α

Goal state after:
case inl
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Subsingleton α
⊢ m₁✝ = m₂✝

case inr
M : Type u_1
α : Type u_2
inst✝¹ : MonoidWithZero α
inst✝ : IsLeftCancelMulZero α
m₁✝ m₂✝ : αᵐᵒᵖ
h : ∀ (a : α), m₁✝ • a = m₂✝ • a
h✝ : Nontrivial α
⊢ m₁✝ = m₂✝
Module: Mathlib.Algebra.Regular.Opposite

Goal state before:
pp: R : Type u_1
inst✝ : Mul R
a : R
⊢ IsRegular (op a) ↔ IsRegular a

Tactic:
simp [isRegular_iff, and_comm]

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
inst✝³ : Semiring R
inst✝² : Semiring S
inst✝¹ : AddCommMonoid M
inst✝ : Module S M
σ : Rᵐᵒᵖ →+* S
f g : R →ₛₗ[σ] M
h : f 1 = g 1
x : R
⊢ f x = g x

Tactic:
rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: case zero
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R₂
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R₂ M₂
σ₁₂ : R →+* R₂
f : M →ₛₗ[σ₁₂] M₂
g : End R M
g₂ : End R₂ M₂
h : g₂ ∘ₛₗ f = f ∘ₛₗ g
⊢ (g₂ ^ 0) ∘ₛₗ f = f ∘ₛₗ (g ^ 0)

Tactic:
| zero =>

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

Goal state before:
pp: case mem
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
p : ↑(toAddSubmonoid '' s)
x : M
hx : x ∈ ↑p
⊢ t • x ∈ ⨆ a, ↑a

Tactic:
| mem p x hx =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
⊢ t • 0 ∈ ⨆ a, ↑a

Tactic:
| zero =>

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
p : Submodule R M
h : ∀ x ∈ p, f' x ∈ p
x : M
hx : x ∈ p
⊢ (f' ^ 0) x ∈ p

Tactic:
| zero =>

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

Goal state before:
pp: S : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Semiring S
inst✝³ : Module S M
inst✝² : Module R M
inst✝¹ : SMul S R
inst✝ : IsScalarTower S R M
s t : Submodule R M
⊢ restrictScalars S (s ⊓ t) = restrictScalars S s ⊓ restrictScalars S t

Tactic:
by
  ext x; simp

Goal state after: