mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) ((f * g) y)

Tactic:
apply Commute.mul_right

Goal state after:
case hac.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (f y)

case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (f x) (g y)
Module: Mathlib.Data.Finset.NoncommProd

Goal state before:
pp: case hbc
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) ((f * g) y)

Tactic:
apply Commute.mul_right

Goal state after:
case hbc.hab
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (f y)

case hac
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f g : α → β
comm_ff : (↑s).Pairwise (Commute on f)
comm_gg : (↑s).Pairwise (Commute on g)
comm_gf : (↑s).Pairwise fun x y ↦ Commute (g x) (f y)
x : α
hx : x ∈ ↑s
y : α
hy : y ∈ ↑s
h : x ≠ y
⊢ Commute (g x) (g y)
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 ∈ {x ∈ s | p x ∧ ¬q x} ∪ {x ∈ s | q x ∧ ¬p x}, f x

Tactic:
← 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.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
β : Type v
inst✝ : Group β
f✝ : α → β
x y : FreeGroup α
f : α → β
⊢ ∀ (a b : FreeGroup α), Quot.lift (Lift.aux f) ⋯ (a * b) = Quot.lift (Lift.aux f) ⋯ a * Quot.lift (Lift.aux f) ⋯ b

Tactic:
by
      rintro ⟨L₁⟩ ⟨L₂⟩; simp [Lift.aux, List.prod_append]

Goal state after:
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, closure ↑(Finset.image (⇑(MonoidHom.mulSingle M i)) (s i)) = Submonoid.pi Set.univ P

Tactic:
Finset.coe_image,

Goal state after:
ι : Type u_3
inst✝¹ : Finite ι
M : ι → Type u_4
inst✝ : (i : ι) → Monoid (M i)
P : (i : ι) → Submonoid (M i)
this : Fintype ι
s : (i : ι) → Finset (M i)
hs : ∀ (i : ι), closure ↑(s i) = P i
⊢ ⨆ i, closure (⇑(MonoidHom.mulSingle M i) '' ↑(s i)) = Submonoid.pi Set.univ P
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure ↑(Finset.image (⇑e) s) = Submonoid.map e (closure ↑s)

Tactic:
Finset.coe_image,

Goal state after:
M : Type u_1
inst✝¹ : Monoid M
M' : Type u_3
inst✝ : Monoid M'
e : M →* M'
s : Finset M
⊢ closure (⇑e '' ↑s) = Submonoid.map e (closure ↑s)
Module: Mathlib.GroupTheory.Finiteness

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

Tactic:
Finset.coe_image,

Goal state after:
case h
M : Type u_1
inst✝² : Monoid M
M' : Type u_3
inst✝¹ : Monoid M'
inst✝ : FG M
f : M →* M'
hf : Function.Surjective ⇑f
s : Finset M
hs : Submonoid.closure ↑s = ⊤
⊢ Submonoid.closure (⇑f '' ↑s) = ⊤
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

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

Tactic:
| succ n ih =>

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : a ∈ s
⊢ (∏ x ∈ s.erase a, f x) * f a = ∏ x ∈ s, f x

Tactic:
by rw [mul_comm, mul_prod_erase s f h]

Goal state after:
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ x + y >>= f >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
rw [add_bind] <;> try rw [ihx, ihy]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= f) + (y >>= f) >>= g = x + y >>= fun x ↦ f x >>= g

Tactic:
rw [add_bind] <;> try rw [ihx, ihy]

Goal state after:
α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
β α✝ β✝ γ✝ : Type u
x✝ : FreeAbelianGroup α✝
f : α✝ → FreeAbelianGroup β✝
g : β✝ → FreeAbelianGroup γ✝
x y : FreeAbelianGroup α✝
ihx : x >>= f >>= g = x >>= fun x ↦ f x >>= g
ihy : y >>= f >>= g = y >>= fun x ↦ f x >>= g
⊢ (x >>= fun x ↦ f x >>= g) + (y >>= fun x ↦ f x >>= g) = x + y >>= fun x ↦ f x >>= g

Tactic:
rw [add_bind] <;> try rw [ihx, ihy]

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

Goal state before:
pp: ι : Type u_1
M : Type u_4
α : Type u_5
inst✝ : CommMonoid M
m : Multiset ι
s : Finset α
f : ι → α → M
⊢ (map (fun i ↦ ∏ a ∈ s, f i a) m).prod = ∏ a ∈ s, (map (fun i ↦ f i a) m).prod

Tactic:
by
  classical
  induction s using Finset.induction with
  | empty => simp
  | insert a s ha ih => simp [Finset.prod_insert ha, prod_map_mul, ih]

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

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

Tactic:
by
  refine le_normalizer_iff.trans ⟨fun hH ↦ ?_, fun hH h hh k hk ↦ ?_⟩
  · exact commutator_le.mpr fun h hh k hk ↦ mul_mem (hH h hh k hk) (inv_mem hk)
  · exact (mul_mem_cancel_right <| inv_mem hk).mp <| hH <| commutator_mem_commutator hh hk

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

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : Preorder α
inst✝⁴ : Preorder β
inst✝³ : Preorder γ
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
g₁ g₂ : α ≃*o β
f : β ≃*o γ
hf : Injective ⇑f
h : g₁.trans f = g₂.trans f
a : α
⊢ f (g₁ a) = f (g₂ a)

Tactic:
by rw [← trans_apply, h, trans_apply]

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

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

Tactic:
| succ n ih =>

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

Goal state before:
pp: M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
⊢ Bijective ⇑f

Tactic:
refine ⟨fun g g' eq ↦ ?_, fun m ↦ ?_⟩

Goal state after:
case refine_1
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
g g' : G
eq : f g = f g'
⊢ g = g'

case refine_2
M : Type u_1
G : Type u_2
F : Type u_3
inst✝³ : CommMonoid M
inst✝² : CommGroup G
S : Submonoid G
inst✝¹ : FunLike F G M
inst✝ : MulHomClass F G M
f : F
h : S.IsLocalizationMap ⇑f
m : M
⊢ ∃ a, f a = m
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : 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 : ℕ
ih : ∀ (hmn : m ≤ Order.succ^[n] m), P (Order.succ^[n] m) hmn
hmn : m ≤ Order.succ^[n + 1] m
⊢ P (Order.succ^[n + 1] m) hmn

Tactic:
| succ n ih =>

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 ≤ n
⊢ P n hmn

Tactic:
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate
  induction n with
  | zero => exact rfl
  | succ n ih =>
    simp_rw [Function.iterate_succ_apply']
    exact succ _ (id_le_iterate_of_id_le le_succ n m) (ih _)

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

Goal state before:
pp: α : Type u_1
a : α
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
⊢ IsSuccLimit a ↔ a ≠ ⊥ ∧ IsSuccPrelimit a

Tactic:
by
  rw [isSuccLimit_iff, isMin_iff_eq_bot]

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

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩

Tactic:
have : Order.pred (⟨c, hc⟩ : s) = ⟨c, hc⟩ := by
          change dite .. = _
          simp [h]

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
s : Set α
inst✝ : s.OrdConnected
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
n : ℕ
hi : ∀ (c : α) (hc : c ∈ s), b ≤ c → pred^[n] c = b → pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
c : α
hc : c ∈ s
hbc : b ≤ c
hn : pred^[n] (pred c) = b
h : pred ↑⟨c, hc⟩ ∉ s
this : pred ⟨c, hc⟩ = ⟨c, hc⟩
⊢ pred^[n] ⟨c, hc⟩ = ⟨b, hb⟩
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
simpa using hin

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

Goal state before:
pp: case top
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
⊢ motive ⊤

pp: case coe
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
a✝ : ℕ
⊢ motive ↑a✝

Tactic:
· exact top A

Goal state after:
case coe
motive : ℕ∞ → Prop
zero : motive 0
succ : ∀ (n : ℕ), motive ↑n → motive ↑n.succ
top : (∀ (n : ℕ), motive ↑n) → motive ⊤
A : ∀ (n : ℕ), motive ↑n
a✝ : ℕ
⊢ motive ↑a✝
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
⊢ a ≤ a * c

Tactic:
obtain rfl | h0 := eq_or_ne a 0

Goal state after:
case inr.inl
c : ℕ∞
hc : c ≠ 0
hne : 0 ≠ ⊤
⊢ 0 ≤ 0 * c

case inr.inr
c a : ℕ∞
hc : c ≠ 0
hne : a ≠ ⊤
h0 : a ≠ 0
⊢ a ≤ a * c
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
C : {n : ℕ} → Vector α n → Sort u_6
nil : C Vector.nil
cons : {n : ℕ} → {x : α} → {w : Vector α n} → C w → C (x ::ᵥ w)
n : ℕ
ih : (v : Vector α n) → C v
v : Vector α (n + 1)
⊢ C v

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Sort u_8
nil : C Vector.nil Vector.nil
cons : {n : ℕ} → {a : α} → {b : β} → {x : Vector α n} → {y : Vector β n} → C x y → C (a ::ᵥ x) (b ::ᵥ y)
n : ℕ
ih : (v : Vector α n) → (w : Vector β n) → C v w
v : Vector α (n + 1)
w : Vector β (n + 1)
⊢ C v w

Tactic:
| succ n ih =>

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

Goal state before:
pp: case succ
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n✝ : ℕ
β : Type u_6
γ : Type u_7
C : {n : ℕ} → Vector α n → Vector β n → Vector γ n → Sort u_8
nil : C Vector.nil Vector.nil Vector.nil
cons :
  {n : ℕ} →
    {a : α} →
      {b : β} →
        {c : γ} → {x : Vector α n} → {y : Vector β n} → {z : Vector γ n} → C x y z → C (a ::ᵥ x) (b ::ᵥ y) (c ::ᵥ z)
n : ℕ
ih : (u : Vector α n) → (v : Vector β n) → (w : Vector γ n) → C u v w
u : Vector α (n + 1)
v : Vector β (n + 1)
w : Vector γ (n + 1)
⊢ C u v w

Tactic:
| succ n ih =>

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

Goal state before:
pp: α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
⊢ ((↑v).insertIdx j a).eraseIdx ↑(if i < j then ⟨i, ⋯⟩ else ⟨i + 1, ⋯⟩) =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(if h : i < j then ⟨j, hj⟩.pred ⋯ else ⟨j, hj⟩.castPred ⋯)) a

Tactic:
split_ifs with hij

Goal state after:
case pos
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.pred ⋯)) a

case neg
α : Type u_1
n : ℕ
a : α
v : Vector α (n + 1)
i : ℕ
hi : i < n + 1
j : ℕ
hj : j < n + 2
hij : ¬i < j
⊢ ((↑v).insertIdx j a).eraseIdx ↑⟨i + 1, ⋯⟩ =
    (↑(match v with
          | ⟨l, p⟩ => ⟨l.eraseIdx i, ⋯⟩)).insertIdx
      (↑(⟨j, hj⟩.castPred ⋯)) a
Module: Mathlib.Data.Set.Countable

Goal state before:
pp: α : Type u
β : Type v
s : Set α
hs : s.Countable
f : α → β
⊢ (f '' s).Countable

Tactic:
by
  rw [image_eq_range]
  have := hs.to_subtype
  apply countable_range

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

Goal state before:
pp: α : Type u
s : Set α
hs : s.Infinite
⊢ ∃ t ⊆ s, t.Countable ∧ t.Infinite

Tactic:
obtain ⟨f, hf⟩ := Infinite.natEmbedding s hs
  refine ⟨range (Subtype.val ∘ f), ?_, ?_, ?_⟩
  · exact fun _ ⟨y, hy⟩ ↦ hy ▸ Subtype.coe_prop (f y)
  · exact countable_range (Subtype.val ∘ f)
  · exact infinite_range_of_injective <| Injective.comp Subtype.val_injective hf

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
inst✝ : Countable β
h : ∀ (b : β), (f ⁻¹' {b}).Countable
⊢ (⋃ i, f ⁻¹' {i}).Countable

Tactic:
Set.countable_iUnion h

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

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

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

Tactic:
· exact (not_inl_lt_inr h).elim

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

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

Tactic:
· exact (not_inl_lt_inr h).elim

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

Goal state before:
pp: case succ
α : Type u_3
inst✝ : SemilatticeSup α
f : α →o α
h : ∀ (a₁ a₂ : α), f (a₁ ⊔ a₂) ≤ f a₁ ⊔ a₂
n₁ n₂ : ℕ
a₁ a₂ : α
n : ℕ
ih : ∀ (a₁ a₂ : α), (⇑f)^[n] (a₁ ⊔ a₂) ≤ (⇑f)^[n] a₁ ⊔ a₂
⊢ ∀ (a₁ a₂ : α), (⇑f)^[n + 1] (a₁ ⊔ a₂) ≤ (⇑f)^[n + 1] a₁ ⊔ a₂

Tactic:
| succ n ih =>

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁ a₂ : α
b₁ b₂ : β
ha : a₁ ≤ a₂
hb : b₁ ≤ b₂
⊢ (pair a₁ a₂ ha).zip (pair b₁ b₂ hb) = pair (a₁, b₁) (a₂, b₂) ⋯

Tactic:
by
  ext n : 2; cases n <;> rfl

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case right
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : (∀ (a_1 : ℕ), c a_1 ≤ a) ∧ ∀ ⦃a_1 : α⦄, (∀ (a : ℕ), c a ≤ a_1) → a ≤ a_1
⊢ ωSup c ≤ a

Tactic:
rw [ωSup_le_iff]
    apply h.1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ Part.ωSup c = some x

Tactic:
ωSup_eq_some

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ some ?m.26 = some x

ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ some ?m.26 ∈ c

ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
c : Chain (Part α)
i : ℕ
x : α
hx : c i = some x
⊢ α
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem.inl
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
le_map : ∀ (x : α), x ≤ f x
c : NonemptyChain α
hc : ↑c ⊆ {y | IsExtremePt x f y}
y : α
hy : y ∈ bot x f
hy' : y < cSup c
z : α
hz : z ∈ c
hzy : ¬f z ≤ y
h : y ≤ z
hyz : y < z
⊢ f y ≤ cSup c

Tactic:
exact le_trans ((hc hz).map_le_of_mem_of_lt hy hyz) (le_cSup _ _ hz)

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
β : α → Type u_6
inst✝ : (a : α) → OmegaCompletePartialOrder (β a)
x✝¹ : Chain ((a : α) → β a)
x✝ : (a : α) → β a
hf : ∀ (i : ℕ), x✝¹ i ≤ x✝
a : α
⊢ ∀ (i : ℕ), (x✝¹.map (Pi.evalOrderHom a)) i ≤ x✝ a

Tactic:
rintro i
      apply hf

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ sᶜ
y : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
y : α
hy : y ∈ sᶜ
x' : β
left✝ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
hxy : g' (g x') = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this : Surjective h
x : α
hx : x ∈ s
y : α
hy : y ∉ s
hxy : f x = g' y
⊢ y ∈ g '' (f '' s)ᶜ

Tactic:
rwa [hns]

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β✝ : Type u_3
γ✝ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β✝
inst✝¹ : OmegaCompletePartialOrder γ✝
inst✝ : OmegaCompletePartialOrder δ
β γ : Type v
f : α →𝒄 Part β
g : α →𝒄 β → Part γ
c : Chain α
⊢ ((↑f).partBind g.toOrderHom).toFun (ωSup c) = ωSup (c.map ((↑f).partBind g.toOrderHom))

Tactic:
by
    rw [ωSup_bind, ← f.continuous, g.toOrderHom_eq_coe, ← g.continuous]
    rfl

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

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n ≤ toENat c ↔ ↑n ≤ c

Tactic:
by
  rw [← toENat_nat n, toENat_le_iff_of_le_aleph0 natCast_le_aleph0]

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

Goal state before:
pp: n : ℕ
⊢ ↑n < ℵ₀

Tactic:
rw [← natCast_add_one_le_iff, ← Nat.cast_add_one, ← lift_mk_fin, aleph0, lift_mk_le.{u}]

Goal state after:
n : ℕ
⊢ Nonempty (Fin (n + 1) ↪ ℕ)
Module: Mathlib.Algebra.Module.Equiv.Defs

Goal state before:
pp: case mp
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f = g ∘ₛₗ ↑e₁₂.symm
x✝ : M₁
⊢ (f ∘ₛₗ ↑e₁₂) x✝ = g x✝

pp: case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝

Tactic:
· simp [H]

Goal state after:
case mpr
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
inst✝⁵ : Semiring R₃
inst✝⁴ : AddCommMonoid M₁
inst✝³ : AddCommMonoid M₂
inst✝² : AddCommMonoid M₃
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
module_M₃ : Module R₃ M₃
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
σ₁₃ : R₁ →+* R₃
σ₂₃ : R₂ →+* R₃
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
inst✝¹ : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂
inst✝ : RingHomCompTriple σ₂₁ σ₁₃ σ₂₃
f : M₂ →ₛₗ[σ₂₃] M₃
g : M₁ →ₛₗ[σ₁₃] M₃
H : f ∘ₛₗ ↑e₁₂ = g
x✝ : M₂
⊢ f x✝ = (g ∘ₛₗ ↑e₁₂.symm) x✝