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

Goal state before:
pp: case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' : ¬IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} fun n ↦ if n < g 0 then f n else (f (g (n - g 0))).tail
⊢ False

Tactic:
rw [IsBadSeq] at hf'

Goal state after:
case inr.refine_2
α : Type u_2
r : α → α → Prop
inst✝ : IsPreorder α r
s : Set α
h : s.PartiallyWellOrderedOn r
h✝ : Nonempty α
inhabited_h : Inhabited α
f : ℕ → List α
hf1 : IsBadSeq (List.SublistForall₂ r) {l | ∀ x ∈ l, x ∈ s} f
hf2 : ∀ (n : ℕ), IsMinBadSeq (List.SublistForall₂ r) List.length {l | ∀ x ∈ l, x ∈ s} n f
hnil : ∀ (n : ℕ), f n ≠ []
g : ℕ ↪o ℕ
hg : ∀ (m n : ℕ), m ≤ n → r (f (g m)).head! (f (g n)).head!
hf' :
  ¬((∀ (n : ℕ), (if n < g 0 then f n else (f (g (n - g 0))).tail) ∈ {l | ∀ x ∈ l, x ∈ s}) ∧
      ∀ (m n : ℕ),
        m < n →
          ¬List.SublistForall₂ r (if m < g 0 then f m else (f (g (m - g 0))).tail)
              (if n < g 0 then f n else (f (g (n - g 0))).tail))
⊢ False
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
⊢ center.commMonoid.toMonoid = (center M).toMonoid

Tactic:
with_reducible_and_instances rfl

Goal state after:
Module: Mathlib.GroupTheory.Subgroup.Centralizer

Goal state before:
pp: G : Type u_1
G' : Type u_2
inst✝¹ : Group G
inst✝ : Group G'
s : Set G
f : G →* G'
⊢ map f (centralizer s) ≤ centralizer (⇑f '' s)

Tactic:
rintro - ⟨g, hg, rfl⟩ - ⟨h, hh, rfl⟩
  rw [← map_mul, ← map_mul, hg h hh]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
x : G
⊢ closure {x⁻¹} = closure {x}

Tactic:
rw [← Set.inv_singleton, closure_inv]

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

Goal state before:
pp: case h.cons.e_a
α : 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 = hd * a

Tactic:
apply comm.of_refl

Goal state after:
case h.cons.e_a.a
α : 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 ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

case h.cons.e_a.a
α : 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
⊢ hd ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ≠ y → Commute x y

Tactic:
apply comm

Goal state after:
case h.cons.a
α : 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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ x ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}

case h.cons.a
α : 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
x y : α
hx : x ∈ {x | x = a ∨ x ∈ tl}
hy : y ∈ {x | x = a ∨ x ∈ tl}
⊢ y ∈ {x | x ∈ a ::ₘ ⟦hd :: tl⟧}
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ j ∈ s.attach.erase i, f ↑j = ∏ j ∈ s.erase ↑i, f j

Tactic:
← Function.Embedding.coe_subtype,

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
i : ↥s
⊢ ∏ j ∈ s.attach.erase i, f ((Embedding.subtype fun x ↦ x ∈ s) j) =
    ∏ j ∈ s.erase ((Embedding.subtype fun x ↦ x ∈ s) i), f j
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv } = ⊤ ↔ r = ⊤

Tactic:
by
  simp [eq_iff_rel_eq]

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

Goal state before:
pp: α : Type u_1
r : α → α → Prop
iseqv : Equivalence r
⊢ { r := r, iseqv := iseqv } = ⊥ ↔ r = fun x1 x2 ↦ x1 = x2

Tactic:
by
  simp [eq_iff_rel_eq]

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
c : Con M
f : M → M
hf : ∀ (x : M), c (f x * x) 1
x y : M
h : c x y
⊢ c (f x) (f y)

Tactic:
simp only [← Con.eq, coe_one, coe_mul] at *
  have hf' : ∀ x : M, (x : c.Quotient) * f x = 1 := fun x ↦
    calc
      (x : c.Quotient) * f x = f (f x) * f x * (x * f x) := by simp [hf]
      _ = f (f x) * (f x * x) * f x := by simp_rw [mul_assoc]
      _ = 1 := by simp [hf]
  have : (⟨_, _, hf' x, hf x⟩ : c.Quotientˣ) = ⟨_, _, hf' y, hf y⟩ := Units.ext h
  exact congr_arg Units.inv this

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
f : ι → M
inst✝ : DecidableEq ι
a b : ι
h : a ≠ b
⊢ ∏ x ∈ {a, b}, f x = f a * f b

Tactic:
rw [prod_insert (notMem_singleton.2 h), prod_singleton]

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

Goal state before:
pp: α : Type u
L : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
⊢ ∀ (b : List (α × Bool)), ¬Step L' b

Tactic:
intro L

Goal state after:
α : Type u
L✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
h : (x1, b1) ≠ (x2, b2)
L' : List (α × Bool)
eq : [(x1, !b1), (x2, b2)] = L'
L : List (α × Bool)
⊢ ¬Step L' L
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ a ∈ s, count a m = ∑ a ∈ m.toFinset, count a m

Tactic:
← Finset.sum_filter_ne_zero

Goal state after:
ι : Type u_1
inst✝ : DecidableEq ι
s : Finset ι
m : Multiset ι
hms : ∀ a ∈ m, a ∈ s
⊢ ∑ x ∈ s with count x m ≠ 0, count x m = ∑ a ∈ m.toFinset, count a m
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
s : Multiset M
⊢ IsUnit s.prod ↔ ∀ a ∈ s, IsUnit a

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons a s ih => simpa using fun _ ↦ ih

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' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ ↑t' * r₁ * r * r₂ = r₁' * ↑t * r * r₂

Tactic:
rw [hr₁]

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)
⊢ g (f.sec 1).1 = g ↑(f.sec 1).2

Tactic:
exact f.eq_of_eq hg (by rw [← sec_spec, one_mul])

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' r₁ r₂ : R
s t : ↥S
h : ↑t * r = ↑t * r'
r₁' : R
t' : ↥S
hr₁ : ↑t' * r₁ = r₁' * ↑t
⊢ r₁' * ↑t * r' * r₂ = ↑t' * r₁ * r' * r₂

Tactic:
rw [hr₁]

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
C : Sort u_2
P : X → ↥S → C
hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t * ↑s ∈ S), P r s = P (t • r) ⟨t * ↑s, ht⟩
x✝² x✝¹ : X × ↥S
r₁ : X
s₁ : ↥S
r₂ : X
s₂ : ↥S
x✝ : (r₁, s₁) ≈ (r₂, s₂)
u : ↥S
v : R
hr₂ : u • r₂ = v • r₁
s₁vS : v * ↑s₁ ∈ S
hs₂ : u * s₂ = ⟨v * ↑s₁, s₁vS⟩
⊢ ↑u * ↑s₂ ∈ S

Tactic:
by norm_cast; rwa [hs₂]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f.symm a ≤ f.symm b

Tactic:
← map_le_map_iff f

Goal state after:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Mul α
inst✝ : Mul β
f : α ≃*o β
a b : β
⊢ a ≤ b ↔ f (f.symm a) ≤ f (f.symm b)
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
r₁ : R
r₂ : X
s₁ s₂ u : ↥S
v : R
huv : ↑u * r₁ = v * ↑s₂
v₀ : R := oreNum r₁ s₂
u₀ : ↥S := oreDenom r₁ s₂
h₀ : ↑u₀ * r₁ = v₀ * ↑s₂
r₃ : R
s₃ : ↥S
h₃ : ↑s₃ * ↑u₀ = r₃ * ↑u
⊢ ↑s₃ * (↑u₀ * r₁) = ↑s₃ * v₀ * ↑s₂

Tactic:
rw [mul_assoc, h₀]

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₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)

Tactic:
clear ha'

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₂
⊢ (ra * r₂ /ₒ (sa * s₁)) • (r₃ /ₒ s₃) = (r₁ /ₒ s₁) • (r₂ /ₒ s₂) • (r₃ /ₒ s₃)
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
x y : OreLocalization S R
z : OreLocalization S X
⊢ (x * y) • z = x • y • z

Tactic:
by
  -- Porting note: `assoc_rw` was not ported yet
  cases x with | _ r₁ s₁
  cases y with | _ r₂ s₂
  cases z with | _ r₃ s₃
  rcases oreDivMulChar' r₁ r₂ s₁ s₂ with ⟨ra, sa, ha, ha'⟩; rw [ha']; clear ha'
  rcases oreDivSMulChar' r₂ r₃ s₂ s₃ with ⟨rb, sb, hb, hb'⟩; rw [hb']; clear hb'
  rcases oreCondition ra sb with ⟨rc, sc, hc⟩
  rw [oreDiv_smul_char (ra * r₂) r₃ (sa * s₁) s₃ (rc * rb) sc]; swap
  · rw [← mul_assoc _ ra, hc, mul_assoc, hb, ← mul_assoc]
  rw [← mul_assoc, mul_smul]
  symm; apply oreDiv_smul_char
  rw [Submonoid.coe_mul, Submonoid.coe_mul, ← mul_assoc, ← hc, mul_assoc _ ra, ← ha, mul_assoc]

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

Goal state before:
pp: case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
ha' : r₁ /ₒ s₁ * (r₂ /ₒ s₂) = ra * r₂ /ₒ (sa * s₁)
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)

Tactic:
clear ha'

Goal state after:
case c.c
R : Type u_1
inst✝³ : Monoid R
S : Submonoid R
inst✝² : OreSet S
X : Type ?u.10
inst✝¹ : MulAction R X
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
r₁ : R
s₁ : ↥S
r₂ : R
s₂ : ↥S
ra : R
sa : ↥S
ha : ↑sa * r₁ = ra * ↑s₂
⊢ liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (ra * r₂ /ₒ (sa * s₁)) =
    liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₁ /ₒ s₁) * liftExpand (fun r s ↦ ↑(fS s)⁻¹ * f r) ⋯ (r₂ /ₒ s₂)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c.c
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
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 /ₒ 1 * (r₁ /ₒ s₁)) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)

Tactic:
oreDiv_mul_char _ _ _ _ (r • 1) s₁ (by simp),

Goal state after:
case c.c
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
inst✝ : SMulCommClass R M M
r : R
r₁ : M
s₁ : ↥S
r₂ : X
s₂ : ↥S
⊢ (r • 1 * r₁ /ₒ (s₁ * 1)) • (r₂ /ₒ s₂) = (r₁ * r • 1 /ₒ s₁) • (r₂ /ₒ s₂)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤ * b₂

Tactic:
rw [top_mul (by simpa [bot_eq_zero] using hb.bot_lt.ne')]

Goal state after:
case inl
α : Type u_1
inst✝⁵ : DecidableEq α
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : OrderBot α
inst✝¹ : CanonicallyOrderedAdd α
inst✝ : PosMulStrictMono α
b₂ : WithTop α
this : MulPosStrictMono α
a₁ b₁ : α
hb : ↑b₁ < b₂
ha : ↑a₁ < ⊤
⊢ ↑a₁ * ↑b₁ < ⊤
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 k : ℕ
h : n ≤ n + k
⊢ succ^[n] r ≤ succ^[k + n] r

Tactic:
Function.iterate_add,

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^[k] ∘ succ^[n]) r
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LT α
⊢ IsSuccPrelimit (toDual a) ↔ IsPredPrelimit a

Tactic:
by
  simp [IsSuccPrelimit, IsPredPrelimit]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b : α
⊢ ∀ (x : α), (∀ y < x, a ≤ y → ∃ n, pred^[n] y = a) → a ≤ x → ∃ n, pred^[n] x = a

Tactic:
intro b ih hab

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : PartialOrder α
h : WellFoundedLT α
inst✝ : PredOrder α
a b✝ b : α
ih : ∀ y < b, a ≤ y → ∃ n, pred^[n] y = a
hab : a ≤ b
⊢ ∃ n, pred^[n] b = a
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
· rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : LinearOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : SuccAddOrder α
⊢ x < 1 ↔ x ≤ 0

Tactic:
rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]

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

Goal state before:
pp: n : ℕ∞
m : ℕ
inst✝ : NeZero m
⊢ n.toNat = m ↔ n = ↑m

Tactic:
cases n
  · simpa using NeZero.ne' m
  · simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
X : Type u_3
Y : Type u_4
inst✝² : Preorder X
inst✝¹ : Preorder Y
inst✝ : SuccOrder X
f : X ≃o Y
a✝ : Y
h : f (succ (f.symm a✝)) ≤ a✝
⊢ IsMax a✝

Tactic:
by
    rw [← f.symm.isMax_apply]
    refine max_of_succ_le ?_
    simp [f.le_symm_apply, h]

Goal state after:
Module: Mathlib.Logic.Equiv.List

Goal state before:
pp: α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ∃ a ∈ decodeList v.succ, encodeList a = v.succ

Tactic:
use ofNat α v₁ :: a

Goal state after:
case h
α : Type u_1
inst✝ : Denumerable α
v v₁ v₂ : ℕ
e : unpair v = (v₁, v₂)
h : (v₁, v₂).2 ≤ v
a : List α
h₁ : decodeList v₂ = some a
h₂ : encodeList a = v₂
⊢ ofNat α v₁ :: a ∈ decodeList v.succ ∧ encodeList (ofNat α v₁ :: a) = v.succ
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 : s.Countable
⊢ {t | (f t).Nonempty}.Countable

Tactic:
by
  rw [← Set.countable_coe_iff] at hs ⊢
  have : ∀ t : {t // (f t).Nonempty}, ∃ x : s, x.1 ∈ f t := by
    rintro ⟨t, ⟨x, hx⟩⟩
    exact ⟨⟨x, (h'f t hx)⟩, hx⟩
  choose F hF using this
  have A : Injective F := by
    rintro ⟨t, ht⟩ ⟨t', ht'⟩ htt'
    have A : (f t ∩ f t').Nonempty := by
      refine ⟨F ⟨t, ht⟩, hF ⟨t, _⟩, ?_⟩
      rw [htt']
      exact hF ⟨t', _⟩
    simp only [Subtype.mk.injEq]
    by_contra H
    exact not_disjoint_iff_nonempty_inter.2 A (hf H)
  exact Injective.countable A

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

Goal state before:
pp: case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝

pp: case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b

Tactic:
· exact Lex.inr (hab.lt_of_not_ge fun h => hba <| Lex.inr h)

Goal state after:
case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
c : Chain (α →𝒄 β)
c' : Chain α
a : β
⊢ (ωSup (c.map toMono)).toFun (ωSup c') ≤ a ↔ ωSup (c'.map (ωSup (c.map toMono))) ≤ a

Tactic:
by simp [(c _).ωScottContinuous.map_ωSup]

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

Goal state before:
pp: m : ℕ∞
hm : m ≠ 0
⊢ ↑m * ℵ₀ = ℵ₀

Tactic:
induction m with
  | top => exact aleph0_mul_aleph0
  | coe m => rw [ofENat_nat, nat_mul_aleph0 (mod_cast hm)]

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₃.comp φ₁₂ = φ₁₂₃

Tactic:
simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₂₃.comp φ₁ = φ₁₂₃

Tactic:
simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]

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

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

Tactic:
rintro ⟨ab, ba⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
ba : IsSMulRegular M (b * a)
⊢ IsSMulRegular M a ∧ IsSMulRegular M b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2.inl
b : Cardinal.{u_1}
⊢ 0 * b < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

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

Goal state before:
pp: case refine_2.inr.inl
a : Cardinal.{u_1}
⊢ a * 0 < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

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

Goal state before:
pp: case refine_2.inr.inr
a b : Cardinal.{u_1}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ a * b < ℵ₀

Tactic:
simp only [*, mul_lt_aleph0, aleph0_pos, zero_mul, mul_zero]

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

Goal state before:
pp: case mp
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) → ∃ h, Fintype.card α = n

Tactic:
rintro ⟨t, ht, hn⟩

Goal state after:
case mp
α : Type u
n : ℕ
t : Finset α
ht : ↑t = univ
hn : t.card = n
⊢ ∃ h, Fintype.card α = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (range fun y ↦ a ^ ↑y)

Tactic:
rw [← image_eq_range]

Goal state after:
b c a : Cardinal.{u}
h : c < b
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
a b c : Cardinal.{u}
⊢ BddAbove (range fun c ↦ a ^ ↑c)

Tactic:
rw [← image_eq_range]

Goal state after:
case h
a b c : Cardinal.{u}
⊢ BddAbove (HPow.hPow a '' Iio b)
Module: Mathlib.Algebra.Group.Hom.End

Goal state before:
pp: M : Type uM
inst✝ : AddCommGroup M
⊢ instRing.toAddCommGroup.toSubNegMonoid = instRing.toAddGroupWithOne.toAddGroup.toSubNegMonoid

Tactic:
with_reducible_and_instances rfl

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

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

Tactic:
hf',

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

Goal state before:
pp: R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
by ext <;> exact zero_smul ..

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
R : Type u_5
inst✝⁴ : Zero R
inst✝³ : Zero M
inst✝² : Zero N
inst✝¹ : SMulWithZero R M
inst✝ : SMulWithZero R N
x✝ : M × N
⊢ 0 • x✝ = 0

Tactic:
by ext <;> exact zero_smul ..

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x✝ : M
x y : M₁
⊢ (f x + f y) • x✝ = f x • x✝ + f y • x✝

Tactic:
add_smul

Goal state after:
R : Type u_1
R₂ : Type u_2
S : Type u_3
M : Type u_4
M₁ : Type u_5
M₂ : Type u_6
M₃ : Type u_7
N₁ : Type u_8
inst✝⁸ : Semiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid M₁
inst✝⁵ : Module R M
inst✝⁴ : Module R M₁
inst✝³ : Semiring S
inst✝² : Module R S
inst✝¹ : Module S M
inst✝ : IsScalarTower R S M
f : M₁ →ₗ[R] S
x✝ : M
x y : M₁
⊢ f x • x✝ + f y • x✝ = f x • x✝ + f y • x✝