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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : PartialOrder α
inst✝ : Preorder β
s : Set (Lex (α × β))
hα : ((fun x ↦ (ofLex x).1) '' s).IsPWO
hβ : ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO
⊢ s.IsPWO

Tactic:
by
  rw [IsPWO, partiallyWellOrderedOn_iff_exists_lt]
  intro f hf
  rw [isPWO_iff_exists_monotone_subseq] at hα
  obtain ⟨g, hg⟩ : ∃ (g : (ℕ ↪o ℕ)), Monotone fun n => (ofLex f (g n)).1 :=
    hα (fun n => (ofLex f n).1) (fun k => mem_image_of_mem (fun x => (ofLex x).1) (hf k))
  have hhg : ∀ n, (ofLex f (g 0)).1 ≤ (ofLex f (g n)).1 := fun n => hg n.zero_le
  by_cases! hc : ∃ n, (ofLex f (g 0)).1 < (ofLex f (g n)).1
  · obtain ⟨n, hn⟩ := hc
    use (g 0), (g n)
    constructor
    · by_contra hx
      simp_all
    · exact Prod.Lex.toLex_le_toLex.mpr <| .inl hn
  · have hhc : ∀ n, (ofLex f (g 0)).1 = (ofLex f (g n)).1 := by
      intro n
      exact (hhg n).eq_of_not_lt (hc n)
    obtain ⟨g', hg'⟩ : ∃ g' : ℕ ↪o ℕ, Monotone ((fun n ↦ (ofLex f (g (g' n))).2)) := by
      simp_rw [isPWO_iff_exists_monotone_subseq] at hβ
      apply hβ (ofLex f (g 0)).1 fun n ↦ (ofLex f (g n)).2
      intro n
      rw [hhc n]
      simpa using! hf _
    use (g (g' 0)), (g (g' 1))
    suffices (f (g (g' 0))) ≤ (f (g (g' 1))) by simpa
    · refine Prod.Lex.toLex_le_toLex.mpr <| .inr ⟨?_, ?_⟩
      · exact (hhc (g' 0)).symm.trans (hhc (g' 1))
      · exact hg' (Nat.zero_le 1)

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : x ∈ closure (⋃ i, ↑(S i))
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x

Tactic:
induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy

Goal state after:
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 ((Embedding.subtype fun x ↦ x ∈ s) j) =
    ∏ j ∈ s.erase ((Embedding.subtype fun x ↦ x ∈ s) i), f j

Tactic:
← prod_map

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

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
x y a b : α
h : r a b
ha : r a x
hb : r b y
⊢ r x y

Tactic:
exact trans (symm ha) (trans h hb)

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

Goal state before:
pp: case refl
α : Type u
p : α × Bool
LL₁ LL₂ L₁ L₂ : List (α × Bool)
eq₁ : p :: L₁ = LL₂
eq₂ : p :: L₂ = LL₂
⊢ Red L₁ L₂

Tactic:
| refl =>

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

Goal state before:
pp: case refl
α : Type u
L L₁₂ L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = L
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
| refl =>

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

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ {i ∈ s | g i = x'} → a ∉ {i ∈ s | g i = y'}

Tactic:
mem_filter

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq κ
s : Finset ι
t : Finset κ
g : ι → κ
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ {i ∈ s | g i = x'} → a ∉ {i ∈ s | g i = y'}

Tactic:
mem_filter

Goal state after:
case h
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝¹ : CommMonoid M
s : Finset ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : ι → M
x' : κ
hx : x' ∈ ↑t
y' : κ
hy : y' ∈ ↑t
hne : x' ≠ y'
⊢ ∀ ⦃a : ι⦄, a ∈ s ∧ g a = x' → ¬(a ∈ s ∧ g a = y')
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case refl
α : Type u
L₁ L₂ : List (α × Bool)
⊢ ∃ n, L₁.length = L₁.length + 2 * n

Tactic:
| refl =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → ¬f x = 1 → x ∈ {x ∈ s | p x}

Tactic:
mem_filter

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝¹ : CommMonoid M
f : ι → M
p : ι → Prop
inst✝ : DecidablePred p
hp : ∀ x ∈ s, f x ≠ 1 → p x
x : ι
⊢ x ∈ s → ¬f x = 1 → x ∈ s ∧ p x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: case refine_1
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ {a} ⊆ s

pp: case refine_2
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1

Tactic:
· intro _ H
          rwa [mem_singleton.1 H]

Goal state after:
case refine_2
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∀ x ∈ s, x ∉ {a} → f x = 1
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
this✝ : DecidableEq ι
b : ι
hb : b ∈ s
h₀ : ∀ b_1 ∈ s, b_1 ≠ b → f b_1 = 1
h₁ : b ∉ s → f b = 1
this : b ∉ s
⊢ False

Tactic:
exact this hb

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

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ ∀ (a b : FreeGroup α), Quot.lift (Lift.aux f) ⋯ (a * b) = Quot.lift (Lift.aux f) ⋯ a * Quot.lift (Lift.aux f) ⋯ b

Tactic:
rintro ⟨L₁⟩ ⟨L₂⟩; simp [Lift.aux, List.prod_append]

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

Goal state before:
pp: case pos.e_a
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
⊢ ∏ x ∈ s.toFinset.erase a, f x ^ count x s = ∏ x ∈ s.toFinset.erase a, f x ^ count x (a :: s)

Tactic:
refine prod_congr rfl fun x hx => ?_

Goal state after:
case pos.e_a
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
f : ι → M
a : ι
s : List ι
IH : (List.map f s).prod = ∏ m ∈ s.toFinset, f m ^ count m s
has : a ∈ s.toFinset
x : ι
hx : x ∈ s.toFinset.erase a
⊢ f x ^ count x s = f x ^ count x (a :: s)
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
⊢ ∃ S, closure S = P ∧ S.Finite

Tactic:
refine ⟨_, ?_, (setOfPred_minimal_antichain _).finite_of_partiallyWellOrderedOn
    (hpwo.mono (setOfPred_minimal_subset _))⟩

Goal state after:
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
⊢ closure {x | Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) x} = P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case neg.a.a
M : Type u_5
inst✝⁴ : CommMonoid M
inst✝³ : PartialOrder M
inst✝² : WellQuasiOrderedLE M
inst✝¹ : IsOrderedCancelMonoid M
inst✝ : CanonicallyOrderedMul M
P : Submonoid M
hP : ∀ x ∈ P, ∀ (y : M), x * y ∈ P → y ∈ P
hpwo : {x | x ∈ P ∧ x ≠ 1}.IsPWO
x : M
hx₁ : x ∈ P
hx₂ : ¬x = 1
z : M
hz₂ : z ∈ P
hz₃ : z ≠ 1
y : M
x✝ : z * y ∈ {x | x ∈ P ∧ x ≠ 1}
hy₁ : z * y ∈ P
hy₂ : z * y ≠ 1
ih : ∀ z_1 ∈ P, z_1 ≠ 1 → z_1 ≤ z * y → ¬z * y ≤ z_1 → z_1 ∈ closure {x | Minimal (fun x ↦ x ∈ P ∧ x ≠ 1) x}
hy₃ : ¬Minimal (fun x ↦ x ∈ {x | x ∈ P ∧ x ≠ 1}) (z * y)
hz₁ : z < z * y
⊢ y ≤ z * y

Tactic:
exact le_mul_self

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

Goal state before:
pp: case h₁
G : Type u_1
inst✝ : Group G
⊢ ⇑(closureCommutatorRepresentatives G).subtype '' commutatorSet ↥(closureCommutatorRepresentatives G) ⊆ commutatorSet G

Tactic:
rintro - ⟨-, ⟨g₁, g₂, rfl⟩, rfl⟩

Goal state after:
case h₁
G : Type u_1
inst✝ : Group G
g₁ g₂ : ↥(closureCommutatorRepresentatives G)
⊢ (closureCommutatorRepresentatives G).subtype ⁅g₁, g₂⁆ ∈ commutatorSet G
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.zero
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 : α
⊢ (lift ⇑f) (0 * of L2) = (lift ⇑f) 0 * (lift ⇑f) (of L2)

Tactic:
simp only [zero_mul, map_zero]

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 : X
s : ↥S
r' : X
s' u : ↥S
v : R
hru : u • r' = v • r
hsu : ↑u * ↑s' = v * ↑s
r₂ : R
s₂ : ↥S
h₁ : ↑s₂ * ↑s = r₂ * ↑s'
r₃ : R
s₃ : ↥S
h₂ : ↑s₃ * r₂ = r₃ * ↑u
⊢ r₃ * v * ↑s = ↑s₃ * ↑s₂ * ↑s

Tactic:
rw [mul_assoc _ (s₂ : R), h₁, ← mul_assoc, h₂, mul_assoc, ← hsu, ← mul_assoc]

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

Goal state before:
pp: case mp.mpr
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)
H : Injective ⇑(f.lift hg)
x y : M
⊢ g x = g y → f x = f y

Tactic:
intro h
      rw [← f.lift_eq hg, ← f.lift_eq hg] at h
      exact H h

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

Goal state before:
pp: M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
x₁ x₂ : M
y : ↥S
⊢ f x₁ * f.mk' x₂ y = f.mk' (x₁ * x₂) y

Tactic:
by
  rw [← mk'_one, ← mk'_mul, one_mul]

Goal state after:
Module: Mathlib.Order.Iterate

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

Tactic:
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.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n + 1] x

Tactic:
iterate_succ_apply

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : Monotone f
hx : x ≤ f x
n : ℕ
⊢ f^[n] x ≤ f^[n] (f x)
Module: Mathlib.Order.Iterate

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n + 1] x

Tactic:
iterate_succ_apply

Goal state after:
α : Type u_1
inst✝ : Preorder α
f : α → α
x : α
hf : StrictMono f
hx : x < f x
n : ℕ
⊢ f^[n] x < f^[n] (f x)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
⊢ f (succ a) = succ (f a)

Tactic:
by
  by_cases h : IsMax a
  · rw [h.succ_eq, (f.isMax_apply.2 h).succ_eq]
  · exact ((apply_covBy_apply_iff f).2 <| covBy_succ_of_not_isMax h).succ_eq.symm

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

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

Tactic:
rw [lt_succ_iff_of_not_isMax hb, succ_le_iff_of_not_isMax ha]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
⊢ ∀ (a b : SuccOrder α), a = b

Tactic:
intro h₀ h₁

Goal state after:
α : Type u_1
β : Type u_2
inst✝ : PartialOrder α
h₀ h₁ : SuccOrder α
⊢ h₀ = h₁
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.succ
α : 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
⊢ f (pred (pred^[n + 1] b)) < f b

Tactic:
by_cases ha' : IsMin (pred^[n + 1] b)

Goal state after:
case pos
α : 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

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
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| n

Tactic:
← s.2,

Goal state after:
α : Type u_1
β : Type u_2
n n' m : ℕ
s✝ : Sym α n
a b : α
s : Sym α n
| (↑s).card
Module: Mathlib.Data.Sym.Basic

Goal state before:
pp: case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ ((if ¬a = b then count b ↑m else 0) + if a = b then count a ↑m else 0) = count b ↑m

Tactic:
if_pos h,

Goal state after:
case inr
α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a : α
m : Sym α n
b : α
h : a ≠ b
⊢ (count b ↑m + if a = b then count a ↑m else 0) = count b ↑m
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ enumerateCountable h default n ∈ s

Tactic:
convert! mem_range_self n

Goal state after:
case e'_4
α : Type u
s : Set α
h : s.Countable
default : α
h_mem : default ∈ s
n : ℕ
⊢ s = range (enumerateCountable h default)
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
s t : Set α
⊢ (s ∪ t).Countable ↔ s.Countable ∧ t.Countable

Tactic:
simp [union_eq_iUnion, and_comm]

Goal state after:
Module: Mathlib.Order.Hom.Lex

Goal state before:
pp: α : Type u_1
r : α → α → Prop
x y : α
inst✝² : IsTrans α r
inst✝¹ : Std.Trichotomous r
inst✝ : DecidableRel r
⊢ ∀ {a b : { x_1 // ¬r x x_1 } ⊕ Subtype (r x)},
    r (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) a)
        (((Equiv.sumComm { x_1 // ¬r x x_1 } (Subtype (r x))).trans (Equiv.sumCompl (r x))) b) ↔
      Sum.Lex (Subrel r fun x_1 ↦ ¬r x x_1) (Subrel r (r x)) a b

Tactic:
rintro (⟨a, ha⟩ | ⟨a, ha⟩) (⟨b, hb⟩ | ⟨b, hb⟩)
    · simp
    · simpa using trans_trichotomous_left ha hb
    · simpa using fun h ↦ hb <| trans ha h
    · simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMinOrder (α ⊕ β)
a : β
⊢ ∃ b, b < a

Tactic:
obtain ⟨b | b, h⟩ := exists_lt (inr a : α ⊕ β)
        · exact (not_inl_lt_inr h).elim
        · exact ⟨b, inr_lt_inr_iff.1 h⟩

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

Goal state before:
pp: ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
⊢ lift.{u, v} a ^ sum f = prod fun i ↦ a ^ f i

Tactic:
by
  induction a using Cardinal.inductionOn with | _ α =>
  induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
b : α ⊕ β
⊢ Sum.Lex r s b ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    b ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
by
    cases b <;> [exact fun _ => ⟨_, rfl⟩; exact False.elim ∘ Sum.lex_inr_inl]

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: case mp
α : Type u_1
o : Part α
⊢ o.Dom → ∃ x, o = some x

Tactic:
exact fun h => ⟨o.get h, eq_some_iff.2 (get_mem h)⟩

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case image_self_subset_self.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
⊢ f z ≤ y ∨ f y ≤ f z

Tactic:
rcases le_iff_lt_or_eq.1 hzy with (hzy | rfl)

Goal state after:
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 ∨ f y ≤ f z

case image_self_subset_self.inl.inr
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
z : α
hz : z ∈ bot x f
hy : IsExtremePt x f z
hzy : z ≤ z
⊢ f z ≤ z ∨ f z ≤ f z
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : β → γ
g : α → Part β
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ f <$> g x

Tactic:
simpa only [map_eq_bind_pure_comp] using! ωScottContinuous.bind hg ωScottContinuous.const

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

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
| ∀ ⦃a₁ a₂ : M⦄, n • a₁ = n • a₂ → a₁ = a₂

Tactic:
rw [← n.sign_mul_natAbs]

Goal state after:
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
| ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
by
  rw [← mk_univ, mk_set_eq_nat_iff_finset]

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

Goal state before:
pp: I : Type u
f : I → Type v
g : I → Type u_1
m : (i : I) → Monoid (f i)
n : (i : I) → Monoid (g i)
inst✝ : (i : I) → MulDistribMulAction (f i) (g i)
r✝ : (i : I) → f i
x✝ y✝ : (i : I) → g i
x : I
⊢ (r✝ • (x✝ * y✝)) x = (r✝ • x✝ * r✝ • y✝) x

Tactic:
apply smul_mul'

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 σ₂₁
p : Submodule R₂ M₂
q : Submodule R M
f : M₂ →ₛₗ[σ₂₁] M
h : ∀ x ∈ p, f x ∈ q
p' : Submodule R₂ ↥p
⊢ map (f.restrict h) p' = comap q.subtype (map f (map p.subtype p'))

Tactic:
rw [restrict_eq_codRestrict_domRestrict, map_codRestrict, map_domRestrict]

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

Goal state before:
pp: R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
s : Set R
sm : Submonoid R
hm : ↑sm = s
sa : AddSubmonoid R
ha : ↑sa = s
x y : R
⊢ x ∈ s → y ∈ s → x * y ∈ s

Tactic:
simpa only [← hm] using! sm.mul_mem

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

Goal state before:
pp: case mul.neg_right
R : Type u
inst✝ : NonUnitalNonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Subsemigroup.closure s)

Tactic:
simpa [mul_neg] using neg_mem h

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

Goal state before:
pp: case mul.neg_right
R : Type u
inst✝ : NonAssocRing R
s : Set R
x x✝¹ y✝¹ x✝ y✝ : R
hx✝ : x✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
hy✝ : y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
h : x✝ * y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)
⊢ x✝ * -y✝ ∈ AddSubgroup.closure ↑(Submonoid.closure s)

Tactic:
simpa [mul_neg] using neg_mem h

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Lemmas

Goal state before:
pp: case mp.refine_2
M : Type u_2
inst✝ : Monoid M
x y : M
h : Irreducible (x * y)
h' : IsUnit x
⊢ Irreducible y

Tactic:
· rwa [irreducible_isUnit_mul h'] at h

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

Goal state before:
pp: case cons.inl
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

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

pp: 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, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)

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

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

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, (∀ x ∈ L, x ∈ s) ∧ (hd.prod = L.prod ∨ hd.prod = -L.prod)
Module: Mathlib.Algebra.GroupWithZero.Associated

Goal state before:
pp: M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a b : M
hab : a ∣ b
hba : b ∣ a
⊢ a ~ᵤ b

Tactic:
rcases hab with ⟨c, rfl⟩

Goal state after:
M : Type u_1
inst✝¹ : MonoidWithZero M
inst✝ : IsLeftCancelMulZero M
a c : M
hba : a * c ∣ a
⊢ a ~ᵤ a * c
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ M₀⁰ ↔ ∀ (x : M₀), x * r = 0 → x = 0

Tactic:
← nonZeroDivisorsRight_eq_nonZeroDivisors

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
r : M₀
⊢ r ∈ nonZeroDivisorsRight M₀ ↔ ∀ (x : M₀), x * r = 0 → x = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ M₀⁰ ∧ b ∈ M₀⁰

Tactic:
← nonZeroDivisorsRight_eq_nonZeroDivisors

Goal state after:
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
⊢ a ∈ nonZeroDivisorsRight M₀ ∧ b ∈ nonZeroDivisorsRight M₀