mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤

Tactic:
induction a

Goal state after:
case top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ ⊤ = ⊤ ∧ b ≠ ⊤

case coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
b : WithTop α
a✝ : α
⊢ ↑a✝ - b = ⊤ ↔ ↑a✝ = ⊤ ∧ b ≠ ⊤
Module: Mathlib.Algebra.Order.Sub.WithTop

Goal state before:
pp: case top
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤

pp: case coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
a✝ : α
⊢ x - ↑a✝ ≤ z ↔ x ≤ z + ↑a✝

Tactic:
· cases z <;> simp

Goal state after:
case coe
α : Type u_1
β : Type u_2
inst✝⁴ : Add α
inst✝³ : LE α
inst✝² : OrderBot α
inst✝¹ : Sub α
inst✝ : OrderedSub α
x z : WithTop α
a✝ : α
⊢ x - ↑a✝ ≤ z ↔ x ≤ z + ↑a✝
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R✝ : Type u_1
R' : Type u_2
M : Type u_3
X : Type u_4
inst✝¹⁷ : Monoid M
S : Submonoid M
inst✝¹⁶ : OreSet S
inst✝¹⁵ : MulAction M X
inst✝¹⁴ : SMul R✝ X
inst✝¹³ : SMul R✝ M
inst✝¹² : IsScalarTower R✝ M M
inst✝¹¹ : IsScalarTower R✝ M X
inst✝¹⁰ : SMul R' X
inst✝⁹ : SMul R' M
inst✝⁸ : IsScalarTower R' M M
inst✝⁷ : IsScalarTower R' M X
inst✝⁶ : SMul R✝ R'
inst✝⁵ : IsScalarTower R✝ R' M
R : Type ?u.51
inst✝⁴ : Monoid R
inst✝³ : MulAction R M
inst✝² : IsScalarTower R M M
inst✝¹ : MulAction R X
inst✝ : IsScalarTower R M X
s₁ s₂ : R
x : OreLocalization S X
⊢ (s₁ * s₂) • x = s₁ • s₂ • x

Tactic:
by rw [← smul_eq_mul, smul_assoc]

Goal state after:
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : CommMonoid R
S : Submonoid R
inst✝ : OreSet S
r₁ r₂ : R
s₁ s₂ : ↥S
⊢ ↑s₂ * r₁ = r₁ * ↑s₂

Tactic:
by simp [mul_comm]

Goal state after:
Module: Mathlib.Order.Iterate

Goal state before:
pp: case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x (n + 1) < y (n + 1)

Tactic:
suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)

Goal state after:
case succ
α : Type u_1
inst✝ : Preorder α
f : α → α
x y : ℕ → α
hf : Monotone f
h₀ : x 0 ≤ y 0
n : ℕ
ihn : 0 < n → (∀ (k : ℕ), k < n → x (k + 1) < f (x k)) → (∀ (k : ℕ), k < n → f (y k) ≤ y (k + 1)) → x n < y n
hn : 0 < n + 1
hx : ∀ (k : ℕ), k < n + 1 → x (k + 1) < f (x k)
hy : ∀ (k : ℕ), k < n + 1 → f (y k) ≤ y (k + 1)
⊢ x n ≤ y n
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ 0 = unbotD 0 a * 0

Tactic:
mul_zero

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ 0 = 0
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ 0 = unbotD 0 ↑a✝ * 0

Tactic:
mul_zero

Goal state after:
case neg.coe.bot
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a✝ : α
ha : ¬↑a✝ = 0
hb : ¬⊥ = 0
⊢ 0 = 0
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
h : n ≤ m
⊢ succ^[n] r ≤ succ^[m] r

Tactic:
obtain ⟨k, rfl⟩ := Nat.exists_eq_add_of_le h

Goal state after:
α✝ : Type u_1
inst✝³ : Preorder α✝
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[n + k] r
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ a < succ a

Tactic:
simpa using (hn h a).not

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : LinearOrder α
succ : α → α
hn : ∀ {a : α}, ¬IsMax a → ∀ (b : α), a < b ↔ succ a ≤ b
hm : ∀ (a : α), IsMax a → succ a = a
a : α
h : ¬IsMax a
⊢ ¬succ a ≤ a

Tactic:
simpa using (hn h a).not

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

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
⊢ b ≤ succ a

Tactic:
by
  obtain hab | ⟨-, hba⟩ := h.covBy_or_le_and_le
  · by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba
  · exact hba.trans (le_succ _)

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a < b
h₂ : ¬IsMax b
⊢ Ioo a (succ b) = insert b (Ioo a b)

Tactic:
by
  simp_rw [← Iio_inter_Ioi, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ioi.2 h₁)]

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

Goal state before:
pp: α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a ≤ ⊥ ↔ a = ⊥

Tactic:
le_bot_iff

Goal state after:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : SuccOrder α
a : α
inst✝¹ : OrderBot α
inst✝ : NoMaxOrder α
⊢ a = ⊥ ↔ a = ⊥
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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)
⊢ MonotoneOn f s

Tactic:
by
  rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_succ_iterate_of_le hab
  clear hab
  induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at hb ⊢
    have : succ^[n] a ∈ s := hs.1 ha hb ⟨le_succ_iterate .., le_succ _⟩
    by_cases hb' : IsMax (succ^[n] a)
    · rw [succ_eq_iff_isMax.2 hb']
      exact hn this
    · exact (hn this).trans (hf _ hb' this hb)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a : WithTop α
ha : a ≠ ⊤
⊢ pred a ≠ ⊤

Tactic:
induction a

Goal state after:
case top
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
ha : ⊤ ≠ ⊤
⊢ pred ⊤ ≠ ⊤

case coe
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderTop α
inst✝ : PredOrder α
a✝ : α
ha : ↑a✝ ≠ ⊤
⊢ pred ↑a✝ ≠ ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Sigma

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
r : Finset (α × γ)
s : Finset γ
t : γ → Finset α
h : ∀ (p : α × γ), p ∈ r ↔ p.2 ∈ s ∧ p.1 ∈ t p.2
f : α × γ → β
⊢ ∏ p ∈ r, f p = ∏ c ∈ s, ∏ a ∈ t c, f (a, c)

Tactic:
refine Eq.trans ?_ (prod_sigma s t fun p => f (p.2, p.1))
  apply prod_equiv ((Equiv.prodComm _ _).trans (Equiv.sigmaEquivProd _ _).symm) <;> simp [h]

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

Goal state before:
pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ image (fun i ↦ b ↑i) univ ⊆ (image b univ).erase k

pp: case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ

Tactic:
· rw [image_subset_iff]
    intro i _
    apply mem_erase_of_ne_of_mem i.2 (mem_image_of_mem _ (mem_univ _))

Goal state after:
case a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
k : β
b : α → β
⊢ (image b univ).erase k ⊆ image (fun i ↦ b ↑i) univ
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ f i * (s \ {i}).prod g = g i * ∏ x ∈ s \ {i}, g x ↔ f i = g i

Tactic:
mul_left_inj

Goal state after:
ι : Type u_1
M : Type u_3
s : Finset ι
inst✝¹ : CommMonoid M
inst✝ : IsRightCancelMul M
f g : ι → M
i : ι
hi : i ∈ s
hfg : ∀ j ∈ s, j ≠ i → f j = g j
⊢ f i = g i ↔ f i = g i
Module: Mathlib.Control.Applicative

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
α✝ β✝ : Type u_2
x✝¹ : Const α (α✝ → β✝)
x✝ : α✝
⊢ x✝¹ <*> pure x✝ = (fun h ↦ h x✝) <$> x✝¹

Tactic:
by simp [Const.map, map, Seq.seq, pure, mul_one]

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

Goal state before:
pp: α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ s = replicate n a ↔ ∀ b ∈ s, b = a

Tactic:
Subtype.ext_iff,

Goal state after:
α : Type u_1
n : ℕ
s : Sym α n
a : α
⊢ ↑s = ↑(replicate n a) ↔ ∀ b ∈ s, b = a
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Encodable α
v : ℕ
⊢ decodeList v.succ = (fun x1 x2 ↦ x1 :: x2) <$> decode (unpair v).1 <*> decode (unpair v).2

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Goal state after:
α : Type u_1
inst✝ : Encodable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = (fun x1 x2 ↦ x1 :: x2) <$> decode (v₁, v₂).1 <*> decode (v₁, v₂).2
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Goal state after:
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v : ℕ
⊢ decodeList v.succ = some (ofNat α (unpair v).1 :: ofNat (List α) (unpair v).2)

Tactic:
rcases e : unpair v with ⟨v₁, v₂⟩

Goal state after:
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
⊢ decodeList v.succ = some (ofNat α (v₁, v₂).1 :: ofNat (List α) (v₁, v₂).2)
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach = s

Tactic:
refine map_injective (Option.some_injective _) _ ?_

Goal state after:
case neg
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
s : Sym α n.succ
h : none ∉ decode (Sum.inr s)
⊢ map some (map (fun o ↦ (↑o).get ⋯) (decode (Sum.inr s)).attach) = map some s
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (⋃ i, t i).Countable

Tactic:
rw [iUnion_eq_range_psigma]

Goal state after:
α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
this : ∀ (i : ι), Countable ↑(t i)
⊢ (range fun a ↦ ↑a.snd).Countable
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Refl r
inst✝ : Std.Refl s
⊢ ∀ (a : α ⊕ β), Lex r s a a

Tactic:
rintro (a | a)
    exacts [Lex.inl (refl _), Lex.inr (refl _)]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : IsWellOrder α r
f : r ≺i r
h : r f.top f.top
⊢ False

Tactic:
exact _root_.irrefl _ h

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_4
a : α
⊢ (↑(Option.some a)).Dom ↔ (Option.some a).isSome = true

Tactic:
by simp [ofOption]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : x = some b
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x

Tactic:
Part.eq_some_iff

Goal state after:
case inr
α : Type u_1
x y z : Part α
hx : x ≤ z
hy : y ≤ z
b : α
h₀ : b ∈ x
b' : α
h₁ : b' ∈ y
⊢ b' ∈ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ Ici x → cSup c ∈ Ici x

Tactic:
intro c

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
⊢ ↑c ⊆ Ici x → cSup c ∈ Ici x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ bot x f → cSup c ∈ bot x f

Tactic:
intro c

Goal state after:
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
⊢ ↑c ⊆ bot x f → cSup c ∈ bot x f
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
f : α → α
H : ∀ (x : α), f x = x
o : Part α
⊢ map id o = o

Tactic:
exact id_map o

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ z ∨ f z ≤ f z

Tactic:
right; exact le_refl _

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
intro c

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
⊢ ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)} → cSup c ∈ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ ∀ (c : NonemptyChain α), ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}

Tactic:
intro c

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
⊢ ↑c ⊆ {y | IsExtremePt x f y} → cSup c ∈ {y | IsExtremePt x f y}
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 [Set.insert_subset_iff] using (IsChain.pair hab).exists_subset_flag

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

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

Tactic:
set h : α → β := s.piecewise f g'

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

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

Tactic:
simp only [Part.mem_bind_iff, Chain.coe_map,
      Function.comp_apply, OrderHom.partBind_coe]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
c₀ : Chain (α →𝒄 β)
c₁ : Chain α
z : β
h : ∀ (i : ℕ), (c₀ i) (c₁ i) ≤ z
i j : ℕ
⊢ (c₀ i) (c₁ (max i j)) ≤ (c₀ (max i j)) (c₁ (max i j))

Tactic:
· apply c₀.monotone
      apply le_max_left

Goal state after:
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
κ : φ.CompTriple ψ χ
⊢ ⇑ψ ∘ ⇑φ = ⇑χ

Tactic:
by rw [← MonoidHom.coe_comp, κ.comp_eq]

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

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

Tactic:
intro c

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
c : Cardinal.{max u_1 u}
⊢ c ∈ upperBounds (lift.{u, u_1} '' s) → lift.{u, u_1} (sSup s) ≤ c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : S.Infinite
⊢ #ℕ ≤ #↑S

Tactic:
have := Infinite.to_subtype h'

Goal state after:
S : Set ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
h' : S.Infinite
this : Infinite ↑S
⊢ #ℕ ≤ #↑S
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2
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 α
⊢ (fun x ↦ SMulCommClass M N α) = fun x ↦ SMulCommClass M N α

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 α
⊢ compHom α (MonoidHom.inr M N) = hN

pp: case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝

Tactic:
· funext; congr; ext m a; (conv_rhs => rw [← hN.one_smul a]); rfl

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 α
⊢ compHom α (MonoidHom.inr M N) = hN

case e_4.e_4
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 α
⊢ ⋯ ≍ snd✝
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: G : Type u''
S : Type u'
R : Type u
M : Type v
ι : Type w
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p✝ q p : Submodule R M
s : Set M
hs : s = ↑p
⊢ ∀ (c : R) {x : M}, x ∈ s → c • x ∈ s

Tactic:
by simpa [hs] using p.smul_mem'

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = c • e a

Tactic:
convert! e.toAddMonoidHom.map_zsmul c a using 1

Goal state after:
case e'_2
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ e (c • a) = e.toAddMonoidHom (c • a)

case e'_3
R : Type u_1
R₂ : Type u_2
K : Type u_3
S : Type u_4
M : Type u_5
M₁ : Type u_6
M₂ : Type u_7
M₃ : Type u_8
inst✝² : AddCommGroup M
inst✝¹ : AddCommGroup M₂
inst✝ : AddCommGroup M₃
modM : Module ℤ M
modM₂ : Module ℤ M₂
modM₃ : Module ℤ M₃
e : M ≃+ M₂
c : ℤ
a : M
⊢ c • e a = c • e.toAddMonoidHom a
Module: Mathlib.Algebra.Module.Submodule.Ker

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ f (x - y) = 0 ↔ f x = f y

Tactic:
map_sub,

Goal state after:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁵ : Ring R
inst✝⁴ : Ring R₂
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
x y : M
⊢ f x - f y = 0 ↔ f x = f y
Module: Mathlib.Algebra.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ p < comap f P

Tactic:
rw [← Submodule.map_lt_map_iff_of_injective hf]

Goal state after:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
inst✝ : RingHomSurjective σ₁₂
f : M →ₛₗ[σ₁₂] M₂
hf : Injective ⇑f
p q : Submodule R M
h : p ⋖ q
P : Submodule R₂ M₂
h₁ : map f p < P
h₂ : P < map f q
⊢ map f p < map f (comap f P)
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 = x✝ * 0

Tactic:
mul_zero

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝ : M₀
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = x✝¹ * 0

Tactic:
mul_zero

Goal state after:
M₀ : Type u_1
inst✝ : MulZeroClass M₀
x✝¹ x✝ : M₀
⊢ 0 = 0
Module: Mathlib.Algebra.GroupWithZero.Center

Goal state before:
pp: case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 = ↑u * 0

Tactic:
mul_zero

Goal state after:
case inl
G₀ : Type u_2
inst✝ : GroupWithZero G₀
u : G₀ˣ
hu : ∀ (g : G₀ˣ), g * u = u * g
⊢ 0 = 0
Module: Mathlib.Algebra.Ring.Center

Goal state before:
pp: case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = x✝¹ * 0

Tactic:
mul_zero

Goal state after:
case zero
M : Type u_1
inst✝ : NonAssocSemiring M
x✝¹ x✝ : M
⊢ 0 = 0
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f (a✝ * b✝) ∈ S

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup N
a✝ b✝ : M
ha : a✝ ∈ ⇑f ⁻¹' ↑S
hb : b✝ ∈ ⇑f ⁻¹' ↑S
⊢ f a✝ * f b✝ ∈ S
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f (x * y) = f x * f y

Tactic:
map_mul

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
σ : Type u_4
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
S✝ : Subsemigroup M
f : M →ₙ* N
S : Subsemigroup M
x : M
hx : x ∈ ↑S
y : M
hy : y ∈ ↑S
⊢ f x * f y = f x * f y
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : Semiring R
s : Set R
x : R
⊢ (∃ L, (∀ t ∈ L, ∀ y ∈ t, y ∈ s) ∧ (List.map List.prod L).sum = x) → x ∈ closure s

Tactic:
rintro ⟨L, HL1, rfl⟩
    exact
      list_sum_mem fun r hr =>
        let ⟨t, ht1, ht2⟩ := List.mem_map.1 hr
        ht2 ▸ list_prod_mem _ fun y hy => subset_closure <| HL1 t ht1 y hy

Goal state after: