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

Goal state before:
pp: case pos
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

pp: case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f

Tactic:
· rw [← ciSup_subtype bdd le]

Goal state after:
case neg
α : Type u_1
ι : Sort u_4
inst✝ : ConditionallyCompleteLinearOrder α
p : ι → Prop
f : Subtype p → α
hp : ¬∀ (i : ι), p i
le : sSup ∅ ≤ iSup f
bdd : ¬BddAbove (range f)
⊢ ⨆ i, ⨆ (h : p i), f ⟨i, h⟩ = iSup f
Module: Mathlib.Order.ConditionallyCompleteLattice.Indexed

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (⨆ i, f i) = ⨆ i, l (f i)

Tactic:
iSup,

Goal state after:
α : Type u_1
β : Type u_2
ι : Sort u_4
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : ConditionallyCompleteLattice β
inst✝ : Nonempty ι
l : α → β
u : β → α
gc : GaloisConnection l u
f : ι → α
hf : BddAbove (range f)
⊢ l (sSup (range fun i ↦ f i)) = ⨆ i, l (f i)
Module: Mathlib.Order.Interval.Multiset

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ ∅.val = 0

Tactic:
Finset.empty_val

Goal state after:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a : α
⊢ 0 = 0
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: a : ℕ
h : 0 < a
⊢ Ico (a - 1) a = {a - 1}

Tactic:
ext x
  rw [mem_Ico, mem_singleton]
  lia

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

Goal state before:
pp: α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ ↑(Ico a b₂)

Tactic:
coe_Ico

Goal state after:
α : Type u_2
a b₁ b₂ : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
h : b₁ < b₂
⊢ Set.Icc a b₁ ⊆ Set.Ico a b₂
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ ↑(Ico a b)

Tactic:
coe_Ico

Goal state after:
α : Type u_2
a b : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
⊢ Set.Ioo a b ⊆ Set.Ico a b
Module: Mathlib.Order.WellQuasiOrder

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun x1 x2 ↦ x1 ≤ x2) s → s.Finite

Tactic:
refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
    fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩
  obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f
  · exfalso
    apply RelEmbedding.not_wellFounded _ hwf.wf
    exact (RelEmbedding.ofMonotone _ h1).swap
  · contrapose! hc
    refine ⟨Set.range (f ∘ g), ?_, ?_⟩
    · rintro _ ⟨m, rfl⟩ _ ⟨n, rfl⟩ _ hf
      obtain h | rfl | h := lt_trichotomy m n
      · exact hc _ _ (g.strictMono h) hf
      · contradiction
      · exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))
    · refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_
      obtain h | rfl | h := lt_trichotomy m n <;>
        (first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl)

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

Goal state before:
pp: case mul
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ ∃ n, r ^ n • (x * y) ∈ closure (r • s)

Tactic:
use ny + nx

Goal state after:
case h
M : Type u_3
inst✝³ : Monoid M
N : Type u_7
inst✝² : CommMonoid N
inst✝¹ : MulAction M N
inst✝ : IsScalarTower M N N
r : M
s : Set N
x✝ x y : N
hx✝¹ : x ∈ closure s
hy✝¹ : y ∈ closure s
hx✝ : ∃ n, r ^ n • x ∈ closure (r • s)
hy✝ : ∃ n, r ^ n • y ∈ closure (r • s)
nx : ℕ
hx : r ^ nx • x ∈ closure (r • s)
ny : ℕ
hy : r ^ ny • y ∈ closure (r • s)
⊢ r ^ (ny + nx) • (x * y) ∈ closure (r • s)
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ ↑(Ico b c)

Tactic:
coe_Ico

Goal state after:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Set.Ico a c ⊆ Set.Ico a b ∪ Set.Ico b c
Module: Mathlib.GroupTheory.GroupAction.Defs

Goal state before:
pp: M : Type u_1
α : Type u_3
inst✝¹ : Monoid M
inst✝ : MulAction M α
S : Submonoid M
a : α
⊢ orbit (↥S) a ⊆ orbit M a

Tactic:
by
  rintro b ⟨g, rfl⟩
  exact mem_orbit _ _

Goal state after:
Module: Mathlib.Order.WellFoundedSet

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ (insert a s).IsPWO ↔ s.IsPWO

Tactic:
by
  simp only [← singleton_union, isPWO_union, isPWO_singleton, true_and]

Goal state after:
Module: Mathlib.GroupTheory.Subsemigroup.Center

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
z : G
⊢ z ∈ center G ↔ ∀ (g : G), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

Goal state after:
Module: Mathlib.GroupTheory.Submonoid.Center

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
z : M
⊢ z ∈ center M ↔ ∀ (g : M), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

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

Goal state before:
pp: α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ (⨆ i, H i).Normal

Tactic:
← normalizer_eq_top_iff,

Goal state after:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst✝² : Group G
inst✝¹ : AddGroup A
s : Set G
ι : Sort u_5
H : ι → Subgroup G
inst✝ : ∀ (i : ι), (H i).Normal
⊢ normalizer ↑(⨆ i, H i) = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Defs

Goal state before:
pp: ι : Type u_1
M : Type u_3
N : Type u_4
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
r : M → N → Prop
f : ι → M
g : ι → N
s : Finset ι
h₁ : r 1 1
h₂ : ∀ (a : ι) (b : M) (c : N), r b c → r (f a * b) (g a * c)
⊢ r (Multiset.map (fun x ↦ f x) s.val).prod (Multiset.map (fun x ↦ g x) s.val).prod

Tactic:
apply Multiset.prod_hom_rel <;> assumption

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

Goal state before:
pp: B : Type u_3
S : B
M : Type u_4
inst✝² : CommMonoid M
inst✝¹ : SetLike B M
inst✝ : SubmonoidClass B M
m : Multiset M
hm : ∀ a ∈ m, a ∈ S
⊢ m.prod ∈ S

Tactic:
lift m to Multiset S using hm
  rw [← coe_multiset_prod]
  exact m.prod.coe_prop

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

Goal state before:
pp: case mul
M : Type u_1
inst✝ : CommMonoid M
x✝ : M
s : Set M
x y : M
hx✝ : x ∈ closure s
hy✝ : y ∈ closure s
hx : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x
hy : ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = y
⊢ ∃ f t, ↑t ⊆ s ∧ Function.support f ⊆ ↑t ∧ ∏ a ∈ t, a ^ f a = x * y

Tactic:
obtain ⟨f, t, hts, hf, rfl⟩ := hx
    obtain ⟨g, u, hus, hg, rfl⟩ := hy
    refine ⟨f + g, t ∪ u, mod_cast Set.union_subset hts hus,
      (Function.support_add _ _).trans <| mod_cast Set.union_subset_union hf hg, ?_⟩
    simp only [Pi.add_apply, pow_add, Finset.prod_mul_distrib]
    congr 1 <;> symm
    · refine Finset.prod_subset Finset.subset_union_left ?_
      simp +contextual [Function.support_subset_iff'.1 hf]
    · refine Finset.prod_subset Finset.subset_union_right ?_
      simp +contextual [Function.support_subset_iff'.1 hg]

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 q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = (∏ x ∈ s with p x ∧ ¬q x, f x) * ∏ x ∈ s with q x ∧ ¬p x, f x

Tactic:
classical rw [← prod_union (disjoint_filter_and_not_filter _ _), ← filter_or]

Goal state after:
ι : Type u_1
M : Type u_4
s : Finset ι
inst✝² : CommMonoid M
f : ι → M
p q : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
⊢ ∏ x ∈ s with Xor (p x) (q x), f x = ∏ x ∈ s with p x ∧ ¬q x ∨ q x ∧ ¬p x, f x
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) =
    (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ (s.toLeft.disjSum s.toRight).toRight, f (Sum.inr x)

Tactic:
Finset.toRight_disjSum

Goal state after:
ι : Type u_1
κ : Type u_2
M : Type u_4
inst✝ : CommMonoid M
s : Finset (ι ⊕ κ)
f : ι ⊕ κ → M
⊢ (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x) =
    (∏ x ∈ s.toLeft, f (Sum.inl x)) * ∏ x ∈ s.toRight, f (Sum.inr x)
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Group β
f : α → β
⊢ (lift f).range = Subgroup.closure (Set.range f)

Tactic:
by
  apply le_antisymm (range_lift_le Subgroup.subset_closure)
  rw [Subgroup.closure_le]
  rintro _ ⟨a, rfl⟩
  exact ⟨FreeGroup.of a, by simp only [lift_apply_of]⟩

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
M : Type u_1
inst✝ : Monoid M
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG M

Tactic:
rintro ⟨S, hfin : Finite S, φ, hφ⟩

Goal state after:
case refine_2
M : Type u_1
inst✝ : Monoid M
S : Set M
hfin : Finite ↑S
φ : FreeMonoid ↑S →* M
hφ : Function.Surjective ⇑φ
⊢ FG M
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case refine_2
G : Type u_3
inst✝ : Group G
⊢ (∃ S, ∃ (_ : S.Finite), ∃ φ, Function.Surjective ⇑φ) → FG G

Tactic:
rintro ⟨S, hfin : Finite S, φ, hφ⟩

Goal state after:
case refine_2
G : Type u_3
inst✝ : Group G
S : Set G
hfin : Finite ↑S
φ : FreeGroup ↑S →* G
hφ : Function.Surjective ⇑φ
⊢ FG G
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁶ : Monoid M
G : Type u_3
H : Type u_4
inst✝⁵ : Group G
inst✝⁴ : AddGroup H
inst✝³ : Monoid N
G' : Type u_5
inst✝² : Group G'
inst✝¹ : FG G
inst✝ : FG G'
⊢ (⊤.prod ⊤).FG

Tactic:
exact ‹FG G›.out.prod ‹FG G'›.out

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

Goal state before:
pp: ι : Type u_1
κ : Type u_5
inst✝³ : DecidableEq ι
inst✝² : CommMonoid κ
inst✝¹ : LT κ
inst✝ : MulLeftStrictMono κ
s : Finset ι
d : ι
hd : d ∈ s
f : ι → κ
hdf : 1 < f d
⊢ ∏ m ∈ s.erase d, f m < ∏ m ∈ s, f m

Tactic:
by
  conv in ∏ m ∈ s, f m => rw [← Finset.insert_erase hd]
  rw [Finset.prod_insert (Finset.notMem_erase d s)]
  exact lt_mul_of_one_lt_left' _ hdf

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
x : FreeAbelianGroup α
⊢ (map id) x = x

Tactic:
rw [map_id]
  rfl

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
G : Type u_6
H : Type u_7
inst✝³ : Group G
inst✝² : PartialOrder G
inst✝¹ : Group H
inst✝ : PartialOrder H
e : G ≃*o H
a b : WithZero G
⊢ (MulEquiv.withZero e.toMulEquiv).toFun a ≤ (MulEquiv.withZero e.toMulEquiv).toFun b ↔ a ≤ b

Tactic:
by cases a <;> cases b <;> simp

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

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

Tactic:
intro H x y

Goal state after:
case mp
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
⊢ f x = f y ↔ g x = g y
Module: Mathlib.Order.Iterate

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

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

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 [*, iterate_pos_lt_of_map_lt]

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

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
Module: Mathlib.Algebra.Order.Ring.WithTop

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

Tactic:
rw [mul_bot x0.ne.symm, ← coe_mul] at h

Goal state after:
case coe.bot
α : Type u_1
inst✝³ : DecidableEq α
inst✝² : MulZeroClass α
inst✝¹ : Preorder α
inst✝ : PosMulReflectLE α
x : α
x0 : 0 < ↑x
a✝ : α
h : ↑(x * a✝) ≤ ⊥
⊢ ↑a✝ ≤ ⊥
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Icc (succ a) b = Ioc a b

Tactic:
by
  rw [← Ici_inter_Iic, Ici_succ_of_not_isMax ha, Ioi_inter_Iic]

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

Goal state before:
pp: ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
i j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
h : i ≠ j
⊢ (insert j s).piecewise f g i = s.piecewise f g i

Tactic:
by simp [piecewise, h]

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 α
f : α → β
hf : ∀ (a : α), ¬IsMin a → f a ≤ f (pred a)
⊢ Antitone f

Tactic:
by
  simpa using antitoneOn_of_le_pred Set.ordConnected_univ (by simpa using hf)

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

Goal state before:
pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑(n + 1) ≤ a✝ ↔ ↑n < ↑a✝

Tactic:
natCast_add,

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑n + ↑1 ≤ a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Algebra.BigOperators.Option

Goal state before:
pp: α : Type u_1
M : Type u_2
inst✝ : CommMonoid M
f : α → M
s : Finset (Option α)
⊢ ∏ x ∈ eraseNone s, f x = ∏ x ∈ s, Option.elim' 1 f x

Tactic:
calc
      ∏ x ∈ eraseNone s, f x = ∏ x ∈ (eraseNone s).map Embedding.some, Option.elim' 1 f x :=
        (prod_map (eraseNone s) Embedding.some <| Option.elim' 1 f).symm
      _ = ∏ x ∈ s.erase none, Option.elim' 1 f x := by rw [map_some_eraseNone]
      _ = ∏ x ∈ s, Option.elim' 1 f x := prod_erase _ rfl

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

Goal state before:
pp: case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ¬∃ i ∈ s, p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1

Tactic:
push Not at h

Goal state after:
case neg
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝ : DecidablePred p
h✝ : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j
a : M
h : ∀ i ∈ s, ¬p i
⊢ (∏ i ∈ s, if p i then a else 1) = 1
Module: Mathlib.Data.Fintype.Powerset

Goal state before:
pp: α : Type u_1
inst✝ : Finite α
⊢ Finite (Set α)

Tactic:
by
  cases nonempty_fintype α
  infer_instance

Goal state after:
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
f g : α → α
x : α
hf : f x = x
hg : g x = x
⊢ (f ∘ g) x = x

Tactic:
rw [comp_apply, hg, hf]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
h : ¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b
b : β
⊢ ∃ a, f a = b

Tactic:
push Not at h

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
⊢ ∃ a, f a = b
Module: Mathlib.Order.UpperLower.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsUpperSet s
⊢ s = ∅ ∨ ∃ a, s = Ici a

Tactic:
refine or_iff_not_imp_left.2 fun ha ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : LinearOrder α
s : Set α
inst✝ : WellFoundedLT α
h : IsUpperSet s
ha : ¬s = ∅
⊢ ∃ a, s = Ici a
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mp
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ωSup c ≤ x
i✝ : ℕ
⊢ c i✝ ≤ x

pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x

Tactic:
· trans ωSup c
    · exact le_ωSup _ _
    · assumption

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
x : α
a✝ : ∀ (i : ℕ), c i ≤ x
⊢ ωSup c ≤ x
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
⊢ IsAdmissible x f {y | IsExtremePt x f y}

Tactic:
exact setOfPred_isExtremePt_isAdmissible le_map

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

Goal state before:
pp: case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat

pp: case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
· lift x to ℕ using hlt
    exact mem_range_self (x : ℕ∞)

Goal state after:
case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
· rintro ⟨h⟩
    exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
· rintro ⟨h⟩
    exact ⟨by simp only [← κ.comp_eq, ← h, ← κ'.comp_eq, MonoidHom.comp_assoc]⟩

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

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (iSup f) = ⨆ i, lift.{u, w} (f i)

Tactic:
iSup,

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (sSup (range f)) = ⨆ i, lift.{u, w} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (sSup (range f)) = ⨆ i, lift.{u, w} (f i)

Tactic:
iSup,

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ lift.{u, w} (sSup (range f)) = sSup (range fun i ↦ lift.{u, w} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ 1 ↔ c = 0 ∨ c = 1

Tactic:
by
  simpa using le_succ_bot_iff (a := c)

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

Goal state before:
pp: case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
rw [eq_div_iff_mul_eq this, smul_mul_smul_comm]

Goal state after:
case neg
G : Type u_1
G₀ : Type u_2
inst✝⁴ : Group G
inst✝³ : GroupWithZero G₀
inst✝² : MulAction G G₀
inst✝¹ : IsScalarTower G G₀ G₀
inst✝ : SMulCommClass G G₀ G₀
g h : G
a b : G₀
this✝ : ∀ (x : G), x • 0 = 0
hb : ¬b = 0
this : h • b ≠ 0
⊢ (g / h * h) • (a / b * b) = g • a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
· exact proof_irrel_heq ..

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

Goal state before:
pp: case e_4.e_4
M : Type u_1
N : Type u_2
α : Type u_3
β : Type u_4
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : AddMonoid α
fst✝ : DistribMulAction M α
x : DistribMulAction N α
snd✝ : SMulCommClass M N α
⊢ ⋯ ≍ snd✝

Tactic:
· exact proof_irrel_heq ..

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
h : ∀ (x y : ↥p), x = y
x : M
hx : x ∈ p
⊢ x = 0

Tactic:
simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩

Goal state after:
Module: Mathlib.Algebra.Module.Submodule.Lattice

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
⊢ Subsingleton ↥p ↔ p = ⊥

Tactic:
by
  rw [subsingleton_iff, Submodule.eq_bot_iff]
  refine ⟨fun h x hx ↦ by simpa using h ⟨x, hx⟩ ⟨0, p.zero_mem⟩,
    fun h ⟨x, hx⟩ ⟨y, hy⟩ ↦ by simp [h x hx, h y hy]⟩

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Membership

Goal state before:
pp: M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ x ∈ ⨆ x, S ↑x ↔ ∃ i, p i ∧ x ∈ S i

Tactic:
mem_iSup_of_directed

Goal state after:
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ (∃ i, x ∈ S ↑i) ↔ ∃ i, p i ∧ x ∈ S i

case hS
M : Type u_2
inst✝ : Mul M
ι : Type u_3
p : ι → Prop
S : ι → Subsemigroup M
hS : DirectedOn ((fun x1 x2 ↦ x1 ≤ x2) on S) {i | p i}
x : M
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun x ↦ S ↑x
Module: Mathlib.Algebra.Ring.Submonoid.Basic

Goal state before:
pp: M : Type u_1
R : Type u_2
inst✝² : NonUnitalNonAssocSemiring R
inst✝¹ : SetLike M R
inst✝ : MulMemClass M R
S : M
a b : R
ha : a ∈ closure ↑S
hb : b ∈ closure ↑S
⊢ a * b ∈ closure ↑S

Tactic:
induction hb using closure_induction with
  | mem r hr => exact MulMemClass.mul_right_mem_add_closure ha hr
  | zero => simp only [mul_zero, zero_mem _]
  | add r s _ _ hr hs => simpa only [mul_add] using add_mem hr hs

Goal state after:
Module: Mathlib.Algebra.Group.Subsemigroup.Operations

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : Mul M
inst✝ : Mul N
s : Subsemigroup M
t : Subsemigroup N
u : Subsemigroup (M × N)
⊢ u ≤ s.prod t ↔ map (fst M N) u ≤ s ∧ map (snd M N) u ≤ t

Tactic:
by
  constructor
  · intro h
    constructor
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).1
    · rintro x ⟨⟨y1, y2⟩, ⟨hy1, rfl⟩⟩
      exact (h hy1).2
  · rintro ⟨hH, hK⟩ ⟨x1, x2⟩ h
    exact ⟨hH ⟨_, h, rfl⟩, hK ⟨_, h, rfl⟩⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : NonUnitalSemiring R
z : R
⊢ z ∈ center R ↔ ∀ (g : R), g * z = z * g

Tactic:
rw [← Semigroup.mem_center_iff]
  exact Iff.rfl

Goal state after: