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

Goal state before:
pp: α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Q x ∧ Minimal P x ↔ Minimal (fun x ↦ Q x ∧ P x) x

Tactic:
and_comm,

Goal state after:
α : Type u_2
P Q : α → Prop
x : α
inst✝ : LE α
hPQ : ∀ ⦃x : α⦄, P x → Q x
⊢ Q x ∧ Minimal P x ↔ Minimal (fun x ↦ P x ∧ Q x) x
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 ⋯
⊢ f = g

Tactic:
let eg := (g.strictMono.strictMonoOn .univ).orderIso

Goal state after:
α : 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 ⋯
⊢ f = g
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: b : ℕ
⊢ #(Iio b) = b

Tactic:
by rw [Iio_eq_Ico, card_Ico, Nat.bot_eq_zero, Nat.sub_zero]

Goal state after:
Module: Mathlib.Order.OrderIsoNat

Goal state before:
pp: case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : ¬Infinite ↑bad
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))

Tactic:
rw [Set.infinite_coe_iff, Set.Infinite, not_not] at hbad

Goal state after:
case neg
α : Type u_1
r : α → α → Prop
f : ℕ → α
bad : Set ℕ := {m | ∀ (n : ℕ), m < n → ¬r (f m) (f n)}
hbad : bad.Finite
⊢ ∃ g, (∀ (n : ℕ), r (f (g n)) (f (g (n + 1)))) ∨ ∀ (m n : ℕ), m < n → ¬r (f (g m)) (f (g n))
Module: Mathlib.Order.Interval.Finset.Nat

Goal state before:
pp: case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ i + a * (n / a + 1) < n + a

Tactic:
refine lt_of_lt_of_le (Nat.add_lt_add_right hi (a * (n / a + 1))) ?_

Goal state after:
case inr.mpr.inl.refine_2
n a : ℕ
ha : a ≠ 0
i : ℕ
hia : i < a
hn : n % a + a * (n / a) = n
hi : i < n % a
⊢ n % a + a * (n / a + 1) ≤ n + a
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 ∈ Finset.subtype p (Ioc ↑a ↑b) ↔ a < x ∧ x ≤ b

Tactic:
by
    simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]

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

Goal state before:
pp: α : Type u_2
a b : α
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : LocallyFiniteOrder α
⊢ Ioo a b ⊆ Iio b

Tactic:
by
  simpa [← coe_subset] using Set.Ioo_subset_Iio_self

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

Goal state before:
pp: α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ≠ a ∧ a ≤ a✝ ↔ a ≤ a✝ ∧ a ≠ a✝

Tactic:
and_comm,

Goal state after:
α : Type u_2
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ≠ a ∧ a ≤ a✝ ↔ a ≠ a✝ ∧ a ≤ a✝
Module: Mathlib.Order.Interval.Finset.Basic

Goal state before:
pp: α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y

Tactic:
have z_card : #(Ico x z) < #(Ico x y) := card_lt_card <| ssubset_iff_of_subset
    (Ico_subset_Ico_right hz.1.2.le) |>.mpr ⟨z, mem_Ico.2 hz.1, right_notMem_Ico⟩

Goal state after:
α : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun x_1 ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
⊢ TransGen (fun x1 x2 ↦ x1 ⋖ x2) x y
Module: Mathlib.Algebra.Group.Center

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
⊢ ∅.centralizer = ⊤

Tactic:
by simp [centralizer]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.ConjAct

Goal state before:
pp: G : Type u_3
inst✝¹ : Group G
H : Subgroup G
inst✝ : H.Normal
g : G
h : ↥H
⊢ ↑((MulEquiv.symm (MulAut.conjNormal g)) h) = g⁻¹ * ↑h * g

Tactic:
by
  change _ * g⁻¹⁻¹ = _
  rw [inv_inv]
  rfl

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

Goal state before:
pp: ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ count a (map (fun x ↦ f x) s.val).sum = (map (fun x ↦ count a (f x)) s.val).sum

Tactic:
count_sum

Goal state after:
ι : Type u_1
α : Type u_6
inst✝ : DecidableEq α
s : Finset ι
a : α
f : ι → Multiset α
⊢ (map (fun b ↦ count a (f b)) s.val).sum = (map (fun x ↦ count a (f x)) s.val).sum
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: case trans.inl.inr
α : Type u_1
β : Type u_2
r : Setoid α
f : α → β
hf : ker f ≤ r
i✝¹ i✝ x✝ y✝ : β
a✝¹ : Relation.EqvGen (Relation.Map (⇑r) f f) x✝ y✝
ih1 : Relation.Map (⇑r) f f x✝ y✝
a✝ : Relation.EqvGen (Relation.Map (⇑r) f f) y✝ y✝
⊢ (Relation.Map (⇑r) f f ⊔ fun x1 x2 ↦ x1 = x2) x✝ y✝

Tactic:
· exact .inl ih1

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

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

Tactic:
replace ha := hf ha

Goal state after:
case inl
α : Type u_1
β : Type u_2
f : α → β
r : Setoid α
hf : ker f ≤ r
x y a b : α
h : r a b
hb : f b = f y
ha : r a x
⊢ r x y
Module: Mathlib.GroupTheory.Congruence.Defs

Goal state before:
pp: M : Type u_1
inst✝ : Mul M
r : M → M → Prop
s : Con M
hs : s ∈ {s | ∀ (x y : M), r x y → s x y}
x y : M
hxy : (conGen r) x y
⊢ s x y

Tactic:
apply ConGen.Rel.recOn (motive := fun x y _ => s x y) hxy
        · exact fun x y h => hs x y h
        · exact s.refl'
        · exact fun _ => s.symm'
        · exact fun _ _ => s.trans'
        · exact fun _ _ => s.mul

Goal state after:
Module: Mathlib.GroupTheory.Congruence.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : MulOneClass M
inst✝¹ : MulOneClass N
inst✝ : MulOneClass P
c : Con M
x✝ y✝ : M
f : M →* P
H : c ≤ ker f
x y : c.Quotient
m n : M
⊢ Con.liftOn (↑m * ↑n) ⇑f ⋯ = Con.liftOn ↑m ⇑f ⋯ * Con.liftOn ↑n ⇑f ⋯

Tactic:
dsimp only [← coe_mul, Con.liftOn_coe]
    rw [map_mul]

Goal state after:
Module: Mathlib.GroupTheory.QuotientGroup.Defs

Goal state before:
pp: G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ x⁻¹ * y ∈ c.subgroup ↔ c x y

Tactic:
Con.mem_subgroup_iff

Goal state after:
G : Type u_1
inst✝ : Group G
c : Con G
x y : G
⊢ c (x⁻¹ * y) 1 ↔ c x y
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
exact AddSubmonoid.fg_iff_mul_fg (AddSubgroup.toAddSubmonoid P)

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

Goal state before:
pp: M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i

Tactic:
let s := { x | p x }.toFinset

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
p : ι → Prop
f : ι → M
inst✝ : DecidablePred p
s : Finset ι := {x | p x}.toFinset
⊢ (∏ i, f ↑i) * ∏ i, f ↑i = ∏ i, f i
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β : Type v
γ : Type w
inst✝ : Mul α
a : FreeAbelianGroup α
⊢ 0 * a = 0

Tactic:
by
    have h : 0 * a + 0 * a = 0 * a := by simp [← add_mul]
    simpa using h

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

Goal state before:
pp: case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z : N
⊢ ∀ ⦃a₂ : N⦄, (f.lift hg) z = (f.lift hg) a₂ → z = a₂

Tactic:
w

Goal state after:
case mpr
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type u_3
inst✝ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
hg : ∀ (y : ↥S), IsUnit (g ↑y)
H : ∀ (x y : M), f x = f y ↔ g x = g y
z w : N
⊢ (f.lift hg) z = (f.lift hg) w → z = w
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 : M →* N
h : ∀ (y : ↥S), IsUnit (f ↑y)
y : ↥S
z : N
H : f ↑y * z = 1
⊢ ↑((IsUnit.liftRight (f.domRestrict S) h) y)⁻¹ = z

Tactic:
by
  rw [← one_mul _⁻¹, Units.val_mul, mul_inv_left]
  exact H.symm

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

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

Tactic:
rw [map_mul f, map_mul f, f.mk'_eq_iff_eq_mul.1 H, ← mul_assoc, mk'_spec', mul_comm (f x₂)]

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
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ Injective fun a ↦ a ^ n

Tactic:
rintro ⟨a⟩ ⟨b⟩ (hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n)

Goal state after:
case mk.mk
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
a₁✝ : Localization S
a : M × ↥S
a₂✝ : Localization S
b : M × ↥S
hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n
⊢ Quot.mk (⇑(OreLocalization.oreEqv S M)) a = Quot.mk (⇑(OreLocalization.oreEqv S M)) b
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithTop α
ha : ¬a = 0
hb : ¬b = 0
⊢ untopD 0 (a * b) = untopD 0 a * untopD 0 b
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : IsCancelMul α
s : Submonoid α
a₁ b₁ : α
a₂ b₂ : ↥s
⊢ mk a₁ a₂ = mk b₁ b₂ ↔ ↑b₂ * a₁ = ↑a₂ * b₁

Tactic:
by
  simp_rw [mk_eq_mk_iff, r_iff_exists, mul_left_cancel_iff, exists_const]

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 α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 2) < y ^ (n + 2)

Tactic:
pow_succ _ (n + 1)

Goal state after:
α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y
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 α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ (fun a ↦ a ^ (n + 2)) x < (fun a ↦ a ^ (n + 2)) y

Tactic:
simp_rw [pow_succ _ (n + 1)]

Goal state after:
α : Type u_1
inst✝⁷ : DecidableEq α
inst✝⁶ : CommSemiring α
inst✝⁵ : PartialOrder α
inst✝⁴ : OrderBot α
inst✝³ : CanonicallyOrderedAdd α
inst✝² : PosMulStrictMono α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
n : ℕ
x✝ : n + 2 ≠ 0
x y : WithTop α
h : x < y
⊢ x ^ (n + 1) * x < y ^ (n + 1) * y
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b

case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
a b : WithBot α
ha : ¬a = 0
hb : ¬b = 0
⊢ unbotD 0 (a * b) = unbotD 0 a * unbotD 0 b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : SuccOrder α
a b : α
h₁ : a ≤ b
h₂ : ¬IsMax b
⊢ Ico a (succ b) = insert b (Ico a b)

Tactic:
by
  simp_rw [← Iio_inter_Ici, Iio_succ_eq_insert_of_not_isMax h₂, insert_inter_of_mem (mem_Ici.2 h₁)]

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁴ : PartialOrder α
inst✝³ : AddMonoidWithOne α
inst✝² : NeZero 1
inst✝¹ : SuccAddOrder α
inst✝ : IsBotZeroClass α
⊢ 1 ≤ x ↔ x ≠ 0

Tactic:
by
  rw [Order.one_le_iff_pos, pos_iff_ne_zero]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α
inst✝⁴ : Preorder β
inst✝³ : Sub α
inst✝² : One α
inst✝¹ : PredSubOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
⊢ (∀ (a : α), ¬IsMin a → a ∈ s → a - 1 ∈ s → f a ≤ f (a - 1)) → AntitoneOn f s

Tactic:
simpa [Order.pred_eq_sub_one] using antitoneOn_of_le_pred hs (f := f)

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

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
⊢ (if h : pred ↑⟨x, hx⟩ ∈ s then ⟨pred ↑⟨x, hx⟩, h⟩ else ⟨x, hx⟩) ≤ ⟨x, hx⟩

Tactic:
dsimp; split <;> simp_all [Order.pred_le]

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

Goal state before:
pp: n : ℕ
m : WithBot ℕ∞
⊢ ↑↑(n + 1) ≤ m ↔ ↑n < m

Tactic:
cases m

Goal state after:
case bot
n : ℕ
⊢ ↑↑(n + 1) ≤ ⊥ ↔ ↑n < ⊥

case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑(n + 1) ≤ ↑a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: case pos
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ ∏ x ∈ s, f x = f i * ∏ x ∈ s \ {i}, f x

Tactic:
convert! (s.prod_inter_mul_prod_sdiff { i } f).symm

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
f : ι → M
h : i ∉ s → f i = 1
hs : i ∈ s
⊢ f i = ∏ x ∈ s ∩ {i}, f x
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:
prod_eq_one

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
⊢ 1 = 1

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
⊢ ∀ x ∈ s, (if p x then a else 1) = 1
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
ι : Type u_4
inst✝² : DecidableEq ι
inst✝¹ : Fintype ι
inst✝ : CommMonoid α
s : Finset ι
f : ι → α
⊢ (∏ i, if i ∈ s then f i else 1) = ∏ i ∈ s, f i

Tactic:
rw [← prod_filter, filter_mem_eq_inter, univ_inter]

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

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ s.append (replicate (↑i) b) ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

Tactic:
mem_append_iff,

Goal state after:
α : Type u_1
n : ℕ
a b : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
⊢ a ∈ s ∨ a ∈ replicate (↑i) b ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s
Module: Mathlib.Data.Fintype.BigOperators

Goal state before:
pp: α : Type u_1
inst✝ : Fintype α
T : Finset (List α)
s : ℕ
⊢ #({x ∈ T | x.length = s}) ≤ Fintype.card α ^ s

Tactic:
by
  classical
  calc
    _ ≤ (Finset.univ.image List.ofFn).card := by
          apply Finset.card_le_card
          intro a ha
          let hlen := Finset.mem_filter.mp ha
          exact Finset.mem_image.mpr ⟨
              (fun j : Fin s => a.get ⟨j.val, by simp [hlen]⟩),
              by simp,
              List.ext_get (by simp [hlen]) (by simp)⟩
    _ = Fintype.card α ^ s := by
          simp [card_image_of_injective univ List.ofFn_injective]

Goal state after:
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: case refine_2
α : Type u
s : Set α
hs : s.Infinite
f : ℕ → ↑s
hf : Injective f
⊢ (range (Subtype.val ∘ f)).Countable

Tactic:
exact countable_range (Subtype.val ∘ f)

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

Goal state before:
pp: case cons.zero
α : Type u_1
β : Type u_2
γ : Type u_3
n : ℕ
f : α → β → γ
n✝ : ℕ
a✝ : α
b✝ : β
x✝ : Vector α n✝
y✝ : Vector β n✝
ih : ∀ (i : Fin n✝), (map₂ f x✝ y✝).get i = f (x✝.get i) (y✝.get i)
⊢ (f a✝ b✝ ::ᵥ map₂ f x✝ y✝).get 0 = f ((a✝ ::ᵥ x✝).get 0) ((b✝ ::ᵥ y✝).get 0)

Tactic:
simp only [get_zero, head_cons]

Goal state after:
Module: Mathlib.Order.Zorn

Goal state before:
pp: case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub

Tactic:
rcases ih c (fun z hz => (hcs hz).1) hc y hy with ⟨z, hzs, hz⟩

Goal state after:
case refine_1.inr
α : Type u_1
inst✝ : Preorder α
s : Set α
ih : ∀ c ⊆ s, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ s, ∀ z ∈ c, z ≤ ub
x : α
hxs : x ∈ s
c : Set α
hcs : c ⊆ {y | y ∈ s ∧ x ≤ y}
hc : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
y : α
hy : y ∈ c
z : α
hzs : z ∈ s
hz : ∀ z_1 ∈ c, z_1 ≤ z
⊢ ∃ ub ∈ {y | y ∈ s ∧ x ≤ y}, ∀ z ∈ c, z ≤ ub
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
γ : Type u_4
β : α → Type u_6
inst✝¹ : (x : α) → OmegaCompletePartialOrder (β x)
inst✝ : OmegaCompletePartialOrder γ
f : γ → (x : α) → β x
hf : ∀ (a : α), ωScottContinuous fun x ↦ f x a
c : Chain γ
⊢ f (ωSup c) = ωSup (c.map { toFun := f, monotone' := ⋯ })

Tactic:
by ext a; apply (hf a).map_ωSup c

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

Goal state before:
pp: ⊢ ∀ {a b c : Cardinal.{u_1}}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c

Tactic:
by
  rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩
  let ⟨a⟩ := mk_ne_zero_iff.1 hα
  exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩

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

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Tactic:
convert! power_le_power_left ha hb

Goal state after:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a = a ^ 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (?u.14 + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{?u.14} := Subtype.val
⊢ False

Tactic:
have hι : Nonempty ι := ⟨⟨_, h⟩⟩

Goal state after:
a : Cardinal.{u}
h : ¬Acc (fun x1 x2 ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c // ¬Acc (fun x1 x2 ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val
hι : Nonempty ι
⊢ False
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < g x

Tactic:
by rw [hx]; exact cantor _

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ σ (σ' x) = x

Tactic:
rw [← RingHom.comp_apply, comp_eq₂]
  simp

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

Goal state before:
pp: case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
· intro α hα h f
    rw [Cardinal.prod, mk_congr Equiv.piOptionEquivProd, mk_prod, lift_umax.{v, u}, mk_out, ←
        Cardinal.prod, lift_prod, Fintype.prod_option, lift_mul, ← h fun a => f (some a)]
    simp only [lift_id]

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

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{u_2}
⊢ ⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0

Tactic:
by
  simp [iInf, sInf_eq_zero_iff]

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

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : ¬a = 0
hb : ¬b = 0
⊢ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
← mk_univ,

Goal state after:
α : Type u
n : ℕ
⊢ #↑univ = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n
Module: Mathlib.Algebra.GroupWithZero.Action.Basic

Goal state before:
pp: 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
⊢ (g / h) • (a / b) = g • a / h • b

Tactic:
by_cases hb : b = 0

Goal state after:
case pos
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
⊢ (g / h) • (a / b) = g • a / h • b

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
⊢ (g / h) • (a / b) = g • a / h • b
Module: Mathlib.Algebra.Module.LinearMap.Defs

Goal state before:
pp: R : Type u_14
M : Type u_15
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
⊢ IsLinearMap R fun z ↦ c • z

Tactic:
by
  refine IsLinearMap.mk (smul_add c) ?_
  intro _ _
  simp only [smul_smul, mul_comm]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[id] Y₁
g : Y₁ → X
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : M
x : Y₁
⊢ g (f (m • g x)) = m • g x

Tactic:
by rw [h₁]

Goal state after:
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: M' : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
φ : M → N
ψ : N → P
χ : M → P
X : Type u_5
inst✝⁵ : SMul M X
inst✝⁴ : SMul M' X
Y : Type u_6
inst✝³ : SMul N Y
inst✝² : SMul M' Y
Z : Type u_7
inst✝¹ : SMul P Z
φ' : N → M
Y₁ : Type u_8
inst✝ : SMul M Y₁
f : X →ₑ[φ] Y
g : Y → X
k : Function.RightInverse φ' φ
h₁ : Function.LeftInverse g ⇑f
h₂ : Function.RightInverse g ⇑f
m : N
x : Y
⊢ g (f (φ' m • g x)) = φ' m • g x

Tactic:
by rw [h₁]

Goal state after:
Module: Mathlib.Algebra.Module.LinearMap.End

Goal state before:
pp: R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : End R M
h : Injective ⇑f'
n : ℕ
⊢ Injective ⇑(f' ^ (n + 1))

Tactic:
rw [iterate_succ]
    exact (iterate_injective h n).comp h

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

Goal state before:
pp: R : Type u
M : Type v
inst✝¹ : Ring R
inst✝ : AddCommGroup M
module_M : Module R M
p : Submodule R M
x y : M
hx : x ∈ p
⊢ x - y ∈ p ↔ y ∈ p

Tactic:
rw [sub_eq_add_neg, p.add_mem_iff_right hx, p.neg_mem_iff]

Goal state after: