mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Subgroup.Basic

Goal state before:
pp: G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv (f x) * x⁻¹ ∈ f.ker

Tactic:
rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]

Goal state after:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst✝² : Group G₁
inst✝¹ : Group G₂
inst✝ : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv ⇑f
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f (f_inv (f x)) = f x
Module: Mathlib.Algebra.Order.BigOperators.Group.List

Goal state before:
pp: α : Type u_5
β : Type u_6
inst✝³ : Monoid α
inst✝² : CommMonoid β
inst✝¹ : Preorder β
inst✝ : IsOrderedMonoid β
f : α → β
p : α → Prop
h_one : f 1 ≤ 1
hp_one : p 1
h_mul : ∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b
hp_mul : ∀ (a b : α), p a → p b → p (a * b)
l : List α
hpl : ∀ (a : α), a ∈ l → p a
⊢ f l.prod ≤ (map f l).prod

Tactic:
by
  induction l with
  | nil => simp [h_one]
  | cons a s ih =>
    have hpla : ∀ x, x ∈ s → p x := fun x hx => hpl x (mem_cons_of_mem _ hx)
    have hp_prod : p s.prod := prod_induction p hp_mul hp_one hpla
    grw [prod_cons, map_cons, prod_cons, h_mul a s.prod (hpl _ mem_cons_self) hp_prod, ih hpla]

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: case right
ι : Type u_1
α : ι → Type u_2
r₁ r₂ : ι → ι → Prop
s₁ s₂ : (i : ι) → α i → α i → Prop
hr : ∀ (a b : ι), r₁ a b → r₂ a b
hs : ∀ (i : ι) (a b : α i), s₁ i a b → s₂ i a b
i✝ : ι
a b : α i✝
hab : s₁ i✝ a b
⊢ Lex r₂ s₂ ⟨i✝, a⟩ ⟨i✝, b⟩

Tactic:
· exact Lex.right _ _ (hs _ _ _ hab)

Goal state after:
Module: Mathlib.Data.Sigma.Lex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
r r₁ r₂ : ι → ι → Prop
s s₁ s₂ : (i : ι) → α i → α i → Prop
a b : (i : ι) × α i
inst✝¹ : IsTrans ι r
inst✝ : ∀ (i : ι), IsTrans (α i) (s i)
⊢ ∀ (a b c : (i : ι) × α i), Lex r s a b → Lex r s b c → Lex r s a c

Tactic:
by
    rintro _ _ _ (⟨a, b, hij⟩ | ⟨a, b, hab⟩) (⟨_, c, hk⟩ | ⟨_, c, hc⟩)
    · exact Lex.left _ _ (_root_.trans hij hk)
    · exact Lex.left _ _ hij
    · exact Lex.left _ _ hk
    · exact Lex.right _ _ (_root_.trans hab hc)

Goal state after:
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
rcases h with (h | h)

Goal state after:
case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMinOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.Prod.Lex

Goal state before:
pp: case h.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1 ∨ x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y

Tactic:
rcases h with (h | h)

Goal state after:
case h.h.inl
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 < y.1
⊢ ∃ a, toLex x < a ∧ a < toLex y

case h.h.inr
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : NoMaxOrder β
inst✝ : DenselyOrdered β
x y : α × β
h : x.1 = y.1 ∧ x.2 < y.2
⊢ ∃ a, toLex x < a ∧ a < toLex y
Module: Mathlib.Data.List.MinMax

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
l : List α
b : WithBot α
h : ∀ (a : α), a ∈ l → ↑a ≤ b
⊢ l.maximum ≤ b

Tactic:
by
  induction l with
  | nil => simp
  | cons a l ih =>
    simp only [maximum_cons, max_le_iff]
    exact ⟨h a (by simp), ih fun a w => h a (mem_cons.mpr (Or.inr w))⟩

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

Goal state before:
pp: case coe.some
α : Type u_1
inst✝ : LinearOrder α
l : List α
d y : α
hy : y ∈ l ∧ ∀ (a : α), a ∈ l → a ≤ y
z : α
hz : l.max? = some z
⊢ (some z).getD d = y

Tactic:
| some z =>

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

Goal state before:
pp: α : Type u
l : List α
⊢ map Prod.snd l.revzip = l.reverse

Tactic:
rw [← unzip_snd, unzip_revzip]

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

Goal state before:
pp: case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ (s.erase x).max ≠ ↑x

Tactic:
rw [s0, max_empty]

Goal state after:
case neg
α : Type u_2
inst✝ : LinearOrder α
x : α
s : Finset α
s0 : s.erase x = ∅
⊢ ⊥ ≠ ↑x
Module: Mathlib.Data.Finset.Max

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
⊢ #s ≤ #t + 1

Tactic:
have f_mono : StrictMonoOn f s := by
    intro x hx y hy hxy
    rcases h x hx y hy hxy with ⟨a, hat, hxa, hay⟩
    calc
      f x ≤ a := min_le (mem_filter.2 ⟨hat, by simpa⟩)
      _ < f y :=
        (Finset.lt_inf_iff <| WithTop.coe_lt_top a).2 fun b hb =>
          WithTop.coe_lt_coe.2 <| hay.trans (by simpa using (mem_filter.1 hb).2)

Goal state after:
α : Type u_2
inst✝ : LinearOrder α
s t : Finset α
h : ∀ x ∈ s, ∀ y ∈ s, x < y → ∃ z ∈ t, x < z ∧ z < y
f : α → WithTop α := fun x ↦ {y ∈ t | x < y}.min
f_mono : StrictMonoOn f ↑s
⊢ #s ≤ #t + 1
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ Forall₂ (fun a c ↦ a = (c.1, ↑l - c.1)) l'.revzip l'.revzip

Tactic:
forall₂_same

Goal state after:
α : Type u_2
inst✝ : DecidableEq α
l : List α
l' : List (Multiset α)
H : ∀ ⦃x : Multiset α × Multiset α⦄, x ∈ l'.revzip → x.1 + x.2 = ↑l
⊢ ∀ (x : Multiset α × Multiset α), x ∈ l'.revzip → x = (x.1, ↑l - x.1)
Module: Mathlib.Data.Multiset.Powerset

Goal state before:
pp: α : Type u_1
s : Multiset α
⊢ powersetCard s.card s = {s}

Tactic:
induction s using Multiset.induction with
  | empty => simp
  | cons _ _ ih => simp [ih]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ∈ s.powerset.erase s ↔ t ⊂ s

Tactic:
mem_erase,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ t ≠ s ∧ t ∈ s.powerset ↔ t ⊂ s
Module: Mathlib.Data.Finset.Option

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

Tactic:
by
  classical rw [card_eraseNone_eq_card_erase, card_erase_of_mem h]

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
P : Type u → Sort v
of_equiv : {α β : Type u} → α ≃ β → P α → P β
h_empty : P PEmpty.{u + 1}
h_option : {α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)
α : Type u
inst✝¹ : Fintype α
inst✝ : DecidableEq α
n : ℕ
⊢ Trunc (P (ULift.{u, 0} (Fin n)))

Tactic:
induction n with

Goal state after:
Module: Mathlib.Data.Finset.Lattice.Fold

Goal state before:
pp: case refine_2
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
s : Finset α
f : α → Multiset β
b : β
this : DecidableEq α := Classical.decEq α
⊢ ∀ (a : α) (s : Finset α),
    a ∉ s →
      (count b (s.sup f) = s.sup fun a ↦ count b (f a)) →
        count b ((insert a s).sup f) = (insert a s).sup fun a ↦ count b (f a)

Tactic:
intro i s _ ih
    rw [Finset.sup_insert, sup_eq_union, count_union, Finset.sup_insert, ih]

Goal state after:
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨆ (_ : i ∈ s), f i

Tactic:
simp only [mem_range]

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, sSup ∅ ≤ f x
h : ⨆ i ∈ s, f i < a
x : ι
hx : x ∈ s
⊢ ∃ y, ⨆ (_ : y ∈ s), f y = f x
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ ⨆ i ∈ s, f i < a → ∀ x ∈ s, f x < a

pp: case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a

Tactic:
· intro h x hx
    refine h.trans_le' (le_csSup ?_ ?_)
    · classical
      refine (((hs.image f).union (finite_singleton (sSup ∅))).subset ?_).bddAbove
      intro
      simp only [ciSup_eq_ite, dite_eq_ite, mem_range, union_singleton, mem_insert_iff, mem_image,
        forall_exists_index]
      grind
    · simp only [mem_range]
      refine ⟨x, ?_⟩
      simp [hx]

Goal state after:
case mpr
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h : ∃ x ∈ s, sSup ∅ ≤ f x
⊢ (∀ x ∈ s, f x < a) → ⨆ i ∈ s, f i < a
Module: Mathlib.Order.ConditionallyCompleteLattice.Finset

Goal state before:
pp: case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ f x ∈ range fun i ↦ ⨅ (_ : i ∈ s), f i

Tactic:
simp only [mem_range]

Goal state after:
case mp.refine_2
ι : Type u_1
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
a : α
s : Set ι
f : ι → α
hs : s.Finite
h✝ : ∃ x ∈ s, f x ≤ sInf ∅
h : a < ⨅ i ∈ s, f i
x : ι
hx : x ∈ s
⊢ ∃ y, ⨅ (_ : y ∈ s), f y = f x
Module: Mathlib.Data.Set.Finite.Lattice

Goal state before:
pp: α : Type u
ι : Type v
κ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ a → α
⊢ ∀ {κ : ι → Type w} [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)

Tactic:
intro κ

Goal state after:
α : Type u
ι : Type v
κ✝ : ι → Sort w
inst✝¹ : Nonempty ((a : ι) → κ✝ a)
inst✝ : Order.Frame α
s : Set ι
hs : s.Finite
f : (a : ι) → κ✝ a → α
κ : ι → Type w
⊢ ∀ [Nonempty ((a : ι) → κ a)] (f : (a : ι) → κ a → α), ⨅ a ∈ s, ⨆ b, f a b = ⨆ g, ⨅ a ∈ s, f a (g a)
Module: Mathlib.Order.Interval.Set.WithBotTop

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
⊢ some ⁻¹' Ico ↑a ⊤ = Ici a

Tactic:
by
  simp [← Ici_inter_Iio]

Goal state after:
Module: Mathlib.Order.CompleteLattice.Finset

Goal state before:
pp: α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ i, s i = ⨆ i, s i.down

Tactic:
← Equiv.plift.surjective.iSup_comp

Goal state after:
α : Type u_2
ι' : Sort u_7
inst✝ : CompleteLattice α
s : ι' → α
⊢ ⨆ x, s (Equiv.plift x) = ⨆ i, s i.down
Module: Mathlib.Order.Cover

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), x ∈ Ioo a b ↔ x ∈ {c}
⊢ a ⋖ c ∧ c ⋖ b

Tactic:
mem_Ioo,

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h : ∀ (x : α), a < x ∧ x < b ↔ x ∈ {c}
⊢ a ⋖ c ∧ c ⋖ b
Module: Mathlib.Data.Finset.Sigma

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ s.sigma t = ∅ ↔ ∀ i ∈ s, t i = ∅

Tactic:
contrapose!; exact sigma_nonempty

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

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ ⟨i, x⟩ ∈ sigmaLift f ⟨i, a⟩ ⟨i, b⟩ ↔ x ∈ f a b

Tactic:
by
  rw [sigmaLift, dif_pos rfl, mem_map]
  refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩
  rintro ⟨x, hx, _, rfl⟩
  exact hx

Goal state after:
Module: Mathlib.Order.Minimal

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
⊢ Minimal P x ↔ Minimal Q x

Tactic:
refine ⟨fun h' ↦ ⟨?_, fun y hy hyx ↦ h'.le_of_le (hPQ hy) hyx⟩,
    fun h' ↦ ⟨hPQ h'.prop, fun y hy hyx ↦ ?_⟩⟩

Goal state after:
case refine_1
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal P x
⊢ Q x

case refine_2
α : Type u_2
P Q : α → Prop
x : α
inst✝ : PartialOrder α
hPQ : ∀ ⦃x : α⦄, Q x → P x
h : ∀ ⦃x : α⦄, P x → ∃ y, y ≤ x ∧ Q y
h' : Minimal Q x
y : α
hy : P y
hyx : y ≤ x
⊢ x ≤ y
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ∈ (Ico a b).erase a

Tactic:
mem_erase,

Goal state after:
a b x : ℕ
⊢ x ∈ Ico a.succ b ↔ x ≠ a ∧ x ∈ Ico a b
Module: Mathlib.Order.Interval.Finset.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f x ∈ Ioo (f a) (f b) ↔ a < x ∧ x < b

Tactic:
mem_Ioo,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ f a < f x ∧ f x < f b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: n a : ℕ
⊢ Set.InjOn (fun x ↦ x % a) ↑(Ico n (n + a))

Tactic:
induction n with

Goal state after:
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: case inl.inl
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m n : ℕ
hle : m ≤ n
hlt : m < n
⊢ r (f (g m)) (f (g n))

pp: case inl.inr
α : Type u_1
r : α → α → Prop
inst✝ : IsPreorder α r
h : WellQuasiOrdered r
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → r (f (g m)) (f (g n))
m : ℕ
hle : m ≤ m
⊢ r (f (g m)) (f (g m))

Tactic:
exacts [h1 m n hlt, refl_of r _]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑x ∈ Ioo ↑a ↑b ↔ a < x ∧ x < b

Tactic:
mem_Ioo,

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ ↑a < ↑x ∧ ↑x < ↑b ↔ a < x ∧ x < b
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DenselyOrdered α
a b : α
⊢ ¬a < b

Tactic:
by
  intro h
  induction hs : Finset.Icc a b using Finset.strongInduction generalizing b with | H i ih
  subst hs
  obtain ⟨c, hac, hcb⟩ := exists_between h
  refine ih _ ?_ c hac rfl
  exact Finset.Icc_ssubset_Icc_right (hac.trans hcb).le le_rfl hcb

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

Goal state before:
pp: α : Type u_1
G : Type u_2
M : Type u_3
R : Type u_4
A : Type u_5
S✝ : Type u_6
inst✝² : Monoid M
inst✝¹ : AddMonoid A
s t u : Set M
inst✝ : Group G
S : Submonoid G
⊢ 1⁻¹ ∈ ↑S

Tactic:
by rw [inv_one]; exact S.one_mem'

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

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico a b ∪ Set.Ico c d = Set.Ico (min a c) (max b d)

Tactic:
Set.Ico_union_Ico h₁ h₂

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c d : α
h₁ : min a b ≤ max c d
h₂ : min c d ≤ max a b
⊢ Set.Ico (min a c) (max b d) = Set.Ico (min a c) (max b d)
Module: Mathlib.Algebra.Group.Support

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x ↦ f x ^ n) ⊆ mulSupport f

Tactic:
induction n with

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

Goal state before:
pp: G : Type u_2
inst✝ : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ MulAut.conj h • P.subgroupOf H = (MulAut.conj ↑h • P).subgroupOf H

Tactic:
refine le_antisymm ?_ ?_
  · rintro - ⟨g, hg, rfl⟩
    exact ⟨g, hg, rfl⟩
  · rintro p ⟨g, hg, hp⟩
    exact ⟨⟨g, hP hg⟩, hg, Subtype.ext hp⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
f : Quotient r → β
x y : α
h : r x y
⊢ (ker (f ∘ Quotient.mk'')) x y

Tactic:
simp [ker_def, Quotient.sound' h]

Goal state after:
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 : ι
h : a ∈ s
h₀ : ∀ b ∈ s, b ≠ a → f b = 1
⊢ ∏ x ∈ s, f x = ∏ x ∈ {a}, f x

Tactic:
refine (prod_subset ?_ ?_).symm

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

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: M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
n : ℕ
step : ∀ k < n, s (k + 1) = s k * f k
⊢ ∏ k ∈ range n, f k = s n

Tactic:
induction n with

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG

Tactic:
AddSubgroup.fg_iff_addSubmonoid_fg,

Goal state after:
H : Type u_4
inst✝ : AddGroup H
P : AddSubgroup H
⊢ P.FG ↔ (toSubgroup P).FG
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
n : ℕ
f : ℕ → M
⊢ ∏ r ∈ range (n + 1), f (n - r) = ∏ k ∈ range (n + 1), f k

Tactic:
induction n with

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
R : Setoid ι
inst✝ : DecidableRel ⇑R
h : ∀ x ∈ s, ∏ a ∈ s with R a x, f a = 1
⊢ ∏ x ∈ s, f x = 1

Tactic:
rw [prod_partition R, ← Finset.prod_eq_one]
  intro xbar xbar_in_s
  obtain ⟨x, x_in_s, rfl⟩ := mem_image.mp xbar_in_s
  simp only [← Quotient.eq] at h
  exact h x x_in_s

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
rw [lift_apply_of, mul_one]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
rw [mul_neg, map_neg, map_neg, mul_neg, ih]

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 : M
y : ↥S
⊢ f x * ↑((IsUnit.liftRight (f.toMonoidHom.domRestrict S) ⋯) y)⁻¹ * f ↑y = f x

Tactic:
rw [mul_assoc, mul_comm _ (f y), ← mul_assoc, mul_inv_left, mul_comm]; dsimp

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
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
⊢ j = k

Tactic:
ext n

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
h : j.comp f.toMonoidHom = k.comp f.toMonoidHom
n : N
⊢ j n = k n
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s : ↥S
n : ℕ
h : Commute r ↑s
⊢ (r /ₒ s) ^ n = r ^ n /ₒ s ^ n

Tactic:
induction n with

Goal state after:
Module: Mathlib.Order.Iterate

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

Tactic:
induction n with

Goal state after:
Module: Mathlib.Order.Iterate

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

Tactic:
induction n with

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

Goal state before:
pp: case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulStrictMono α
x : α
x0 : 0 < ↑x
a✝ : α
h : ⊥ < ↑a✝
⊢ ↑x * ⊥ < ↑x * ↑a✝

Tactic:
simp_rw [mul_bot x0.ne.symm, ← coe_mul, bot_lt_coe]

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
m : α
P : (n : α) → m ≤ n → Prop
rfl : P m ⋯
succ : ∀ (n : α) (hmn : m ≤ n), P n hmn → P (Order.succ n) ⋯
n : ℕ
hmn : m ≤ Order.succ^[n] m
⊢ P (Order.succ^[n] m) hmn

Tactic:
induction n with

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⟩ ↦ ?_⟩
  obtain ⟨c, hbc, hca⟩ := (not_covBy_iff hb).1 (h b)
  exact ⟨⟨c, hca⟩, hbc⟩

Goal state after:
Module: Mathlib.Data.Nat.SuccPred

Goal state before:
pp: case succ
m n n✝ : ℕ
ha : n✝ + 1 ≤ (n✝ + 1).pred
⊢ IsMin (n✝ + 1)

Tactic:
exact (not_succ_le_self _ ha).elim

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddMonoidWithOne α
inst✝ : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + ↑n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
x : α
n : ℕ
⊢ pred^[n] x = x - ↑n

Tactic:
induction n with

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - (↑n + 1)

Tactic:
← sub_sub

Goal state after:
α : Type u_1
x y : α
inst✝² : PartialOrder α
inst✝¹ : AddCommGroupWithOne α
inst✝ : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - ↑n - 1
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: α : 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] a ∈ s
⊢ f a ≤ f (succ^[n] a)

Tactic:
induction n with

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

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

Tactic:
induction n with

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

Goal state before:
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 : ¬IsMax a
⊢ f a < f (succ^[n + 1] a)

Tactic:
induction n with

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

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

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

Goal state after:
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
b : α
hb : b ∈ s
n : ℕ
ha : pred^[n] b ∈ s
⊢ f (pred^[n] b) ≤ f b

Tactic:
induction n with

Goal state after: