mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: G : Type u_1
inst✝ : Group G
s : Set G
x : G
hx : x ∈ center G
y : G
⊢ y ∈ s ↔ x * y * x⁻¹ ∈ s

Tactic:
simp [← mem_center_iff.mp hx y]

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

Goal state before:
pp: M : Type u_1
inst✝ : MulOneClass M
x✝ : M
⊢ Commute 1 x✝

Tactic:
commute_iff_eq,

Goal state after:
M : Type u_1
inst✝ : MulOneClass M
x✝ : M
⊢ 1 * x✝ = x✝ * 1
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝ : Group G
⊢ fixedPoints (ConjAct G) G = ↑(center G)

Tactic:
ext x
  simp [mem_center_iff, smul_def, mul_inv_eq_iff_eq_mul]

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

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β → β
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
h' : {x | x ∈ s}.Pairwise fun x y ↦ ∀ (b : β), f x (f y b) = f y (f x b)
b : β
⊢ noncommFoldr f (a ::ₘ s) h b = f a (noncommFoldr f s h' b)

Tactic:
induction s using Quotient.inductionOn
  simp

Goal state after:
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:
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 α
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:
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:
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 = a * s.noncommProd ⋯

Tactic:
induction s using Quotient.inductionOn
  simp

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

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

Tactic:
induction s using Quotient.inductionOn
  simp

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

Goal state before:
pp: case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ MulAut.conj h • H

Tactic:
rw [subset_pointwise_smul_iff, ← map_inv]

Goal state after:
case refine_2
G : Type u_2
inst✝ : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ MulAut.conj h⁻¹ • H ≤ H
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case mpr
α : Type u
L₁ L₂ : List (α × Bool)
a : α
b : Bool
⊢ (∃ L, Step L₁ L ∧ L₂ = (a, b) :: L) ∨ L₁ = (a, !b) :: L₂ → Step ((a, b) :: L₁) L₂

Tactic:
rintro (⟨L, h, rfl⟩ | rfl)

Goal state after:
case mpr.inl
α : Type u
L₁ : List (α × Bool)
a : α
b : Bool
L : List (α × Bool)
h : Step L₁ L
⊢ Step ((a, b) :: L₁) ((a, b) :: L)

case mpr.inr
α : Type u
L₂ : List (α × Bool)
a : α
b : Bool
⊢ Step ((a, b) :: (a, !b) :: L₂) L₂
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: case tail
α : Type u
L L₁₂ b✝ c✝ : List (α × Bool)
hLL' : ReflTransGen Step L b✝
h : Step b✝ c✝
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = b✝ → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
L₁ L₂ : List (α × Bool)
eq : L₁ ++ L₂ = c✝
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂

Tactic:
obtain @⟨s, e, a, b⟩ := h

Goal state after:
case tail
α : Type u
L L₁₂ L₁ L₂ s e : List (α × Bool)
a : α
b : Bool
hLL' : ReflTransGen Step L (s ++ (a, b) :: (a, !b) :: e)
ih : ∀ {L₁ L₂ : List (α × Bool)}, L₁ ++ L₂ = s ++ (a, b) :: (a, !b) :: e → ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
eq : L₁ ++ L₂ = s ++ e
⊢ ∃ L₃ L₄, L = L₃ ++ L₄ ∧ Red L₃ L₁ ∧ Red L₄ L₂
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'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
simp_rw [disjoint_left, 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'
⊢ (Disjoint on fun j ↦ {i ∈ s | g i = j}) x' y'

Tactic:
simp_rw [disjoint_left, 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.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
let s' := ({a, b} : Finset ι)

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
s' : Finset ι := {a, b}
⊢ ∏ x ∈ s, f x = f a * f b
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
P Q : Submonoid M
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG

Tactic:
classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ ⇑e '' ⇑e ⁻¹' ↑s = ↑s

Tactic:
rw [Set.image_preimage_eq_iff, ← MonoidHom.coe_mrange e, ← Submonoid.closure_le, hs,
      MonoidHom.mrange_eq_map e]

Goal state after:
case h
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
P : Submonoid M
e : M →* M'
he : Function.Injective ⇑e
s : Finset M'
hs : closure ↑s = Submonoid.map e P
⊢ Submonoid.map e P ≤ Submonoid.map e ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.map f ⊤ = ⊤

Tactic:
← MonoidHom.mrange_eq_map,

Goal state after:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ MonoidHom.mrange f = ⊤
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: G : Type u_3
inst✝ : Group G
P Q : Subgroup G
hP : P.FG
hQ : Q.FG
⊢ (P ⊔ Q).FG

Tactic:
classical
  rcases hP with ⟨s, rfl⟩
  rcases hQ with ⟨t, rfl⟩
  exact ⟨s ∪ t, by simp [closure_union]⟩

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H₁ H₂ : Subgroup G
⊢ H₂ ≤ normalizer ↑⁅H₂, H₁⁆

Tactic:
apply normalizer_commutator_ge_left

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
a b : M
d : ↥S
⊢ f.mk' a d = f.mk' b d ↔ ∃ c, ↑c * a = ↑c * b

Tactic:
rw [mk'_eq_iff_eq', map_mul, map_mul, ← eq_iff_exists f]

Goal state after:
M : Type u_1
inst✝¹ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝ : CommMonoid N
f : S.LocalizationMap N
a b : M
d : ↥S
⊢ f a * f ↑d = f b * f ↑d ↔ f a = f b
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = ↑(fS s)⁻¹ * f r

Tactic:
← huniv r,

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = ↑(fS s)⁻¹ * φ (numeratorHom r)
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ∃ c, ⟨b, ⋯⟩ < c ∧ c < a
⊢ False

Tactic:
obtain ⟨c, hc, hc'⟩ := this

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
c : ↑s
hc : ⟨b, ⋯⟩ < c
hc' : c < a
⊢ False
Module: Mathlib.Order.SuccPred.Basic

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

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

Tactic:
· simpa using hin

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

Goal state before:
pp: case zero
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
hb : succ^[0] a ∈ s
hab : a < succ^[0] a
⊢ f a < f (succ^[0] a)

pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : a < succ^[n + 1] a
⊢ f a < f (succ^[n + 1] a)

Tactic:
· simp at hab

Goal state after:
case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMax a → a ∈ s → succ a ∈ s → f a < f (succ a)
a : α
ha : a ∈ s
n : ℕ
hb : succ^[n + 1] a ∈ s
hab : a < succ^[n + 1] a
⊢ f a < f (succ^[n + 1] a)
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case top
m : ℕ
inst✝ : NeZero m
⊢ ⊤.toNat = m ↔ ⊤ = ↑m

pp: case coe
m : ℕ
inst✝ : NeZero m
a✝ : ℕ
⊢ (↑a✝).toNat = m ↔ ↑a✝ = ↑m

Tactic:
· simpa using NeZero.ne' m

Goal state after:
case coe
m : ℕ
inst✝ : NeZero m
a✝ : ℕ
⊢ (↑a✝).toNat = m ↔ ↑a✝ = ↑m
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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
⊢ MonotoneOn f s

Tactic:
by
  rintro a ha b hb hab
  obtain ⟨n, rfl⟩ := exists_pred_iterate_of_le hab
  clear hab
  induction n with
  | zero => simp
  | succ n hn =>
    rw [Function.iterate_succ_apply'] at ha ⊢
    have : pred^[n] b ∈ s := hs.1 ha hb ⟨pred_le _, pred_iterate_le ..⟩
    by_cases ha' : IsMin (pred^[n] b)
    · rw [pred_eq_iff_isMin.2 ha']
      exact hn this
    · exact (hn this).trans' (hf _ ha' this ha)

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

Goal state before:
pp: case zero
α : 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
ha : pred^[0] b ∈ s
hab : pred^[0] b < b
⊢ f (pred^[0] b) < f b

pp: case 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
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : pred^[n + 1] b < b
⊢ f (pred^[n + 1] b) < f b

Tactic:
· simp at hab

Goal state after:
case 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
n : ℕ
ha : pred^[n + 1] b ∈ s
hab : pred^[n + 1] b < b
⊢ f (pred^[n + 1] b) < f b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case nil
n : ℕ
F G : Type u → Type u
inst✝² : Applicative F
inst✝¹ : Applicative G
inst✝ : LawfulApplicative G
α β γ : Type u
f : β → F γ
g : α → G β
⊢ Vector.traverse (Comp.mk ∘ Functor.map f ∘ g) nil = Comp.mk (Vector.traverse f <$> Vector.traverse g nil)

Tactic:
simp! [cast, *, functor_norm]
    rfl

Goal state after:
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
F : { t // (f t).Nonempty } → ↑s
hF : ∀ (t : { t // (f t).Nonempty }), ↑(F t) ∈ f ↑t
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t, ht⟩) ∈ f t'

Tactic:
rw [htt']

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
t : β
ht : (f t).Nonempty
t' : β
ht' : (f t').Nonempty
htt' : F ⟨t, ht⟩ = F ⟨t', ht'⟩
⊢ ↑(F ⟨t', ht'⟩) ∈ f t'
Module: Mathlib.Data.Sum.Order

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

Tactic:
· exact (not_inr_lt_inl h).elim

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

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

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b

Tactic:
· exact (not_inr_lt_inl h).elim

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : NoMaxOrder (α ⊕ β)
a b : β
h : inr a < inr b
⊢ ∃ b, a < b
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
hab : a < b
⊢ ¬b ≤ a

Tactic:
rintro (⟨hba⟩ | ⟨hba⟩ | ⟨b, a⟩)
        · exact hba.not_gt (inl_lt_inl_iff.1 hab)
        · exact hba.not_gt (inr_lt_inr_iff.1 hab)
        · exact not_inr_lt_inl hab

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ioi a = Ioi (e a)

Tactic:
by
  rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsLowerSet s
⊢ s = univ ∨ ∃ a, s = Iio a

Tactic:
simp_rw [← @compl_inj_iff _ s]
  simpa using h.compl.eq_empty_or_Ici

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
x : β
⊢ s x a ↔ s x b

Tactic:
rw [← hf, hg]

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

Goal state before:
pp: case bot.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ⊥ ≤ ↑a✝

pp: case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ ⊥

pp: case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝

Tactic:
· simp only [elim_inr, elim_inl, Lex.sep, bot_le]

Goal state after:
case coe.bot
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ⊥, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝ ≤ ⊥

case coe.coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : LE α
a✝¹ a✝ : α
⊢ Sum.Lex (fun x1 x2 ↦ True) (fun x1 x2 ↦ x1 ≤ x2)
      (Sum.elim inr inl
        (match ↑a✝¹, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y))
      (Sum.elim inr inl
        (match ↑a✝, inr PUnit.unit, inl with
        | Option.some x, x_1, f => f x
        | none, y, x => y)) ↔
    ↑a✝¹ ≤ ↑a✝
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
c : Chain α
f : α →o β
b : β
h : ∃ a ∈ c, f a = b
⊢ b ∈ c.map f

Tactic:
rcases h with ⟨w, h, h'⟩
    subst b
    apply mem_map c _ h

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
⊢ cSup c ∈ {y | IsExtremePt x f y}

Tactic:
refine ⟨(bot_isAdmissible le_map).cSup_mem _ (subset_trans hc (fun _ h ↦ h.mem_bot)), ?_⟩

Goal state after:
case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
⊢ ∀ {z : α}, z ∈ bot x f → z < cSup c → f z ≤ cSup c
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
h : c < ℵ₀
⊢ ↑(toNat c) = ↑(Classical.choose ⋯)

Tactic:
rw [cast_toNat_of_lt_aleph0 h, ← Classical.choose_spec (lt_aleph0.1 h)]

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

Goal state before:
pp: ⊢ ∀ (i i_1 : ℕ), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

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

Goal state before:
pp: c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : (∀ (a : ℕ), ↑a ≤ c) ↔ ∀ (a : ℕ), ↑a ≤ d
⊢ toNat c = toNat d

Tactic:
rw [← Cardinal.aleph0_le, ← Cardinal.aleph0_le] at h'

Goal state after:
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: ⊢ ∀ (i i_1 : ℕ∞), i < i_1 → i < i_1

Tactic:
exact fun _ _ ↦ id

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

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

Tactic:
IsSMulRegular,

Goal state after:
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ (Function.Injective fun x ↦ n.natAbs • x) ↔ Function.Injective fun x ↦ n • x
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)

Tactic:
induction n with
  | zero => rw [pow_zero]; simp only [one]
  | succ n hn =>
    rw [pow_succ']
    exact (ra.smul_iff (a ^ n)).mpr hn

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ h, Fintype.card α = n

Tactic:
rw [mk_eq_nat_iff_finset]

Goal state after:
α : Type u
n : ℕ
⊢ (∃ t, ↑t = univ ∧ t.card = n) ↔ ∃ h, Fintype.card α = n
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
classical
  exact Quot.sound ⟨Equiv.Set.unionSumInter S T⟩

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

Goal state before:
pp: case pos
α : Type u
s : Set α
a : α
h : a ∈ s
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
simp only [insert_eq_of_mem h, self_le_add_right]

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

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ c ≤ #↑s ↔ ∃ p ⊆ s, #↑p = c

Tactic:
le_mk_iff_exists_set,

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ (∃ p, #↑p = c) ↔ ∃ p ⊆ s, #↑p = c
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
R₁ : Type u_9
R₂ : Type u_10
R₁' : Type u_11
R₂' : Type u_12
M₁ : Type u_13
M₂ : Type u_14
M₁' : Type u_15
M₂' : Type u_16
inst✝¹⁹ : Semiring R₁
inst✝¹⁸ : Semiring R₂
inst✝¹⁷ : Semiring R₁'
inst✝¹⁶ : Semiring R₂'
inst✝¹⁵ : AddCommMonoid M₁
inst✝¹⁴ : AddCommMonoid M₂
inst✝¹³ : AddCommMonoid M₁'
inst✝¹² : AddCommMonoid M₂'
inst✝¹¹ : Module R₁ M₁
inst✝¹⁰ : Module R₂ M₂
inst✝⁹ : Module R₁' M₁'
inst✝⁸ : Module R₂' M₂'
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁'₂' : R₁' →+* R₂'
σ₂'₁' : R₂' →+* R₁'
σ₁₁' : R₁ →+* R₁'
σ₂₂' : R₂ →+* R₂'
σ₂₁' : R₂ →+* R₁'
σ₁₂' : R₁ →+* R₂'
inst✝⁷ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁶ : RingHomInvPair σ₂₁ σ₁₂
inst✝⁵ : RingHomInvPair σ₁'₂' σ₂'₁'
inst✝⁴ : RingHomInvPair σ₂'₁' σ₁'₂'
inst✝³ : RingHomCompTriple σ₁₁' σ₁'₂' σ₁₂'
inst✝² : RingHomCompTriple σ₂₁ σ₁₂' σ₂₂'
inst✝¹ : RingHomCompTriple σ₂₂' σ₂'₁' σ₂₁'
inst✝ : RingHomCompTriple σ₁₂ σ₂₁' σ₁₁'
e₁ : M₁ ≃ₛₗ[σ₁₂] M₂
e₂ : M₁' ≃ₛₗ[σ₁'₂'] M₂'
f : M₂ →ₛₗ[σ₂₂'] M₂'
⊢ (fun f ↦ (↑e₂ ∘ₛₗ f) ∘ₛₗ ↑e₁.symm) ((fun f ↦ (↑e₂.symm ∘ₛₗ f) ∘ₛₗ ↑e₁) f) = f

Tactic:
by
    ext x
    simp only [Function.comp_apply, apply_symm_apply, coe_comp, coe_coe]

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₂
f : M →ₛₗ[τ₁₂] M₂
hf : Injective ⇑f
⊢ f.ker = ⊥

Tactic:
rw [eq_bot_iff]
  intro x hx
  simpa only [mem_ker, mem_bot, ← map_zero f, hf.eq_iff] using hx

Goal state after: