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

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ Pow.pow a 0 = 1

Tactic:
Pow.pow

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n : ℕ
a : WithTop α
⊢ (match a, 0 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    1
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ Pow.pow a (n + 1) = Pow.pow a n * a

Tactic:
Pow.pow

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : WithTop α
n✝ n : ℕ
a : WithTop α
⊢ (match a, n + 1 with
    | Option.some a, n => ↑(a ^ n)
    | none, 0 => 1
    | none, _n.succ => ⊤) =
    (match a, n with
      | Option.some a, n => ↑(a ^ n)
      | none, 0 => 1
      | none, _n.succ => ⊤) *
      a
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) a n₂

Tactic:
b

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 < x2) a b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 < x2) a n₂

Tactic:
b

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLT α
x : WithBot α
x0 : 0 ≤ x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 < x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 < x2) a b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) a n₂

Tactic:
b

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ a) ((fun x y ↦ ↑x * y) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 ≤ x2) a b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a : WithBot α
⊢ ∀ {n₂ : WithBot α},
    (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ n₂) → (fun x1 x2 ↦ x1 ≤ x2) a n₂

Tactic:
b

Goal state after:
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : MulPosReflectLE α
x : WithBot α
x0 : 0 < x
a b : WithBot α
⊢ (fun x1 x2 ↦ x1 ≤ x2) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ a) ((fun x y ↦ y * ↑x) ⟨x, x0⟩ b) → (fun x1 x2 ↦ x1 ≤ x2) a b
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case inr
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α
n m : ℕ
this :
  ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] {r : α} (n m : ℕ),
    n ≤ m → succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r
h : ¬n ≤ m
⊢ succ^[n] r ≤ succ^[m] r ∨ succ^[m] r ≤ succ^[n] r

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 ∨ succ^[m] r ≤ succ^[n] r

Tactic:
· rw [Or.comm]
    apply this
    exact Nat.le_of_not_ge h

Goal state after:
α✝ : 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 ∨ succ^[m] r ≤ succ^[n] r
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
⊢ IsSuccPrelimit ↑a

Tactic:
by
  intro b hb
  have := ha ⟨b, hs hb.le a.2⟩
  rw [not_covBy_iff] at this
  · obtain ⟨c, hc, hc'⟩ := this
    exact hb.2 hc hc'
  · exact hb.lt

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

Goal state before:
pp: α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ 0 < j

Tactic:
apply Nat.pos_of_ne_zero

Goal state after:
α : Type u_1
inst✝⁴ : Nontrivial α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
h : ∀ (i : α), P (succ i)
j : ℕ
hi : Order.succ^[j] ⊥ ≠ ⊥
⊢ j ≠ 0
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
le_succ_iff_eq_or_le,

Goal state after:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
a : α
inst✝ : OrderBot α
⊢ a = succ ⊥ ∨ a ≤ ⊥ ↔ a = ⊥ ∨ a = succ ⊥
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : PartialOrder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ succ y < x

Tactic:
exact hx.succ_lt hy

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ ⟨c, hc⟩ = ⟨b, hb⟩

pp: case neg.h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩

Tactic:
· simp only [Order.pred_eq_iff_isMin] at this
          apply (this.eq_of_le _).symm
          exact hbc

Goal state after:
case neg.h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case neg.h
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred ⟨c, hc⟩ = ⟨c, hc⟩

Tactic:
· exact this

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a : WithTop α
⊢ a ≤
    match a with
    | none => ⊤
    | Option.some a => if succ a = a then ⊤ else ↑(succ a)

Tactic:
by
    obtain - | a := a
    · exact le_top
    change _ ≤ ite _ _ _
    split_ifs
    · exact le_top
    · exact coe_le_coe.2 (le_succ a)

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : ↑(succ a✝) ≤ ↑a✝
⊢ IsMax ↑a✝

Tactic:
rw [coe_le_coe, succ_le_iff_isMax, ← succ_eq_iff_isMax] at ha

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : (a : α) → Decidable (succ a = a)
a✝ : α
ha' : ¬succ a✝ = a✝
ha : succ a✝ = a✝
⊢ IsMax ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: n : ℕ∞
hn : n ≠ ⊤
a : ℕ∞
⊢ ∀ ⦃a₂ : ℕ∞⦄, (fun x ↦ x + n) a = (fun x ↦ x + n) a₂ → a = a₂

Tactic:
b

Goal state after:
n : ℕ∞
hn : n ≠ ⊤
a b : ℕ∞
⊢ (fun x ↦ x + n) a = (fun x ↦ x + n) b → 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_1 ∈ s, b_1 ≠ a → (if h : b_1 = a then b b_1 h else 1) = 1

Tactic:
intro _ _ h
      rw [dif_neg]
      exact h

Goal state after:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s with x ∈ t, f x) * ∏ x ∈ s with x ∉ t, g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x

Tactic:
filter_mem_eq_inter,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s t : Finset ι
f g : ι → M
⊢ (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s with x ∉ t, g x = (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, g x
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case h.inr
α : 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 : α
hi : i ∈ s
⊢ ↑((g'.trans (Equiv.swap ⟨f a, hfat⟩ (g' a))) i) = f i

Tactic:
rw [Equiv.trans_apply, Equiv.swap_apply_of_ne_of_ne, hg' _ hi]

Goal state after:
case h.inr.a
α : 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 : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

case h.inr.a
α : 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 : α
hi : i ∈ s
⊢ g' i ≠ g' a
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ ∏ a with a ∈ s, f a = ∏ i ∈ s, f i

Tactic:
filter_mem_eq_inter,

Goal state after:
α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ ∏ a ∈ univ ∩ s, f a = ∏ i ∈ s, f i
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
⊢ Injective fun f ↦ f.toFun

Tactic:
rintro ⟨f, hf⟩ ⟨g, hg⟩ h

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
f : r ↪r s
hf : ∀ (a : α) (b : β), s b (f a) → b ∈ Set.range ⇑f
g : r ↪r s
hg : ∀ (a : α) (b : β), s b (g a) → b ∈ Set.range ⇑g
h :
  (fun f ↦ f.toFun) { toRelEmbedding := f, mem_range_of_rel' := hf } =
    (fun f ↦ f.toFun) { toRelEmbedding := g, mem_range_of_rel' := hg }
⊢ { toRelEmbedding := f, mem_range_of_rel' := hf } = { toRelEmbedding := g, mem_range_of_rel' := hg }
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
⊢ Surjective ⇑f

Tactic:
b

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
b : β
⊢ ∃ a, f a = b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a b : WithBot α
⊢ ((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) a ≤
      ((Equiv.optionEquivSumPUnit α).trans ((Equiv.sumComm α PUnit).trans toLex)) b ↔
    a ≤ b

Tactic:
by
    simp only [Equiv.optionEquivSumPUnit, Option.elim, Equiv.trans_apply, Equiv.coe_fn_mk,
      Equiv.sumComm_apply, swap, Lex.toLex_le_toLex, le_refl]
    cases a <;> cases b
    · simp only [elim_inr, lex_inl_inl, bot_le]
    · simp only [elim_inr, elim_inl, Lex.sep, bot_le]
    · simp only [elim_inl, elim_inr, lex_inr_inl, false_iff]
      exact not_coe_le_bot _
    · simp only [elim_inl, lex_inr_inr, coe_le_coe]

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ∀ a ∈ d, f a ≤ p₁

Tactic:
intro _ hb

Goal state after:
case right.left
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a✝ : α
hb : a✝ ∈ d
⊢ f a✝ ≤ p₁
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
⊢ ∀ a ∈ d, g a ≤ p₂

Tactic:
intro _ hb

Goal state after:
case right.right
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
D : Set (Set α)
f : α → β
g : α → γ
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
hf : ScottContinuousOn D f
hg : ScottContinuousOn D g
d : Set α
hd₁ : d ∈ D
hd₂ : d.Nonempty
hd₃ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
a : α
hda : IsLUB d a
p₁ : β
p₂ : γ
hp : ∀ a ∈ d, f a ≤ p₁ ∧ g a ≤ p₂
a✝ : α
hb : a✝ ∈ d
⊢ g a✝ ≤ p₂
Module: Mathlib.Data.Part

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

Tactic:
b

Goal state after:
case mp
β α : Type u_2
x : Part α
f : α → Part β
y : Part β
h : x >>= f ≤ y
a : α
h' : a ∈ x
b : β
⊢ b ∈ f a → b ∈ y
Module: Mathlib.SetTheory.Cardinal.Order

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

Tactic:
b

Goal state after:
case refine_1
α β : Type u
a 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:
b

Goal state after:
case refine_2
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ 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
n : ℕ
c : Cardinal.{u}
⊢ Pow.pow c (n + 1) = Pow.pow c n * c

Tactic:
Pow.pow

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

Goal state before:
pp: α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α

Tactic:
by
  rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]

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

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

Tactic:
· rintro ⟨y, hne, hy⟩
    exact ⟨x, y, hne.symm, eq_univ_of_forall fun z => or_iff_not_imp_left.2 (hy z)⟩

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a : ℕ
⊢ ∀ ⦃a₂ : ℕ⦄, ↑a = ↑a₂ → a = a₂

Tactic:
b

Goal state after:
R : Type u_2
S : Type u_3
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
ϕ : R →+* S
hϕ : Injective ⇑ϕ
hR : CharZero R
a b : ℕ
⊢ ↑a = ↑b → a = b
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₂
q : Submodule R₂ M₂
f₁ f₂ : M →ₛₗ[τ₁₂] M₂
⊢ comap f₁ q ⊓ comap f₂ q ≤ comap (f₁ + f₂) q

Tactic:
by
  simp only [SetLike.le_def, mem_comap, mem_inf, LinearMap.add_apply]
  exact fun _ h ↦ add_mem h.1 h.2

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

Goal state before:
pp: case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ a * c = c * a

Tactic:
ha c hc

Goal state after:
case inr
G₀ : Type u_2
inst✝ : GroupWithZero G₀
s : Set G₀
a : G₀
ha : a ∈ s.centralizer
ha₀ : a ≠ 0
c : G₀
hc : c ∈ s
⊢ a * c = a * c
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
⊢ ∀ (b : M) (x : ι), b ∈ S x → a * b = b * a

Tactic:
b

Goal state after:
ι : Sort u_1
M : Type u_2
inst✝ : Mul M
S : ι → Subsemigroup M
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : M
i : ι
ha : a ∈ S i
b : M
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
⊢ ∀ (b : R) (x : ι), b ∈ S x → a * b = b * a

Tactic:
b

Goal state after:
R : Type u
inst✝¹ : NonUnitalNonAssocSemiring R
ι : Sort u_2
inst✝ : Nonempty ι
S : ι → NonUnitalSubsemiring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
a : R
i : ι
ha : a ∈ S i
b : R
⊢ ∀ (x : ι), b ∈ S x → a * b = b * a
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
y : ↥s'
⊢ ((↑e.symm).restrict s s' ⋯) ((↑↑((↑e).restrict s' s ⋯)).toFun y) = y

Tactic:
simp [← Subtype.val_inj]

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

Goal state before:
pp: R✝ : Type u
S✝ : Type v
T : Type w
inst✝⁸ : NonAssocRing R✝
inst✝⁷ : NonAssocRing S✝
inst✝⁶ : NonAssocRing T
s✝ t : Subring R✝
R : Type u
S : Type v
inst✝⁵ : NonAssocSemiring R
inst✝⁴ : NonAssocSemiring S
σR : Type u_1
σS : Type u_2
inst✝³ : SetLike σR R
inst✝² : SetLike σS S
inst✝¹ : SubsemiringClass σR R
inst✝ : SubsemiringClass σS S
e : R ≃+* S
s' : σR
s : σS
h : ∀ (x : R), x ∈ s' ↔ e x ∈ s
x : ↥s
⊢ (↑↑((↑e).restrict s' s ⋯)).toFun (((↑e.symm).restrict s s' ⋯) x) = x

Tactic:
simp [← Subtype.val_inj]

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

Goal state before:
pp: case cons.inr
R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
h1 : C 1
hneg1 : C (-1)
hs : ∀ z ∈ s, ∀ (n : R), C n → C (z * n)
ha : ∀ {x y : R}, C x → C y → C (x + y)
h0 : C 0
hd : List R
HL : ∀ y ∈ hd, y ∈ s ∨ y = -1
L : List R
HL' : ∀ x ∈ L, x ∈ s
HP : hd.prod = -L.prod
⊢ C hd.prod

Tactic:
rw [HP]
    clear HP HL hd
    induction L with
    | nil => exact hneg1
    | cons hd tl ih =>
      rw [List.prod_cons, neg_mul_eq_mul_neg]
      rw [List.forall_mem_cons] at HL'
      exact hs _ HL'.1 _ (ih HL'.2)

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
x✝ : IsUnit q
v : Mˣ
hv : ↑v = q
⊢ ↑(v * u⁻¹) = p

Tactic:
simp [hv, hu.symm]

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

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
a : M
⊢ ∀ (b : M), p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
b

Goal state after:
M : Type u_1
inst✝ : CommMonoidWithZero M
p q : M
h : p ~ᵤ q
hp : Prime p
u : Mˣ
hu : p * ↑u = q
a b : M
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

Tactic:
exact hy.dvd

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

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a b : M
h : a ~ᵤ b
u : Mˣ
hu : a * ↑u = b
x✝ : IsUnit a
v : Mˣ
hv : ↑v = a
⊢ ↑(v * u) = b

Tactic:
simp [hv, hu.symm]

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

Goal state before:
pp: F : Type u_1
M₀ : Type u_2
M₀' : Type u_3
inst✝⁴ : MonoidWithZero M₀
inst✝³ : MonoidWithZero M₀'
inst✝² : FunLike F M₀ M₀'
inst✝¹ : NoZeroDivisors M₀'
inst✝ : MonoidWithZeroHomClass F M₀ M₀'
f : F
hf : Injective ⇑f
S : Submonoid M₀
hS : S ≤ M₀⁰
⊢ Submonoid.map f S ≤ M₀'⁰

Tactic:
by
  cases subsingleton_or_nontrivial M₀
  · simp [Subsingleton.elim S ⊥]
  · refine le_nonZeroDivisors_of_noZeroDivisors ?_
    rintro ⟨x, hx, hx0⟩
    exact zero_notMem_nonZeroDivisors <| hS <| map_eq_zero_iff f hf |>.mp hx0 ▸ hx

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

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a b : M
⊢ (∃ x, a * x ~ᵤ b) → ∃ c, b = a * c

Tactic:
rintro ⟨x, u, rfl⟩

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a x : M
u : Mˣ
⊢ ∃ c, a * x * ↑u = a * c
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
⊢ ∀ ⦃b c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂

Tactic:
b

Goal state after:
case mp
M : Type u_1
inst✝ : CommMonoid M
a : M
h : ∀ (a_1 a_2 : M), a ∣ a_1 * a_2 → ∃ x x_1, x ∣ a_1 ∧ x_1 ∣ a_2 ∧ Associates.mk a = Associates.mk (x * x_1)
b : M
⊢ ∀ ⦃c : M⦄, a ∣ b * c → ∃ a₁ a₂, a₁ ∣ b ∧ a₂ ∣ c ∧ a = a₁ * a₂