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

Goal state before:
pp: 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 b : Y
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
refine (exists_succ_iterate_of_le ((map_inv_le_map_inv_iff f).mpr h)).imp ?_
    intro n
    rw [← f.apply_eq_iff_eq, EquivLike.apply_inv_apply]
    rintro rfl
    clear h
    induction n generalizing a with
    | zero => simp
    | succ n IH => simp only [Function.iterate_succ', Function.comp_apply, IH, f.map_succ]

Goal state after:
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: α : Type v
inst✝ : Subsingleton α
⊢ Small.{w, v} α

Tactic:
by
  rcases isEmpty_or_nonempty α with ⟨⟩
  · apply small_map (Equiv.equivPEmpty α)
  · apply small_map Equiv.punitOfNonemptyOfSubsingleton

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

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

Tactic:
[

Goal state after:
n : ℕ∞
hn : n ≠ ⊤
⊢ ∃ m, n < ↑m
Module: Mathlib.Data.ENat.Basic

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

Tactic:
[

Goal state after:
n : ℕ∞
hn : n ≠ ⊤
⊢ Injective fun x ↦ n + x
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + ↑1 ↔ n ≤ ↑m

Tactic:
← ENat.natCast_one,

Goal state after:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + ↑↑1 ↔ n ≤ ↑m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩

Tactic:
[

Goal state after:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
σ : α → Type u_6
s : Finset α
t : (a : α) → Finset (σ a)
f : Sigma σ → β
⊢ ∏ x ∈ s.sigma t, f x = ∏ a ∈ s, ∏ s ∈ t a, f ⟨a, s⟩
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z

Tactic:
[

Goal state after:
κ : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : Finset α
u : Finset κ
f : γ → α → κ → β
⊢ ∏ x ∈ s, ∏ y ∈ t, ∏ z ∈ u, f x y z = ∏ z ∈ u, ∏ x ∈ s, ∏ y ∈ t, f x y z
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

Tactic:
[

Goal state after:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, ¬p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)

Tactic:
[

Goal state after:
ι : Type u_1
M : Type u_3
γ : Type u_5
s : Finset ι
inst✝¹ : CommMonoid M
p : ι → Prop
inst✝ : DecidablePred p
f g : ι → γ
k : γ → M
h : ∀ x ∈ s, p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (f x)
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
⊢ ∀ i ∈ insert a s, ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
[

Goal state after:
case h
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
⊢ ∀ i ∈ insert a s, ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))

Tactic:
[

Goal state after:
α : Type u_1
n : ℕ
v : Vector α (n + 1)
⊢ v.reverse.toList.get (Fin.cast ⋯ 0) = v.toList.get (Fin.cast ⋯ (Fin.last n))
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:
have i0 : i = 0 := Fin.eq_zero _
    simp [scanl_singleton, i0, get_zero]; simp [get_eq_get_toList]

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

Goal state before:
pp: α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f i = f a * ∏ i, f ↑i

Tactic:
[

Goal state after:
α : Type u_1
M : Type u_4
inst✝² : Fintype α
inst✝¹ : CommMonoid M
inst✝ : DecidableEq α
f : α → M
a : α
⊢ ∏ i, f i = f a * ∏ i, f ↑i
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ ↑(replicate (↑m.fst) a) ∧ a ≠ b
⊢ False

Tactic:
Sym.mem_coe,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
b : α
hb : b ∈ replicate (↑m.fst) a ∧ a ≠ b
⊢ False
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
obtain ⟨f, hf⟩ := Infinite.natEmbedding s hs

Goal state after:
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite
Module: Mathlib.Logic.Small.Set

Goal state before:
pp: α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst✝¹ : Small.{u, u1} ↑s
inst✝ : Small.{u, u2} ↑t
⊢ Small.{u, u3} ↑(Set.image2 f s t)

Tactic:
rw [← Set.image_uncurry_prod]
  infer_instance

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

Goal state before:
pp: case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x

Tactic:
[

Goal state after:
case h
α : Type u_1
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : Fintype α
p : α → Prop
inst✝ : DecidablePred p
f : α → M
⊢ ∀ (x : α), x ∈ {x | p x}.toFinset ↔ p x
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α

Tactic:
[

Goal state after:
α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ Countable α
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)

Tactic:
simp! [cast, *, functor_norm]

Goal state after:
case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ pure nil = Comp.mk (pure (pure nil))
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝¹ : α
hab : r a₁✝ a₂✝¹
a₂✝ : α
hbc : r a₂✝¹ a₂✝
⊢ Lex r s (inl a₁✝) (inl a₂✝)

pp: case inl.sep
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a₁✝ a₂✝ : α
hab : r a₁✝ a₂✝
b✝ : β
⊢ Lex r s (inl a₁✝) (inr b✝)

pp: case inr.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
b₁✝ b₂✝¹ : β
hab : s b₁✝ b₂✝¹
b₂✝ : β
hbc : s b₂✝¹ b₂✝
⊢ Lex r s (inr b₁✝) (inr b₂✝)

pp: case sep.inr
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrans β s
a✝ : α
b✝ b₂✝ : β
hbc : s b✝ b₂✝
⊢ Lex r s (inl a✝) (inr b₂✝)

Tactic:
exacts [.inl (_root_.trans hab hbc), .sep _ _, .inr (_root_.trans hab hbc), .sep _ _]

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

Goal state before:
pp: case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (lift.{u, v} #α ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ #(f i)

Tactic:
[

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (lift.{u, v} #α ^ sum fun i ↦ #(f i)) = prod fun i ↦ #α ^ #(f i)
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ₗ β₁},
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) b ↔ a ≤ b

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝⁸ : LE α
inst✝⁷ : LE β
inst✝⁶ : LE γ
inst✝⁵ : LE α₁
inst✝⁴ : LE α₂
inst✝³ : LE β₁
inst✝² : LE β₂
inst✝¹ : LE γ₁
inst✝ : LE γ₂
a : α
b : β
c : γ
ea : α₁ ≃o α₂
eb : β₁ ≃o β₂
⊢ ∀ {a b : α₁ ⊕ₗ β₁},
    (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) a ≤ (ofLex.trans (((↑ea).sumCongr ↑eb).trans toLex)) b ↔ a ≤ b
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:
[

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
h : IsMin a
x : α
hb : f x ≤ f a
⊢ f a ≤ f x

Tactic:
rw [f.le_iff_le] at hb ⊢

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : PartialOrder α
f : α ≤i β
h : IsMin a
x : α
hb : x ≤ a
⊢ a ≤ x
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x : β
⊢ ScottContinuous (Function.const α x)

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
x : β
⊢ ScottContinuous (Function.const α x)
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.fst

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.fst
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.snd

Tactic:
[

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
⊢ ScottContinuous Prod.snd
Module: Mathlib.Data.Part

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

Tactic:
eq_iff_of_dom ha hb'

Goal state after:
α : Type u_1
a b : Part α
ha : a.Dom
hb' : b.Dom
hb : a = b
⊢ a = b
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption

Tactic:
[

Goal state after:
case pos
α : Type u_1
β : Type u_2
f : α → Part β
o : Part α
inst✝² : Decidable o.Dom
inst✝¹ : (a : α) → Decidable (f a).Dom
inst✝ : Decidable (o.bind f).Dom
h : o.Dom
⊢ (o.bind f).toOption = o.toOption.elim Option.none fun a ↦ (f a).toOption
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
  refine (lfp_le _ ?_).antisymm (lfp_le _ (Eq.le ?_))
  · exact lfp_le _ h.onDiag.map_lfp.le
  have ha : (lfp ∘ h) a = a := (lfp.comp h).map_lfp
  calc
    h a a = h a (h a).lfp := congr_arg (h a) ha.symm
    _ = (h a).lfp := (h a).map_lfp
    _ = a := ha

Goal state after:
Module: Mathlib.Data.Part

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

Tactic:
by simp [sdiff_def]; aesop

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : α →o β
⊢ ωScottContinuous ⇑f ↔ ∀ (c : Chain α), f (ωSup c) = ωSup (c.map f)

Tactic:
by
  rw [ωScottContinuous_iff_monotone_map_ωSup]
  exact exists_prop_of_true f.monotone'

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
c : Chain (Part α)
a : α
h : a ∈ Part.ωSup c
⊢ some a ∈ c

Tactic:
by
  simp only [Part.ωSup] at h; split_ifs at h with h_1
  · have h' := Classical.choose_spec h_1
    rw [← eq_some_iff] at h
    rw [← h]
    exact h'
  · rcases h with ⟨⟨⟩⟩

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

Goal state before:
pp: α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ (n + 1) = c ^ n * c

Tactic:
[

Goal state after:
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ (n + 1) = c ^ n * c
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : Type u
β : Type v
f✝ : α → β
g : β → α
hf✝ : Injective f✝
hg : Injective g
f : α → β
hf : Bijective f
right✝ : ∀ (a : α), True
⊢ ∃ h, Bijective h

Tactic:
exact ⟨f, hf⟩

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
this

Goal state after:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
this : (iterateChain (↑f) x h) n.succ = ((iterateChain (↑f) x h).map ↑f) n
⊢ ((iterateChain (↑f) x h).map ↑f) n ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ (iterateChain (↑f) x h) (n + 1) ≤ a

Tactic:
this

Goal state after:
case succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : f a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f) x h) n ≤ a
this : (iterateChain (↑f) x h) n.succ = f ((iterateChain (↑f) x h) n)
⊢ f ((iterateChain (↑f) x h) n) ≤ a
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 * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
simp only [toENatAux_eq_top hy]
        rw [toENatAux_eq_top, ENat.mul_top]
        · rwa [Ne, toENatAux_eq_zero]
        · exact le_mul_of_one_le_of_le (Cardinal.one_le_iff_ne_zero.2 hx) hy

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

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

Tactic:
[

Goal state after:
c' : Cardinal.{u}
c : ℕ∞
⊢ toENat ↑c ≤ toENat c' ↔ ↑c ≤ c'
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
[

Goal state after:
c : Cardinal.{u}
c' : ℕ
⊢ toENat c ≤ toENat ↑c' ↔ c ≤ ↑c'
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

Tactic:
[

Goal state after:
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
rintro ⟨ab, ba⟩
    exact ⟨ba.of_mul, ab.of_mul⟩

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

Goal state before:
pp: case refine_2
s : Set Cardinal.{u_1}
h : s = ∅ ∨ ∃ a ∈ s, a = 0
⊢ sInf s = 0

Tactic:
· rcases h with rfl | ⟨a, ha, rfl⟩
    · exact Cardinal.sInf_empty
    · exact eq_bot_iff.2 (csInf_le' ha)

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
[

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f

Tactic:
[

Goal state after:
case e'_3
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ (range fun i ↦ lift.{u, v} (f i)) = lift.{u, v} '' range f
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
[

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬lift.{u, u_1} (sSup s) ≤ lift.{u, u_1} d
⊢ False
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
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = (1, n) • (m, 1) • a

Tactic:
[

Goal state after:
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
x✝ : MulAction (M × N) α
instM : MulAction M α := compHom α (MonoidHom.inl M N)
instN : MulAction N α := compHom α (MonoidHom.inr M N)
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = (1, n) • (m, 1) • a
Module: Mathlib.Algebra.Module.Hom

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m

Tactic:
[

Goal state after:
R : Type u_1
S✝ : Type u_2
M✝ : Type u_3
A : Type u_4
B : Type u_5
S : Type u_6
M : Type u_7
M₂ : Type u_8
inst✝³ : Semiring S
inst✝² : AddCommMonoid M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module S M
s s' : Sᵈᵐᵃ
f : M →+ M₂
m : M
⊢ ((s + s') • f) m = (s • f + s' • f) m
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst✝¹ : RingHomInvPair σ₂₃ σ₃₂
inst✝ : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ f ∘ₛₗ f' ∘ₛₗ h = h

Tactic:
[

Goal state after:
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
inst✝⁸ : Semiring R₁
inst✝⁷ : Semiring R₂
inst✝⁶ : Semiring R₃
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
f : M₂ →ₛₗ[σ₂₃] M₃
σ₃₂ : R₃ →+* R₂
inst✝¹ : RingHomInvPair σ₂₃ σ₃₂
inst✝ : RingHomCompTriple σ₁₃ σ₃₂ σ₁₂
h : M₁ →ₛₗ[σ₁₃] M₃
f' : M₃ →ₛₗ[σ₃₂] M₂
hf' : f ∘ₛₗ f' = id
⊢ f ∘ₛₗ f' ∘ₛₗ h = h
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Injective (⇑g ∘ ⇑f)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Injective (⇑g ∘ ⇑f)
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Surjective (⇑g ∘ ⇑f)

Tactic:
[

Goal state after:
R : Type u_1
S : Type u_5
M : Type u_8
M₂ : Type u_10
inst✝⁶ : Semiring R
inst✝⁵ : Semiring S
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 : g ∘ₛₗ f = id
⊢ Surjective (⇑g ∘ ⇑f)
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 R₂
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₂
inst✝⁵ : Module R M
inst✝⁴ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝³ : DistribSMul S M₂
inst✝² : SMulCommClass R₂ S M₂
inst✝¹ : DistribSMul T M₂
inst✝ : SMulCommClass R₂ T M₂
a : S
f : M →ₛₗ[σ₁₂] M₂
x y : M
⊢ (a • ⇑f) (x + y) = (a • ⇑f) x + (a • ⇑f) y

Tactic:
by simp only [Pi.smul_apply, f.map_add, smul_add]

Goal state after: