mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
h : LeftCommutative f
b : β
⊢ noncommFoldr f s ⋯ b = foldr f b s

Tactic:
by
  induction s using Quotient.inductionOn
  simp

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

Goal state before:
pp: F : Type u_1
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
f : α → β → β
op : α → α → α
assoc : Std.Associative op
s : Multiset α
comm : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
hx : x ∈ {x | x ∈ s}
y : α
hy : y ∈ {x | x ∈ s}
h : x ≠ y
b : α
⊢ op x (op y b) = op y (op x b)

Tactic:
by rw [← assoc.assoc, comm hx hy h, assoc.assoc]

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

Goal state before:
pp: α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y ↦ op x y = op y x
h' : {x | x ∈ s}.Pairwise fun x y ↦ op x y = op y x
x : α
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Tactic:
by
  induction s using Quotient.inductionOn
  simp

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

Goal state before:
pp: α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
inst✝ : Std.Commutative op
a : α
⊢ noncommFold op s ⋯ a = fold op a s

Tactic:
by
  induction s using Quotient.inductionOn
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s = ↑(closure s)

Tactic:
rw [← Set.iUnion_op_smul_set]
  have h a (ha : a ∈ s) : (closure s : Set G) <• a = closure s :=
    op_smul_coe_set <| subset_closure ha
  simp +contextual [h, hs]

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = a * s.noncommProd ⋯

Tactic:
by
  induction s using Quotient.inductionOn
  simp

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

Goal state before:
pp: α : Type u_3
inst✝ : Monoid α
s : Multiset α
a : α
comm : {x | x ∈ a ::ₘ s}.Pairwise Commute
⊢ (a ::ₘ s).noncommProd comm = s.noncommProd ⋯ * a

Tactic:
induction s using Quotient.inductionOn with | _ s

Goal state after:
case h
α : Type u_3
inst✝ : Monoid α
a : α
s : List α
comm : {x | x ∈ a ::ₘ ⟦s⟧}.Pairwise Commute
⊢ (a ::ₘ ⟦s⟧).noncommProd comm = noncommProd ⟦s⟧ ⋯ * a
Module: Mathlib.Algebra.Group.Subgroup.Pointwise

Goal state before:
pp: G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ S * ↑N = ↑N * S

Tactic:
← iUnion_mul_left_image,

Goal state after:
G : Type u_2
inst✝ : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ ↑(normalizer ↑N)
⊢ ⋃ a ∈ S, (fun x ↦ a * x) '' ↑N = ↑N * S
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case h.cons
α : Type u_3
inst✝ : Monoid α
a hd : α
tl : List α
IH : {x | x ∈ a ::ₘ ⟦tl⟧}.Pairwise Commute → a * tl.prod = tl.prod * a
comm : {x | x ∈ a ::ₘ ⟦hd :: tl⟧}.Pairwise Commute
⊢ a * (hd :: tl).prod = (hd :: tl).prod * a

Tactic:
| cons hd tl IH =>

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

Goal state before:
pp: α : Type u_6
inst✝ : CommMonoid α
s : Multiset α
⊢ s.noncommProd ⋯ = s.prod

Tactic:
by
  induction s using Quotient.inductionOn
  simp

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: M : Type u_1
B : Type u_3
inst✝² : Monoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
S : B
l : List M
hl : ∀ x ∈ l, x ∈ S
⊢ l.prod ∈ S

Tactic:
lift l to List S using hl
  rw [← coe_list_prod]
  exact l.prod.coe_prop

Goal state after:
Module: Mathlib.Algebra.Group.Submonoid.BigOperators

Goal state before:
pp: B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset ↥S
⊢ ↑m.prod ∈ S

Tactic:
exact m.prod.coe_prop

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

Goal state before:
pp: α : Type u_1
S : Set (Setoid α)
⊢ sSup S = EqvGen.setoid fun x y ↦ ∃ r ∈ S, r x y

Tactic:
rw [eqvGen_eq]
  apply congr_arg sInf
  simp only [upperBounds, le_def, and_imp, exists_imp]
  ext
  exact ⟨fun H x y r hr => H hr, fun H r hr x y => H r hr⟩

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

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ s.disjSum t, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)

Tactic:
← map_inl_disjUnion_map_inr,

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
t : Finset κ
f : ι ⊕ κ → M
⊢ ∏ x ∈ (map Embedding.inl s).disjUnion (map Embedding.inr t) ⋯, f x = (∏ x ∈ s, f (Sum.inl x)) * ∏ x ∈ t, f (Sum.inr x)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
x y z : FreeAbelianGroup α
⊢ (x + y) * z = x * z + y * z

Tactic:
by simp [mul_def, ← Pi.add_def]

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

Goal state before:
pp: case e'_2.e'_7
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ y✝.1 * ↑y✝.2 = ↑(⟨y✝.1, ⋯⟩ * y✝.2)

Tactic:
Submonoid.coe_mul

Goal state after:
case e'_2.e'_7
M : Type u_1
G : Type u_2
inst✝¹ : CommMonoid M
inst✝ : CommGroup G
y✝ : M × ↥⊤
⊢ y✝.1 * ↑y✝.2 = ↑⟨y✝.1, ⋯⟩ * ↑y✝.2
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_2
inst✝ : MulAction R X
β : OreLocalization S X → Prop
c : ∀ (r : X) (s : ↥S), β (r /ₒ s)
⊢ ∀ (q : OreLocalization S X), β q

Tactic:
apply Quotient.ind
  rintro ⟨r, s⟩
  exact c r s

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
r : R
s : ↥S
r₁ : X
r₂ : R
s' : ↥S
hs : r₂ * ↑s' ∈ S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r = r₁' * ↑s'
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * r = r₂' * ↑⟨r₂ * ↑s', hs⟩
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * ↑s₁' = r₃' * ↑s₂'
this : ↑s₃' * r₁' * ↑s' = r₃' * r₂' * r₂ * ↑s'
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₁') = ↑s₄' * (r₃' * r₂' * r₂)
⊢ ↑s₄' * (↑s₃' * ↑s₁' * ↑s) ∈ S

Tactic:
exact (s₄' * (s₃' * s₁' * s)).2

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
r : R
hr : r ∈ S
⊢ ∃ u v, u • 1 = v • r ∧ ↑u * ↑1 = v * ↑⟨r, hr⟩

Tactic:
exact ⟨⟨r, hr⟩, 1, by simp, by simp⟩

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

Goal state before:
pp: case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = ↑sc * ra * ↑s₂

Tactic:
mul_assoc _ ra,

Goal state after:
case c.c.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
r₃ : X
s₃ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
rb : R
sb : ↥S
hb : ↑sb * r₂ = rb * ↑s₃
rc : R
sc : ↥S
hc : ↑sc * ra = rc * ↑sb
⊢ ↑sc * ↑sa * r₁ = ↑sc * (ra * ↑s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : MulZeroOneClass α
inst✝ : Nontrivial α
a : α
⊢ ↑a * 1 = ↑a

Tactic:
by rw [← coe_one, ← coe_mul, mul_one]

Goal state after:
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
n₁ n₂ : N
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
⊢ n₁ * f ↑(ms₁.2 * ms₂.2) = n₂ * f ↑(ms₁.2 * ms₂.2)

Tactic:
Submonoid.coe_mul

Goal state after:
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
n₁ n₂ : N
eq : (fun x ↦ f m * x) n₁ = (fun x ↦ f m * x) n₂
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
⊢ n₁ * f (↑ms₁.2 * ↑ms₂.2) = n₂ * f (↑ms₁.2 * ↑ms₂.2)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x < g^[n] x ↔ f x < g x

Tactic:
by
  rcases lt_trichotomy (f x) (g x) with (H | H | H)
  · simp only [*, iterate_pos_lt_of_map_lt]
  · simp only [*, h.iterate_eq_of_map_eq, lt_irrefl]
  · simp only [lt_asymm H, lt_asymm (h.symm.iterate_pos_lt_of_map_lt' hg hf H hn)]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
⊢ (∃ b, b ⋖ a) ↔ ∃ b, ¬IsMax b ∧ succ b = a

Tactic:
refine exists_congr fun b ↦ ⟨fun hba ↦ ⟨hba.lt.not_isMax, hba.succ_eq⟩, ?_⟩

Goal state after:
α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ ¬IsMax b ∧ succ b = a → b ⋖ a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ a < succ b ↔ a ≤ b

Tactic:
lt_succ_iff_of_not_isMax hb

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
hb : ¬IsMax b
⊢ a ≤ b ↔ a ≤ b
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a✝ : α
⊢ (↑a✝).succ = 0 ↔ ↑a✝ = ⊥

Tactic:
rename_i a

Goal state after:
case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a : α
⊢ (↑a).succ = 0 ↔ ↑a = ⊥
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe.top
a✝ : ℕ
⊢ (↑a✝ * ⊤).toNat = (↑a✝).toNat * ⊤.toNat

Tactic:
rename_i a

Goal state after:
case coe.top
a : ℕ
⊢ (↑a * ⊤).toNat = (↑a).toNat * ⊤.toNat
Module: Mathlib.Order.SuccPred.Archimedean

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

Tactic:
· exact (hn this).trans' (hf _ ha' this ha)

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

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

Tactic:
· exact (hn this).trans' (hf _ ha' this ha)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y

Tactic:
have : ∀ z : γ × α, (z ∈ s.biUnion fun x => (t x).map <| Function.Embedding.sectR x _) ↔
      z.1 ∈ s ∧ z.2 ∈ t z.1 := by
      rintro ⟨x, y⟩
      simp only [mem_biUnion, mem_map, Function.Embedding.sectR_apply, Prod.mk.injEq,
        exists_eq_right, ← and_assoc]

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝ : CommMonoid β
s : Finset γ
t : γ → Finset α
t' : Finset α
s' : α → Finset γ
h : ∀ (x : γ) (y : α), x ∈ s ∧ y ∈ t x ↔ x ∈ s' y ∧ y ∈ t'
f : γ → α → β
this : ∀ (z : γ × α), (z ∈ s.biUnion fun x ↦ map (Embedding.sectR x α) (t x)) ↔ z.1 ∈ s ∧ z.2 ∈ t z.1
⊢ ∏ x ∈ s, ∏ y ∈ t x, f x y = ∏ y ∈ t', ∏ x ∈ s' y, f x y
Module: Mathlib.Data.Vector.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p✝ : α → Prop
i : Fin n
l : List α
p : l.length = n
⊢ (l.eraseIdx ↑i).length = n - 1

Tactic:
rw [l.length_eraseIdx_of_lt] <;> rw [p]; exact i.2

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype α
u : Finset (α ⊕ β)
⊢ u.toLeft = univ ↔ map Function.Embedding.inl univ ⊆ u

Tactic:
simp [map_inl_subset_iff_subset_toLeft]

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

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
← prod_filter,

Goal state after:
α : 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
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case neg.a
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ j ≤ i

Tactic:
· simpa [not_lt] using hij

Goal state after:
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)

Goal state after:
case inl
α : 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 (inl a) (inl a)

case inr
α : 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 (inr a) (inr a)
Module: Mathlib.SetTheory.Cardinal.Defs

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

Tactic:
prod,

Goal state after:
case mk.mk
ι : Type u
α : Type v
f : ι → Type v
⊢ (#(ULift α) ^ sum fun i ↦ #(f i)) = #((i : ι) → Quotient.out (#α ^ #(f i)))
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LT α
f : α ≤i β
h : b ≤ f a
⊢ b ∈ Set.range ⇑f

Tactic:
obtain rfl | hb := h.eq_or_lt

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
inst✝ : LT α
f : α ≤i β
h : f a ≤ f a
⊢ f a ∈ Set.range ⇑f

case inr
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder β
a : α
b : β
inst✝ : LT α
f : α ≤i β
h : b ≤ f a
hb : b < f a
⊢ b ∈ Set.range ⇑f
Module: Mathlib.Order.ScottContinuity

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α → β
⊢ ScottContinuousOn univ f ↔ ScottContinuous f

Tactic:
by
  simp [ScottContinuousOn, ScottContinuous]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case neg
α : Type u_2
c : Chain (Part α)
a : α
h_1 : ¬∃ a, some a ∈ c
h : a ∈ none
⊢ some a ∈ c

Tactic:
rcases h with ⟨⟨⟩⟩

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' := ⋯ }
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)

Tactic:
set s : Set α := F.lfp

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
⊢ ∃ h, Bijective h ∧ ∀ (a : α), R a (h a)
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
n : ℕ∞
x : Cardinal.{u_1}
hx : ℵ₀ ≤ x
⊢ ↑n ≤ x ↔ n ≤ x.toENatAux

Tactic:
simp [toENatAux_eq_top hx, (ofENat_le_aleph0 n).trans hx]

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

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

Tactic:
by
  apply ((le_csSup_iff' (bddAbove_image.{_, u} _ hs)).2 fun c hc => _).antisymm (csSup_le' _)
  · intro c hc
    by_contra h
    obtain ⟨d, rfl⟩ := Cardinal.mem_range_lift_of_le (not_le.1 h).le
    simp_rw [lift_le] at h hc
    rw [csSup_le_iff' hs] at h
    exact h fun a ha => lift_le.1 <| hc (mem_image_of_mem _ ha)
  · rintro i ⟨j, hj, rfl⟩
    exact lift_le.2 (le_csSup hs hj)

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

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
by
  rw [← not_lt, lt_aleph0_iff_finite, not_finite_iff_infinite]

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

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

Tactic:
by
  refine ⟨fun H s hs ↦ by simpa using (mk_le_mk_of_subset hs).trans H, fun H ↦ ?_⟩
  apply card_le_of (fun s ↦ ?_)
  classical
  let u : Finset α := s.image Subtype.val
  have : u.card = s.card := Finset.card_image_of_injOn Subtype.coe_injective.injOn
  grind

Goal state after:
Module: Mathlib.Algebra.Algebra.Defs

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
⊢ P = Q

Tactic:
have h' : (haveI := P; (· • ·) : R → A → A) = (haveI := Q; (· • ·) : R → A → A) := by
    funext r a
    rw [P.smul_def', Q.smul_def', h]

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
h' : (fun x1 x2 ↦ x1 • x2) = fun x1 x2 ↦ x1 • x2
⊢ P = Q
Module: Mathlib.Algebra.Module.Submodule.Defs

Goal state before:
pp: R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
⊢ r • x ∈ p ↔ x ∈ p

Tactic:
refine ⟨fun h ↦ ?_, p.smul_mem r⟩

Goal state after:
R : Type u
M : Type v
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
module_M : Module R M
p : Submodule R M
r : R
x : M
inst✝ : Invertible r
h : r • x ∈ p
⊢ x ∈ p
Module: Mathlib.GroupTheory.GroupAction.SubMulAction

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizer R m = MulAction.stabilizer R ↑m

Tactic:
← Subgroup.toSubmonoid_inj

Goal state after:
R : Type u
M : Type v
inst✝¹ : Group R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ (MulAction.stabilizer R m).toSubmonoid = (MulAction.stabilizer R ↑m).toSubmonoid
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₂
⊢ M ≃ₗ[ℤ] M₂

Tactic:
refine e.toLinearEquiv fun c a ↦ ?_
  convert! e.toAddMonoidHom.map_zsmul c a using 1
  · exact congr(e $(int_smul_eq_zsmul ..))
  · exact int_smul_eq_zsmul ..

Goal state after:
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
⊢ map f p ⋖ map f q

Tactic:
by
  refine ⟨lt_of_le_of_ne (map_mono h.1.le) ((map_injective_of_injective hf).ne h.1.ne), ?_⟩
  intro P h₁ h₂
  refine h.2 ?_ (Submodule.comap_lt_of_lt_map_of_injective hf h₂)
  rw [← Submodule.map_lt_map_iff_of_injective hf]
  refine h₁.trans_le ?_
  exact (Set.image_preimage_eq_of_subset (.trans h₂.le (Set.image_subset_range _ _))).superset

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑↑n * (x✝¹ * x✝) = ↑↑n * x✝¹ * x✝

Tactic:
by rw [Int.cast_natCast, (natCast_mem_center _ n).left_assoc _ _]

Goal state after:
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
S T : Subsemigroup M
f : M →ₙ* N
g : N → M
h : Function.LeftInverse g ⇑f
x : ↥f.srange
x' : M
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
rw [← hx', h x']

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

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝³ : NonUnitalNonAssocSemiring R
M : Subsemigroup R
s t : NonUnitalSubsemiring R
inst✝² : NonUnitalNonAssocSemiring S
F : Type u_1
inst✝¹ : FunLike F R S
inst✝ : NonUnitalRingHomClass F R S
g : S → R
f : F
h : Function.LeftInverse g ⇑f
x : ↥(srange f)
x' : R
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
rw [← hx', h x']

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ + y✝ ∈ closure s

Tactic:
exact add_mem h₁ h₂

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

Goal state before:
pp: R : Type u
inst✝¹ : NonUnitalNonAssocRing R
ι : Sort u_1
inst✝ : Nonempty ι
S : ι → NonUnitalSubring R
hS : ∀ (i : ι), IsMulCommutative ↥(S i)
dir : Directed (fun x1 x2 ↦ x1 ≤ x2) S
⊢ IsMulCommutative ↥(⨆ i, S i)

Tactic:
by
  simpa [isMulCommutative_iff, ← SetLike.mem_coe, NonUnitalSubsemiring.coe_iSup_of_directed dir,
    coe_iSup_of_directed dir] using NonUnitalSubsemiring.isMulCommutative_iSup dir

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonUnitalRing R
inst✝ : NonUnitalRing S
s t : NonUnitalSubring R
g : S → R
f : R →ₙ+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
rw [← hx', h x']

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

Goal state before:
pp: R : Type u
A : Type v
B : Type w
inst✝⁴ : CommSemiring R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : Semiring B
inst✝ : Algebra R B
x✝ : A →ₐ[R] A
⊢ ↑(x✝ • 1) = ↑1

Tactic:
exact map_one _

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

Goal state before:
pp: case add
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h₁ : x✝ ∈ closure s
h₂ : y✝ ∈ closure s
⊢ x✝ + y✝ ∈ closure s

Tactic:
exact add_mem h₁ h₂

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
g : S → R
f : R →+* S
h : Function.LeftInverse g ⇑f
x : ↥f.range
x' : R
hx' : f x' = ↑x
⊢ f (g ↑x) = ↑x

Tactic:
rw [← hx', h x']

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
s : Set R
C : R → Prop
x : R
hx : x ∈ closure s
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
⊢ C x

Tactic:
rcases exists_list_of_mem_closure hx with ⟨L, HL, rfl⟩

Goal state after:
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
L : List (List R)
HL : ∀ t ∈ L, ∀ y ∈ t, y ∈ s ∨ y = -1
hx : (List.map List.prod L).sum ∈ closure s
⊢ C (List.map List.prod L).sum