mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case mpr
α : Type u_1
κ : Sort u_4
r : α → α → Prop
f : κ → Set α
hd : Directed (fun x1 x2 ↦ x1 ⊆ x2) f
⊢ (∀ (n : κ), (f n).Pairwise r) → (⋃ n, f n).Pairwise r

Tactic:
intro H i hi j hj hij
    rcases mem_iUnion.1 hi with ⟨m, hm⟩
    rcases mem_iUnion.1 hj with ⟨n, hn⟩
    rcases hd m n with ⟨p, mp, np⟩
    exact H p (mp hm) (np hn) hij

Goal state after:
Module: Mathlib.Data.Set.Pairwise.Lattice

Goal state before:
pp: case inl
α : Type u_1
ι : Type u_2
ι' : Type u_3
inst✝ : CompleteLattice α
s : Set ι'
g : ι' → Set ι
f : ι → α
hs : s.PairwiseDisjoint fun i' ↦ ⨆ i ∈ g i', f i
hg : ∀ i ∈ s, (g i).PairwiseDisjoint f
a b : ι
hab : a ≠ b
c : ι'
hc : c ∈ s
ha : a ∈ g c
d : ι'
hd : d ∈ s
hb : b ∈ g d
hcd : g c = g d
⊢ (Disjoint on f) a b

Tactic:
exact hg d hd (hcd ▸ ha) hb hab

Goal state after:
Module: Mathlib.Data.List.Sublists

Goal state before:
pp: case cons
α : Type u
h : α
tl : List α
l_ih : flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'
⊢ flatMap (fun n ↦ sublistsLen n tl) (range (tl.length + 1)) ~ tl.sublists'

Tactic:
exact l_ih

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

Goal state before:
pp: α : Type u_1
s : Finset α
β : Type u_2
inst✝ : DecidableEq β
f : α → β
H : Set.InjOn f ↑s
⊢ Set.InjOn (fun x ↦ image f x) ↑s.powerset

Tactic:
by
  have {z a} (_ : z ⊆ s) (_ : a ∈ s) : a ∈ z ↔ f a ∈ z.image f := by grind [H.eq_iff]
  exact fun _ _ _ _ _ => by grind

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
⊢ (insert a s).powerset = s.powerset ∪ image (insert a) s.powerset

Tactic:
by
  ext t
  simp only [mem_powerset, mem_image, mem_union, subset_insert_iff]
  grind

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

Goal state before:
pp: case mpr
α : Type u_1
s a✝ : Finset α
⊢ a✝ = s → a✝ ⊆ s ∧ #a✝ = #s

Tactic:
rintro rfl
    simp

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

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ #(eraseNone s) = #s - 1

Tactic:
card_eraseNone_eq_card_erase,

Goal state after:
α : Type u_1
s : Finset (Option α)
h : none ∈ s
⊢ #(s.erase none) = #s - 1
Module: Mathlib.Data.Finset.Option

Goal state before:
pp: α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #(eraseNone s) = #s

Tactic:
card_eraseNone_eq_card_erase,

Goal state after:
α : Type u_1
s : Finset (Option α)
h : none ∉ s
⊢ #(s.erase none) = #s
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type u_1
s : Set ι
hs : s.Finite
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), (t i hi).Finite
⊢ (⋃ i, ⋃ (h : i ∈ s), t i h).Finite

Tactic:
by
  have := hs.to_subtype
  rw [biUnion_eq_iUnion]
  apply finite_iUnion fun i : s => ht i.1 i.2

Goal state after:
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b c : α
h : a ⩿ b
⊢ c = a ∨ c = b → a ≤ c ∧ c ≤ b

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
b c : α
h : c ⩿ b
⊢ c ≤ c ∧ c ≤ b

case inr
α : Type u_1
inst✝ : PartialOrder α
a c : α
h : a ⩿ c
⊢ a ≤ c ∧ c ≤ c
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrderBot α
a : α
f : ι → α
h : BddAbove (range f)
⊢ a < iSup f ↔ ∃ i, a < f i

Tactic:
simpa only [not_le, not_forall] using (ciSup_le_iff' h).not

Goal state after:
Module: Mathlib.Order.Preorder.Finite

Goal state before:
pp: α : Type u_4
β : Type u_5
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
inst✝ : Finite α
f g : α ↪o β
h : Set.range ⇑f = Set.range ⇑g
ef : ↑Set.univ ≃o ↑(⇑f '' Set.univ) := StrictMonoOn.orderIso (⇑f) Set.univ ⋯
eg : ↑Set.univ ≃o ↑(⇑g '' Set.univ) := StrictMonoOn.orderIso (⇑g) Set.univ ⋯
i : ↑(⇑f '' Set.univ) ≃o ↑(⇑g '' Set.univ) :=
  let __spread.0 := Equiv.setCongr ⋯;
  { toEquiv := __spread.0, map_rel_iff' := ⋯ }
⊢ (ef.trans i).trans eg.symm = OrderIso.refl ↑Set.univ

Tactic:
exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
⊢ i < a → ∃ a_2, (n ≤ a_2 ∧ a_2 < n + a) ∧ a_2 % a = i

Tactic:
intro hia

Goal state after:
case inr.mpr
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
⊢ ∃ a_1, (n ≤ a_1 ∧ a_1 < n + a) ∧ a_1 % a = i
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
⊢ False

Tactic:
obtain ⟨f, hStrictMono | hStrictAnti⟩ := Infinite.exists_strictMono_or_strictAnti α

Goal state after:
case inl
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictMono : StrictMono f
⊢ False

case inr
α : Type u_2
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : WellFoundedGT α
a✝ : Infinite α
f : ℕ → α
hStrictAnti : StrictAnti f
⊢ False
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ (range' a b).toFinset ↔ x ∈ Ico a (a + b)

Tactic:
List.mem_toFinset,

Goal state after:
a b x : ℕ
⊢ x ∈ range' a b ↔ x ∈ Ico a (a + b)
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a x : ℕ
⊢ x ∈ (range' 1 a).toFinset ↔ x ∈ Icc 1 a

Tactic:
List.mem_toFinset,

Goal state after:
a x : ℕ
⊢ x ∈ range' 1 a ↔ x ∈ Icc 1 a
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a x : ℕ
⊢ x ∈ (range a).toFinset ↔ x ∈ Finset.range a

Tactic:
List.mem_toFinset,

Goal state after:
a x : ℕ
⊢ x ∈ range a ↔ x ∈ Finset.range a
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y ↦ P ↑y
⊢ P x

Tactic:
change Q ⟨x, hx⟩

Goal state after:
α : Type u_2
r : α → α → Prop
s : Set α
x : α
hs : s.WellFoundedOn r
hx : x ∈ s
P : α → Prop
hP : ∀ y ∈ s, (∀ z ∈ s, r z y → P z) → P y
Q : ↑s → Prop := fun y ↦ P ↑y
⊢ Q ⟨x, hx⟩
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Preorder α
inst✝ : WellQuasiOrderedLE α
f : (fun x1 x2 ↦ x1 > x2) ↪r fun x1 x2 ↦ x1 < x2
a b : ℕ
h : a < b
hf : f a ≤ f b
⊢ False

Tactic:
exact (f.map_rel_iff.2 h).not_ge hf

Goal state after:
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc a₁ a₂ ∩ Ioc b₁ b₂ = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁

Tactic:
Ioc_inter_Ioc,

Goal state after:
α : Type u_2
a₁ a₂ b₁ b₂ : α
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
⊢ Ioc (max a₁ b₁) (min a₂ b₂) = ∅ ↔ min a₂ b₂ ≤ max a₁ b₁
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
s : Set α
hs : s.PartiallyWellOrderedOn r
f : ℕ → α
hf : ∀ (m n : ℕ), m < n → ¬r (f m) (f n)
this : ∀ (k : ℕ), ∃ m, k < m ∧ f m ∈ s
⊢ ¬BddAbove (f ⁻¹' s)

Tactic:
simpa [not_bddAbove_iff, and_comm]

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }

Tactic:
refine Nat.rec ?_ fun n fn => ?_

Goal state after:
case refine_1
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s Nat.zero f }

case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
n : ℕ
fn : { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f }
⊢ { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n.succ f }
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs m) m = g m

Tactic:
← hg1 m mn

Goal state after:
case refine_2
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f0 : ℕ → α
hf0 : IsBadSeq r s f0
fs : (n : ℕ) → { f // IsBadSeq r s f ∧ IsMinBadSeq r rk s n f } :=
  fun t ↦
    Nat.rec ⟨↑(minBadSeqOfBadSeq r rk s 0 f0 hf0), ⋯⟩ (fun n fn ↦ ⟨↑(minBadSeqOfBadSeq r rk s (n + 1) ↑fn ⋯), ⋯⟩) t
h : ∀ (m n : ℕ), m ≤ n → ↑(fs m) m = ↑(fs n) m
n : ℕ
g : ℕ → α
hg1 : ∀ m < n, (fun n ↦ ↑(fs n) n) m = g m
hg2 : rk (g n) < rk ((fun n ↦ ↑(fs n) n) n)
m : ℕ
mn : m < n
⊢ ↑(fs m) m = (fun n ↦ ↑(fs n) n) m
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
⊢ (∃ f, IsBadSeq r s f ∧ ∀ (n : ℕ), IsMinBadSeq r rk s n f) → ∃ x, IsBadSeq r s x

Tactic:
rintro ⟨f, hf1, -⟩

Goal state after:
case mpr
α : Type u_2
r : α → α → Prop
rk : α → ℕ
s : Set α
f : ℕ → α
hf1 : IsBadSeq r s f
⊢ ∃ x, IsBadSeq r s x
Module: Mathlib.GroupTheory.Subgroup.Center

Goal state before:
pp: case refine_1
G : Type u_2
inst✝ : Group G
g : G
hg : g ∈ ↑(Subgroup.center G)
⊢ ConjClasses.mk g ∈ (noncenter G)ᶜ

Tactic:
simp only [mem_noncenter, Set.compl_def, Set.mem_ofPred, Set.not_nontrivial_iff]
    intro x hx y hy
    simp only [mem_carrier_iff_mk_eq, mk_eq_mk_iff_isConj] at hx hy
    rw [hx.eq_of_right_mem_center hg, hy.eq_of_right_mem_center hg]

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ closure s), p y hy → p (x⁻¹ * y) ⋯
x : G
⊢ ∀ (h : x ∈ closure s), p x h

Tactic:
← mem_toSubmonoid,

Goal state after:
G : Type u_2
inst✝ : Group G
s : Set G
p : (x : G) → x ∈ closure s → Prop
one : p 1 ⋯
x : G
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ (closure s).toSubmonoid), p y ⋯ → p (x * y) ⋯
inv_mul_cancel : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : y ∈ (closure s).toSubmonoid), p y ⋯ → p (x⁻¹ * y) ⋯
⊢ ∀ (h : x ∈ (closure s).toSubmonoid), p x ⋯
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
⊢ (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x

Tactic:
by
  have := Classical.decEq ι
  rw [← prod_union (disjoint_filter_filter_not s s p), filter_union_filter_not_eq]

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 → x ∉ {x ∈ s | p x} → f x = 1

Tactic:
not_imp_comm,

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 ∈ {x ∈ s | p x}
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Function.Injective f
⊢ Function.Injective ⇑(map f)

Tactic:
by
  by_cases! h : IsEmpty α
  · exact Function.injective_of_subsingleton _
  · rw [Function.injective_iff_hasLeftInverse]
    use map (Function.invFun f)
    simp [Function.LeftInverse, map.comp, Function.invFun_comp hf]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_5
inst✝¹ : Finite ι
G : ι → Type u_6
inst✝ : (i : ι) → Group (G i)
P : (i : ι) → Subgroup (G i)
hP : ∀ (i : ι), (P i).FG
⊢ (Subgroup.pi Set.univ P).FG

Tactic:
simp_rw [fg_iff_submonoid_fg] at *
  exact .pi hP

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

Goal state before:
pp: ι : Type u_1
G : Type u_3
s₁ s₂ : Finset ι
inst✝¹ : CommGroup G
inst✝ : DecidableEq ι
f : ι → G
h : s₁ ⊆ s₂
⊢ ∏ x ∈ s₂ \ s₁, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
by
  rw [eq_div_iff_mul_eq', prod_sdiff h]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ Prod.mk p <$> y₁ + Prod.mk p <$> y₂ = ((fun b a ↦ (a, b)) <$> y₁ <*> pure p) + ((fun b a ↦ (a, b)) <$> y₂ <*> pure p)

Tactic:
ih1,

Goal state after:
case pure.add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
p : α✝
y₁ y₂ : FreeAbelianGroup β✝
ih1 : Prod.mk p <$> y₁ = (fun b a ↦ (a, b)) <$> y₁ <*> pure p
ih2 : Prod.mk p <$> y₂ = (fun b a ↦ (a, b)) <$> y₂ <*> pure p
⊢ ((fun b a ↦ (a, b)) <$> y₁ <*> pure p) + Prod.mk p <$> y₂ =
    ((fun b a ↦ (a, b)) <$> y₁ <*> pure p) + ((fun b a ↦ (a, b)) <$> y₂ <*> pure p)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ (Prod.mk <$> x₁ <*> y) + (Prod.mk <$> x₂ <*> y) =
    ((fun b a ↦ (a, b)) <$> y <*> x₁) + ((fun b a ↦ (a, b)) <$> y <*> x₂)

Tactic:
ih1,

Goal state after:
case add
α : Type u
G : Type u_1
β α✝ β✝ : Type u
y : FreeAbelianGroup β✝
x₁ x₂ : FreeAbelianGroup α✝
ih1 : Prod.mk <$> x₁ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₁
ih2 : Prod.mk <$> x₂ <*> y = (fun b a ↦ (a, b)) <$> y <*> x₂
⊢ ((fun b a ↦ (a, b)) <$> y <*> x₁) + (Prod.mk <$> x₂ <*> y) =
    ((fun b a ↦ (a, b)) <$> y <*> x₁) + ((fun b a ↦ (a, b)) <$> y <*> x₂)
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Semigroup α
x : FreeAbelianGroup α
L3 : α
y₁ y₂ : FreeAbelianGroup α
ih₁ : x * y₁ * of L3 = x * (y₁ * of L3)
ih₂ : x * y₂ * of L3 = x * (y₂ * of L3)
⊢ x * (y₁ + y₂) * of L3 = x * ((y₁ + y₂) * of L3)

Tactic:
| add y₁ y₂ ih₁ ih₂ =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ (lift fun x₂ ↦ of (1 * x₂)) x1 + (lift fun x₂ ↦ of (1 * x₂)) x2 = x1 + x2

Tactic:
ih1,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ x1 + (lift fun x₂ ↦ of (1 * x₂)) x2 = x1 + x2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₂ ↦ of (1 * x₂)) x1 = x1
ih2 : (lift fun x₂ ↦ of (1 * x₂)) x2 = x2
⊢ (lift fun x₂ ↦ of (1 * x₂)) (x1 + x2) = x1 + x2

Tactic:
| add x1 x2 ih1 ih2 =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ (lift fun x₁ ↦ of (x₁ * 1)) x1 + (lift fun x₁ ↦ of (x₁ * 1)) x2 = x1 + x2

Tactic:
ih1,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ x1 + (lift fun x₁ ↦ of (x₁ * 1)) x2 = x1 + x2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
x1 x2 : FreeAbelianGroup α
ih1 : (lift fun x₁ ↦ of (x₁ * 1)) x1 = x1
ih2 : (lift fun x₁ ↦ of (x₁ * 1)) x2 = x2
⊢ (lift fun x₁ ↦ of (x₁ * 1)) (x1 + x2) = x1 + x2

Tactic:
| add x1 x2 ih1 ih2 =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
L2 : α
x1 x2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x1 * of L2) = (lift ⇑f) x1 * (lift ⇑f) (of L2)
ih2 : (lift ⇑f) (x2 * of L2) = (lift ⇑f) x2 * (lift ⇑f) (of L2)
⊢ (lift ⇑f) ((x1 + x2) * of L2) = (lift ⇑f) (x1 + x2) * (lift ⇑f) (of L2)

Tactic:
| add x1 x2 ih1 ih2 =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) (x * y1) + (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y1 + (lift ⇑f) x * (lift ⇑f) y2

Tactic:
ih1,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
R : Type u_2
inst✝¹ : Monoid α
inst✝ : Ring R
f : α →* R
x y1 y2 : FreeAbelianGroup α
ih1 : (lift ⇑f) (x * y1) = (lift ⇑f) x * (lift ⇑f) y1
ih2 : (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y2
⊢ (lift ⇑f) x * (lift ⇑f) y1 + (lift ⇑f) (x * y2) = (lift ⇑f) x * (lift ⇑f) y1 + (lift ⇑f) x * (lift ⇑f) y2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ of s * y1 + of s * y2 = y1 * of s + y2 * of s

Tactic:
ih1,

Goal state after:
case of.add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
s : α
y1 y2 : FreeAbelianGroup α
ih1 : of s * y1 = y1 * of s
ih2 : of s * y2 = y2 * of s
⊢ y1 * of s + of s * y2 = y1 * of s + y2 * of s
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ x1 * y + x2 * y = y * x1 + y * x2

Tactic:
ih1,

Goal state after:
case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ y * x1 + x2 * y = y * x1 + y * x2
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: case add
α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : CommMonoid α
y x1 x2 : FreeAbelianGroup α
ih1 : x1 * y = y * x1
ih2 : x2 * y = y * x2
⊢ (x1 + x2) * y = y * (x1 + x2)

Tactic:
| add x1 x2 ih1 ih2 =>

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ (lift fun x ↦ 1) ((fun n ↦ n • of default) n) = n

Tactic:
by
    rw [map_zsmul, lift_apply_of]
    exact zsmul_one n

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
P : Type u_3
inst✝ : CommMonoid P
a b c : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑c.2 * b.1) = ↑t₂ * (↑b.2 * c.1)
⊢ ↑t₂ * ↑t₁ * ↑b.2 * (↑c.2 * a.1) = ↑t₂ * ↑c.2 * (↑t₁ * (↑b.2 * a.1))

Tactic:
by ac_rfl

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
P : Type u_3
inst✝ : CommMonoid P
a b c d : M × ↥S
t₁ : ↥S
ht₁ : ↑t₁ * (↑b.2 * a.1) = ↑t₁ * (↑a.2 * b.1)
t₂ : ↥S
ht₂ : ↑t₂ * (↑d.2 * c.1) = ↑t₂ * (↑c.2 * d.1)
⊢ ↑t₂ * ↑t₁ * (↑b.2 * ↑d.2 * (a.1 * c.1)) = ↑t₂ * (↑d.2 * c.1) * (↑t₁ * (↑b.2 * a.1))

Tactic:
by ac_rfl

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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
z : N
⊢ (f.map hy k) z * k (g ↑(f.sec z).2) = k (g (f.sec z).1)

Tactic:
f.map_mul_right

Goal state after:
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
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
z : N
⊢ k (g (f.sec z).1) = k (g (f.sec z).1)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : NonUnitalNonAssocSemiring α
inst✝¹ : PartialOrder α
inst✝ : CanonicallyOrderedAdd α
c a b : WithTop α
⊢ c * (a + b) = c * a + c * b

Tactic:
by
    cases c with
    | top => by_cases ha : a = 0 <;> simp [ha]
    | coe c =>
      by_cases hc : c = 0; · simp [hc]
      simp only [coe_mul_eq_bind hc]
      cases a <;> cases b <;> try rfl
      exact congr_arg some (mul_add _ _ _)

Goal state after:
Module: Mathlib.Order.Iterate

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

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

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

Goal state before:
pp: α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x✝ : 1 ≠ 0
⊢ StrictMono fun a ↦ a ^ 1

Tactic:
simpa only [pow_one] using! strictMono_id

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

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

Tactic:
exact absurd h bot_le.not_gt

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

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

Tactic:
exact absurd h bot_le.not_gt

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
h : IsSuccPrelimit a
⊢ NoMaxOrder ↑(Iio a)

Tactic:
refine ⟨fun ⟨b, hb⟩ ↦ ?_⟩

Goal state after:
α : Type u_1
a : α
inst✝ : Preorder α
h : IsSuccPrelimit a
x✝ : ↑(Iio a)
b : α
hb : b ∈ Iio a
⊢ ∃ b_1, ⟨b, hb⟩ < b_1
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
⊢ b = a ∨ b = succ a → a ≤ b ∧ b ≤ succ a

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
b : α
⊢ b ≤ b ∧ b ≤ succ b

case inr
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a : α
⊢ a ≤ succ a ∧ succ a ≤ succ a
Module: Mathlib.Logic.Small.Basic

Goal state before:
pp: case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β

Tactic:
refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)

Goal state after:
case pos
α : Type v
β : Type w
γ : Type v'
inst✝ : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ a, f a = g b
hβ : Nonempty β
b : β
⊢ ∃ a, (Function.invFun g ∘ f) a = b