mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n✝ n : ℕ
a✝ : n < n✝
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n - f 0 + (f (n + 1) - f n)

Tactic:
tsub_add_eq_add_tsub h₂,

Goal state after:
M : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : PartialOrder M
inst✝⁴ : Sub M
inst✝³ : OrderedSub M
inst✝² : AddLeftMono M
inst✝¹ : AddLeftReflectLE M
inst✝ : ExistsAddOfLE M
f : ℕ → M
h : Monotone f
n✝ n : ℕ
a✝ : n < n✝
h₁ : f n ≤ f (n + 1)
h₂ : f 0 ≤ f n
⊢ f (n + 1) - f 0 = f n + (f (n + 1) - f n) - f 0
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ ∏ x, f x = f a

Tactic:
rw [prod_unique f, Subsingleton.elim default a]

Goal state after:
Module: Mathlib.GroupTheory.MonoidLocalization.Maps

Goal state before:
pp: M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
z : N
w v : P
⊢ (f.lift hg) z * w = v ↔ g (f.sec z).1 * w = g ↑(f.sec z).2 * v

Tactic:
by
  rw [mul_comm, lift_apply, ← mul_assoc, mul_inv_left hg, mul_comm]

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

Goal state before:
pp: R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S

Tactic:
rw [← mul_assoc, mul_assoc _ r₃', ← h₃, ← mul_assoc, ← mul_assoc, mul_assoc]

Goal state after:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
⊢ ↑s₄' * ↑s₃' * ↑s₂' * (r₂ * ↑s) ∈ S
Module: Mathlib.Algebra.Order.Sub.WithTop

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

Tactic:
induction b

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

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

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

Tactic:
induction b

Goal state after:
case coe.top
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝ : α
⊢ ↑a✝ - ⊤ = ⊤ ↔ ↑a✝ = ⊤ ∧ ⊤ ≠ ⊤

case coe.coe
α : Type u_1
inst✝¹ : Sub α
inst✝ : Bot α
a✝¹ a✝ : α
⊢ ↑a✝¹ - ↑a✝ = ⊤ ↔ ↑a✝¹ = ⊤ ∧ ↑a✝ ≠ ⊤
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
⊢ IsRegular (f m)

Tactic:
by
  refine (Commute.isRegular_iff (Commute.all _)).mpr fun n₁ n₂ eq ↦ ?_
  have ⟨ms₁, eq₁⟩ := f.surj n₁
  have ⟨ms₂, eq₂⟩ := f.surj n₂
  rw [← (f.map_units (ms₁.2 * ms₂.2)).mul_left_inj, Submonoid.coe_mul]
  replace eq := congr($eq * f (ms₁.2 * ms₂.2))
  simp_rw [mul_assoc] at eq
  rw [map_mul, ← mul_assoc n₁, eq₁, ← mul_assoc n₂, mul_right_comm n₂, eq₂] at eq ⊢
  simp_rw [← map_mul, eq_iff_exists] at eq ⊢
  simp_rw [mul_left_comm _ m] at eq
  exact eq.imp fun _ ↦ (hm.1 ·)

Goal state after:
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 : R
m : R'
x : OreLocalization S X
⊢ ((r • m) • 1 /ₒ 1) • x = (r • 1 /ₒ 1 * (m • 1 /ₒ 1)) • x

Tactic:
mul_div_one

Goal state after:
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 : R
m : R'
x : OreLocalization S X
⊢ ((r • m) • 1 /ₒ 1) • x = (r • 1 * m • 1 /ₒ 1) • x
Module: Mathlib.Order.Iterate

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

Tactic:
by
  induction n with
  | zero => exact hn.false.elim
  | succ n ihn =>
  suffices x n ≤ y n from (hx n n.lt_succ_self).trans_le ((hf this).trans <| hy n n.lt_succ_self)
  cases n with
  | zero => exact h₀
  | succ n =>
    refine (ihn n.zero_lt_succ (fun k hk => hx _ ?_) fun k hk => hy _ ?_).le <;>
    exact hk.trans n.succ.lt_succ_self

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : WithBot α
x0 : 0 < x
a b : WithBot α
h : a < b
⊢ x * a < x * b

Tactic:
lift x to α using x0.ne_bot
    cases b
    · exact absurd h not_lt_bot
    cases a
    · simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]
    simp only [← coe_mul, coe_lt_coe] at *
    norm_cast at x0
    exact mul_lt_mul_of_pos_left h x0

Goal state after:
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inr.coe.coe
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLT α
x : α
x0' : ↑x ≠ 0
a✝¹ a✝ : α
h : x * a✝ < x * a✝¹
x0 : 0 ≤ x
⊢ a✝ < a✝¹

Tactic:
exact lt_of_mul_lt_mul_left h x0

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

Goal state before:
pp: case succ
α : Type u_1
inst✝³ : Preorder α
inst✝² : SuccOrder α
inst✝¹ : IsSuccArchimedean α
inst✝ : NoMaxOrder α
b : α
n : ℕ
h : IsSuccPrelimit (succ (succ^[n] b))
hb : b ≤ succ^[n + 1] b
⊢ succ^[n + 1] b ≤ b

Tactic:
exact (not_isSuccPrelimit_succ _ h).elim

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Add α
inst✝¹ : One α
inst✝ : SuccAddOrder α
x : α
⊢ x ⩿ x + 1

Tactic:
rw [← succ_eq_add_one]
  exact wcovBy_succ x

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

Goal state before:
pp: case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
⊢ j ≤ succ^[n + 1] i

Tactic:
have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)

Goal state after:
case succ
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : SuccOrder α
inst✝ : PredOrder α
i : α
n : ℕ
hn : ¬IsMax (succ^[n] i) → pred^[n + 1] (succ^[n + 1] i) = i
hin : ¬IsMax (succ^[n + 1] i)
h_sub_le : succ^[n] i ≤ succ^[n.succ] i
h_max : IsMax (succ^[n] i)
j : α
hj : succ^[n + 1] i ≤ j
hj_le : j ≤ succ^[n] i
⊢ j ≤ succ^[n + 1] i
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
by
  induction n with
  | zero => simp only [Function.iterate_zero, id]
  | succ n hn =>
    rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
    have h_not_max : ¬IsMax (succ^[n - 1] i) := by
      rcases n with - | n
      · simpa using hin
      rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
      have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
      refine fun h_max => hin fun j hj => ?_
      have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
      exact hj_le.trans h_sub_le
    rw [Function.iterate_succ, Function.iterate_succ']
    simp only [Function.comp_apply]
    rw [pred_succ_of_not_isMax hin]
    exact hn h_not_max

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

Goal state before:
pp: α : Type u_1
p q : α → Prop
inst✝² : Fintype { x // p x }
inst✝¹ : Fintype { x // q x }
inst✝ : Fintype { x // p x ∨ q x }
⊢ card { x // p x ∨ q x } ≤ card { x // p x } + card { x // q x }

Tactic:
by
  classical
    convert! Fintype.card_le_of_embedding (subtypeOrLeftEmbedding p q)
    rw [Fintype.card_sum]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList

Tactic:
exact .inl rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
rw [← cons_head_tail v]

Goal state after:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b v).head = b

Tactic:
rw [← cons_head_tail v]

Goal state after:
case succ
α : Type u_1
β : Type u_6
f : β → α → β
b : β
n✝ : ℕ
v : Vector α (n✝ + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).head = b
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ #(piFinset (Function.update s i {a})) = ∏ j, #(Function.update s i {a} j)

Tactic:
Fintype.card_piFinset

Goal state after:
ι : Type u_4
α : ι → Type u_6
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : (i : ι) → DecidableEq (α i)
s : (i : ι) → Finset (α i)
i : ι
a : α i
ha : a ∈ s i
⊢ ∏ i_1, #(Function.update s i {a} i_1) = ∏ j, #(Function.update s i {a} j)
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
⊢ filter (fun x ↦ a ≠ x) (↑m.snd + ↑(replicate (↑m.fst) a)) = ↑m.snd

Tactic:
filter_add,

Goal state after:
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : (i : Fin (n + 1)) × Sym α (n - ↑i)
h : a ∉ m.snd
⊢ filter (fun x ↦ a ≠ x) ↑m.snd + filter (fun x ↦ a ≠ x) ↑(replicate (↑m.fst) a) = ↑m.snd
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
⊢ range (enumerateCountable h default) ⊆ insert default s

Tactic:
by
  refine range_subset_iff.mpr (fun n ↦ ?_)
  rw [enumerateCountable]
  match @decode s (Countable.toEncodable h) n with
  | none => exact mem_insert _ _
  | some val => simp

Goal state after:
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 : ℕ → ↑S
hs : Surjective s
⊢ ⨆ y, ↑y = ⊤

Tactic:
← sSup_eq_iSup'

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
⊢ sSup S = ⊤
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
this : ∀ (t : { t // (f t).Nonempty }), ∃ x, ↑x ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}

Tactic:
choose F hF using this

Goal state after:
α : Type u
β : Type v
f : β → Set α
hf : Pairwise (Disjoint on f)
s : Set α
h'f : ∀ (t : β), f t ⊆ s
hs : Countable ↑s
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
⊢ Countable ↑{t | (f t).Nonempty}
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (upperBounds {a, b}) b

Tactic:
upperBounds_insert,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici a ∩ upperBounds {b}) b
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici a ∩ upperBounds {b}) b

Tactic:
upperBounds_singleton,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
D : Set (Set α)
hD : ∀ (a b : α), a ≤ b → {a, b} ∈ D
h : ScottContinuousOn D f
a b : α
hab : a ≤ b
⊢ IsLeast (Ici a ∩ Ici b) b
Module: Mathlib.Order.Hom.Order

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

Tactic:
by
  constructor <;> intro h
  · exact h 1 0
  · intro n₁ n₂ a₁ a₂
    have h' : ∀ n a₁ a₂, f^[n] (a₁ ⊔ a₂) ≤ f^[n] a₁ ⊔ a₂ := by
      intro n
      induction n with
      | zero => intro a₁ a₂; rfl
      | succ n ih =>
        intro a₁ a₂
        calc
          f^[n + 1] (a₁ ⊔ a₂) = f^[n] (f (a₁ ⊔ a₂)) := Function.iterate_succ_apply f n _
          _ ≤ f^[n] (f a₁ ⊔ a₂) := f.mono.iterate n (h a₁ a₂)
          _ ≤ f^[n] (f a₁) ⊔ a₂ := ih _ _
          _ = f^[n + 1] a₁ ⊔ a₂ := by rw [← Function.iterate_succ_apply]
    calc
      f^[n₁ + n₂] (a₁ ⊔ a₂) = f^[n₁] (f^[n₂] (a₁ ⊔ a₂)) :=
        Function.iterate_add_apply f n₁ n₂ _
      _ = f^[n₁] (f^[n₂] (a₂ ⊔ a₁)) := by rw [sup_comm]
      _ ≤ f^[n₁] (f^[n₂] a₂ ⊔ a₁) := f.mono.iterate n₁ (h' n₂ _ _)
      _ = f^[n₁] (a₁ ⊔ f^[n₂] a₂) := by rw [sup_comm]
      _ ≤ f^[n₁] a₁ ⊔ f^[n₂] a₂ := h' n₁ a₁ _

Goal state after:
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: case refine_2
β : Type u_2
inst✝ : SemilatticeSup β
d : Set (β × β)
x✝² : d.Nonempty
x✝¹ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : β × β
p₁ p₂ : β
hdp : (∀ (a b : β), (a, b) ∈ d → a ≤ p₁ ∧ b ≤ p₂) ∧ (p₁, p₂) ∈ lowerBounds {x | ∀ (a b : β), (a, b) ∈ d → (a, b) ≤ x}
e1 : ∀ (a b : β), (∀ (b₁ b₂ : β), (b₁, b₂) ∈ d → b₁ ≤ a ∧ b₂ ≤ b) → p₁ ≤ a ∧ p₂ ≤ b
b : β
hb : b ∈ {x | ∀ ⦃a : β⦄ (x_1 x_2 : β), (x_1, x_2) ∈ d → x_1 ⊔ x_2 = a → a ≤ x}
⊢ p₁ ⊔ p₂ ≤ b

Tactic:
· rw [sup_le_iff]
    exact e1 _ _ fun b₁ b₂ hb' => sup_le_iff.mp (hb b₁ b₂ hb' rfl)

Goal state after:
Module: Mathlib.Order.BourbakiWitt

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

Tactic:
exact hy.map_le_of_mem_of_lt hz hzy

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ ChainClosure r ∅

Tactic:
by
  have : ChainClosure r (⋃₀ ∅) := ChainClosure.union fun a h => (notMem_empty _ h).elim
  simpa using this

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
x✝¹ : Chain ((a : α) → β a)
x✝ : (a : α) → β a
hf : ∀ (i : ℕ), x✝¹ i ≤ x✝
a : α
⊢ ∀ (i : ℕ), (x✝¹.map (Pi.evalOrderHom a)) i ≤ x✝ a

Tactic:
rintro i

Goal state after:
ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
x✝¹ : Chain ((a : α) → β a)
x✝ : (a : α) → β a
hf : ∀ (i : ℕ), x✝¹ i ≤ x✝
a : α
i : ℕ
⊢ (x✝¹.map (Pi.evalOrderHom a)) i ≤ x✝ a
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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
⊢ g' '' g '' (f '' s)ᶜ = (f '' s)ᶜ

Tactic:
g'g.image_image

Goal state after:
α : 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
⊢ (f '' s)ᶜ = (f '' s)ᶜ
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_2
α : 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'
this : Surjective h
⊢ ∀ x ∈ s, ∀ y ∉ s, f x ≠ g' y

Tactic:
intro x hx y hy hxy
      obtain ⟨y', hy', rfl⟩ : y ∈ g '' (f '' s)ᶜ := by rwa [hns]
      rw [g'g _] at hxy
      exact hy' ⟨x, hx, hxy⟩

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:
by
  apply ωScottContinuous.of_monotone_map_ωSup ⟨?_, fun c ↦ ?_⟩
  · intro x y hxy
    exact OrderHom.apply_mono (hf.monotone hxy) (hg.monotone hxy)
  · rw [hf.map_ωSup, hg.map_ωSup]
    simp only [ωSup_def, ωSup_apply]
    apply le_antisymm
    · apply ωSup_le
      intro i
      dsimp
      rw [(f (c i)).continuous]
      apply ωSup_le
      intro j
      apply le_ωSup_of_le (i ⊔ j)
      apply apply_mono
      · apply hf.monotone (c.monotone le_sup_left)
      · apply hg.monotone (c.monotone le_sup_right)
    · simp only [ωSup_le_iff]
      intro i
      apply le_ωSup_of_le i
      apply (f (c i)).monotone
      apply le_ωSup_of_le i
      rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
rw [← this]

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

Goal state before:
pp: R : Type u_1
inst✝ : AddGroupWithOne R
n : ℕ
⊢ op ↑↑n = op ↑n

Tactic:
rw [Int.cast_natCast]

Goal state after:
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
C : Set M
nonempty : C.Nonempty
linearComb : ∀ x ∈ C, ∀ y ∈ C, ∀ (a b : R), a • x + b • y ∈ C
x y : M
hx : x ∈ C
hy : y ∈ C
⊢ x + y ∈ C

Tactic:
by simpa [one_smul] using linearComb x hx y hy 1 1

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

Goal state before:
pp: case add
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 x✝ y✝ : M
hx✝ : x✝ ∈ ⨆ i, ↑i
hy✝ : y✝ ∈ ⨆ i, ↑i
⊢ t • x✝ ∈ ⨆ a, ↑a → t • y✝ ∈ ⨆ a, ↑a → t • x✝ + t • y✝ ∈ ⨆ a, ↑a

Tactic:
exact add_mem

Goal state after:
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✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
τ₁₂ : R →+* R₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ N ≤ f.ker ↔ f ∘ₛₗ N.subtype = 0

Tactic:
SetLike.le_def,

Goal state after:
R : Type u_1
R₂ : Type u_2
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₂
N : Submodule R M
f : M →ₛₗ[τ₁₂] M₂
⊢ (∀ ⦃x : M⦄, x ∈ N → x ∈ f.ker) ↔ f ∘ₛₗ N.subtype = 0
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:
← 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.Module.Submodule.Map

Goal state before:
pp: R : Type u_1
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p p' : Submodule R M
x : M
⊢ x ∈ map p.subtype (comap p.subtype p') → x ∈ p ⊓ p'

Tactic:
by rintro ⟨⟨_, h₁⟩, h₂, rfl⟩; exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x : R
h : x ∈ closure s
⊢ x ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
induction h using closure_induction with
    | mem _ hx => exact AddSubgroup.subset_closure (Subsemigroup.subset_closure hx)
    | zero => exact zero_mem _
    | add _ _ _ _ hx hy => exact add_mem hx hy
    | neg x _ hx => exact neg_mem hx
    | mul _ _ _hx _hy hx hy =>
      clear _hx _hy
      induction hx, hy using AddSubgroup.closure_induction₂ with
      | mem _ _ hx hy => exact AddSubgroup.subset_closure (mul_mem hx hy)
      | zero_left => simp
      | zero_right => simp
      | add_left _ _ _ _ _ _ h₁ h₂ => simpa [add_mul] using add_mem h₁ h₂
      | add_right _ _ _ _ _ _ h₁ h₂ => simpa [mul_add] using add_mem h₁ h₂
      | neg_left _ _ _ _ h => simpa [neg_mul] using neg_mem h
      | neg_right _ _ _ _ h => simpa [mul_neg] using neg_mem h

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
hι : Nonempty ι
S : ι → NonUnitalSubring R
hS : Directed (fun x1 x2 ↦ x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩
  let U : NonUnitalSubring R :=
    NonUnitalSubring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubsemigroup) (⨆ i, (S i).toAddSubgroup)
      (Subsemigroup.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)
  suffices ⨆ i, S i ≤ U by simpa [U] using @this x
  exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Goal state after: