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

Goal state before:
pp: F : Type u_1
α : Type u_3
β : Type u_4
inst✝³ : Monoid α
inst✝² : Monoid β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
s : Multiset α
comm : {x | x ∈ s}.Pairwise Commute
f : F
x : α
hx : x ∈ s
y : α
hy : y ∈ s
a✝ : f x ≠ f y
⊢ Commute (f x) (f y)

Tactic:
exact (comm.of_refl hx hy).map f

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Monoid β
s₁ s₂ : Finset α
f g : α → β
h₁ : s₁ = s₂
h₂ : ∀ x ∈ s₂, f x = g x
comm : (↑s₁).Pairwise (Commute on f)
⊢ s₁.noncommProd f comm = s₂.noncommProd g ⋯

Tactic:
simp_rw [noncommProd, Multiset.map_congr (congr_arg _ h₁) h₂]

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

Goal state before:
pp: case cons
α : Type u_6
a b : Multiset α
bs : List (Multiset α)
ih : Disjoint bs.sum a ↔ ∀ b ∈ bs, Disjoint b a
⊢ Disjoint (b :: bs).sum a ↔ ∀ b_1 ∈ b :: bs, Disjoint b_1 a

Tactic:
simp [ih]

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

Goal state before:
pp: case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ f x = g x

Tactic:
← noncommProd_mulSingle x,

Goal state after:
case intro
ι : Type u_2
γ : Type u_5
inst✝³ : Monoid γ
M : ι → Type u_6
inst✝² : (i : ι) → Monoid (M i)
inst✝¹ : Finite ι
inst✝ : DecidableEq ι
f g : ((i : ι) → M i) →* γ
h : ∀ (i : ι) (x : M i), f (Pi.mulSingle i x) = g (Pi.mulSingle i x)
val✝ : Fintype ι
x : (i : ι) → M i
⊢ f (univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯) = g (univ.noncommProd (fun i ↦ Pi.mulSingle i (x i)) ⋯)
Module: Mathlib.Data.Setoid.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : Setoid α
s : Setoid β
q : Quotient (r.prod s)
⊢ (fun x ↦
        match x with
        | (x, y) => Quotient.map₂ Prod.mk ⋯ x y)
      ((fun q ↦ q.liftOn' (fun xy ↦ (Quotient.mk'' xy.1, Quotient.mk'' xy.2)) ⋯) q) =
    q

Tactic:
induction q using Quotient.inductionOn'; rfl

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

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u_1
M : Type u_4
inst✝² : CommMonoid M
s : Finset ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : (x : ι) → Decidable ¬p x
f : ι → M
this : DecidableEq ι
⊢ (∏ x ∈ s with p x, f x) * ∏ x ∈ s with ¬p x, f x = ∏ x ∈ s, f x
Module: Mathlib.GroupTheory.FreeGroup.Basic

Goal state before:
pp: α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]

Tactic:
rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩

Goal state after:
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
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
⊢ f (m * n) = f m * f n

Tactic:
rw [map_mul]

Goal state after:
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 ι
t : Finset κ
inst✝ : DecidableEq κ
g : ι → κ
h : ∀ i ∈ s, g i ∈ t
f : κ → M
y : κ
x✝ : y ∈ t
x : ι
hx : x ∈ {i ∈ s | g i = y}
⊢ f y = f (g x)

Tactic:
rw [(mem_filter.1 hx).2]

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

Goal state before:
pp: α : Type u
L₁ L₂ : List (α × Bool)
h : Red L₁ L₂
⊢ ∃ n, L₁.length = L₂.length + 2 * n

Tactic:
by
  induction h with
  | refl => exact ⟨0, rfl⟩
  | tail _h₁₂ h₂₃ ih =>
    rcases ih with ⟨n, eq⟩
    exists 1 + n
    simp [Nat.mul_add, eq, (Step.length h₂₃).symm, add_assoc]

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
p : ι → Prop
inst✝ : DecidablePred p
f : ι → M
⊢ (∏ a ∈ s with p a, if p a then f a else 1) = ∏ a ∈ s, if p a then f a else 1

Tactic:
{ refine prod_subset (filter_subset _ s) fun x hs h => ?_
        rw [mem_filter, not_and] at h
        exact if_neg (by simpa using h hs) }

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 b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
ha : a ∈ s
hb : b ∈ s
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = f a * f b
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 b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
⊢ ∏ x ∈ s, f x = f a * f b

Tactic:
have := Classical.decEq ι

Goal state after:
ι : Type u_1
M : Type u_4
inst✝ : CommMonoid M
s : Finset ι
f : ι → M
a b : ι
hn : a ≠ b
h₀ : ∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1
ha : a ∉ s → f a = 1
hb : b ∉ s → f b = 1
this : DecidableEq ι
⊢ ∏ x ∈ s, f x = f a * f b
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)
hP : ∀ (i : ι), (P i).FG
⊢ (Submonoid.pi Set.univ P).FG

Tactic:
classical
  have := Fintype.ofFinite ι
  choose s hs using hP
  refine ⟨Finset.univ.biUnion fun i => (s i).image (MonoidHom.mulSingle M i), ?_⟩
  simp_rw [Finset.coe_biUnion, Finset.coe_univ, Set.biUnion_univ, closure_iUnion, Finset.coe_image,
    ← MonoidHom.map_mclosure, hs, iSup_map_mulSingle]

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

Goal state before:
pp: case succ
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : (∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1) → ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∏ k ∈ range (k + 1), f k = s (k + 1)

Tactic:
rw [Finset.prod_range_succ, step _ (Nat.lt_succ_self _), hk]

Goal state after:
case succ
M : Type u_4
inst✝ : CommMonoid M
f s : ℕ → M
base : s 0 = 1
k : ℕ
hk : (∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1) → ∏ k ∈ range k, f k = s k
step : ∀ k_1 < k + 1, s (k_1 + 1) = s k_1 * f k_1
⊢ ∀ k_1 < k, s (k_1 + 1) = s k_1 * f k_1
Module: Mathlib.GroupTheory.Finiteness

Goal state before:
pp: case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑P.toSubmonoid

Tactic:
← hS

Goal state after:
case mpr.refine_1
G : Type u_3
inst✝ : Group G
P : Subgroup G
S : Finset G
hS : Submonoid.closure ↑S = P.toSubmonoid
⊢ ↑S ⊆ ↑(Submonoid.closure ↑S)
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
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ ⊤.FG

Tactic:
← Subgroup.pi_top Set.univ

Goal state after:
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
ι : Type u_5
inst✝² : Finite ι
G : ι → Type u_6
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), Group.FG (G i)
⊢ (Subgroup.pi Set.univ fun i ↦ ⊤).FG
Module: Mathlib.GroupTheory.FreeAbelianGroup

Goal state before:
pp: α : Type u
G : Type u_1
inst✝ : AddCommGroup G
f g : α → G
a : FreeAbelianGroup α
⊢ (lift (f + g)) a = (lift f) a + (lift g) a

Tactic:
induction a using FreeAbelianGroup.induction_on with

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
inst✝ : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ f default = f a

Tactic:
Subsingleton.elim default a

Goal state after:
M : Type u_4
ι : Type u_7
inst✝² : Fintype ι
inst✝¹ : CommMonoid M
inst✝ : Subsingleton ι
f : ι → M
a : ι
this : Unique ι
⊢ f a = f a
Module: Mathlib.GroupTheory.FreeAbelianGroup

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

Tactic:
simp only [zero_smul, map_zero]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
f : S.LocalizationMap N
T : Submonoid M
hST : S ≤ T
Q : Type u_4
inst✝¹ : CommMonoid Q
k : T.LocalizationMap Q
A : Type u_5
inst✝ : CommMonoid A
l : M →* A
hl : ∀ (w : ↥T), IsUnit (l ↑w)
x : M
⊢ ((k.lift hl).comp (f.lift ⋯)) (f x) = l x

Tactic:
by rw [← toMonoidHom_apply, ← MonoidHom.comp_apply,
    MonoidHom.comp_assoc, lift_comp, lift_comp]

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

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * φ (↑s /ₒ 1 * (r /ₒ s)) = ↑(fS s)⁻¹ * φ (r /ₒ 1)

Tactic:
OreLocalization.mul_cancel

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ ↑(fS s)⁻¹ * φ (r /ₒ 1) = ↑(fS s)⁻¹ * φ (r /ₒ 1)
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = sInf (range fun x ↦ ↑x)

Tactic:
Subtype.range_coe_subtype,

Goal state after:
α : Type u_1
inst✝¹ : CompleteLattice α
inst✝ : SuccOrder α
a : α
⊢ sInf (Ioi a) = sInf {x | x > a}
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ Set.Iic 2 = {0, 1, 2}

Tactic:
ext; simp [le_two_iff]

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

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

Tactic:
rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hin
    have h_not_max : ¬IsMax (succ^[n - 1] i) := by
      rcases n with - | n
      · simpa using hin
      rw [Nat.succ_sub_succ_eq_sub, Nat.sub_zero] at hn ⊢
      have h_sub_le : succ^[n] i ≤ succ^[n.succ] i := by
        rw [Function.iterate_succ']
        exact le_succ _
      refine fun h_max => hin fun j hj => ?_
      have hj_le : j ≤ succ^[n] i := h_max (h_sub_le.trans hj)
      exact hj_le.trans h_sub_le
    rw [Function.iterate_succ, Function.iterate_succ']
    simp only [Function.comp_apply]
    rw [pred_succ_of_not_isMax hin]
    exact hn h_not_max

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

Goal state before:
pp: a b : ℕ∞
h : a + b < ⊤
⊢ (a + b).lift h = a.lift ⋯ + b.lift ⋯

Tactic:
apply natCast_inj.1
  simp

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type u_1
F1 : Functor F
p1 : {α : Type u} → α → F α
s1 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl1 : {α β : Type u} → F α → (Unit → F β) → F α
sr1 : {α β : Type u} → F α → (Unit → F β) → F β
F2 : Functor F
s2 : {α β : Type u} → F (α → β) → (Unit → F α) → F β
sl2 : {α β : Type u} → F α → (Unit → F β) → F α
sr2 : {α β : Type u} → F α → (Unit → F β) → F β
L1 : LawfulApplicative F
L2 : LawfulApplicative F
H1 : ∀ {α : Type u} (x : α), pure x = pure x
H2 : ∀ {α β : Type u} (f : F (α → β)) (x : F α), f <*> x = f <*> x
⊢ s1 = s2

Tactic:
funext α β f x
      exact H2 f (x Unit.unit)

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

Goal state before:
pp: α : Type u_3
β : Type u_4
inst✝ : Fintype β
u : Finset (α ⊕ β)
⊢ u.toLeft = ∅ ↔ u ⊆ map Function.Embedding.inr univ

Tactic:
simp [subset_map_inr]

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

Goal state before:
pp: α : Type u_1
n : ℕ
inst✝ : DecidableEq α
a x : α
i : Fin (n + 1)
s : Sym α (n - ↑i)
hx : x ≠ a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
by
  suffices x ∉ Multiset.replicate i a by simp [coe_fill, coe_replicate, this]
  simp [Multiset.mem_replicate, hx]

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

Goal state before:
pp: α✝ : Type u_1
α : Type u_2
β : Type u_3
inst✝² : Preorder α
inst✝¹ : Unique α
inst✝ : LE β
x : Lex (α × β)
x✝ : α × β
a : α
b : β
⊢ (fun x ↦ toLex (default, x)) ((fun x ↦ (ofLex x).2) (toLex (a, b))) = toLex (a, b)

Tactic:
simpa using Unique.default_eq a

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

Goal state before:
pp: case inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inl val✝) ≤ b

Tactic:
rcases b with ((_ | _) | _)

Goal state after:
case inl.inl.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inl (inl val✝¹) ≤ inl (inl val✝)

case inl.inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : α
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inl (inl val✝¹) ≤ inl (inr val✝)

case inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : α
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inl (inl val✝¹) ≤ inr val✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ≤ (Equiv.sumAssoc α β γ) b ↔ inl (inr val✝) ≤ b

Tactic:
rcases b with ((_ | _) | _)

Goal state after:
case inl.inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : β
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inl (inr val✝¹) ≤ inl (inl val✝)

case inl.inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inl (inr val✝¹) ≤ inl (inr val✝)

case inl.inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : β
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inl (inr val✝¹) ≤ inr val✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b✝ : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
b : (α ⊕ β) ⊕ γ
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inr val✝) ≤ (Equiv.sumAssoc α β γ) b ↔ inr val✝ ≤ b

Tactic:
rcases b with ((_ | _) | _)

Goal state after:
case inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : γ
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inr val✝¹ ≤ inl (inl val✝)

case inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : γ
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inr val✝¹ ≤ inl (inr val✝)

case inr.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inr val✝¹) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inr val✝¹ ≤ inr val✝
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case inl.inl.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inl (inl val✝¹) ≤ inl (inl val✝)

Tactic:
simp [Equiv.sumAssoc]

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

Goal state before:
pp: ι : Type u
c : ι → Type v
⊢ #(ULift ((i : ι) → c i)) = #((i : ι) → ULift (c i))

Tactic:
exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

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

Goal state before:
pp: case inl.inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : α
val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inl (inl val✝¹) ≤ inl (inr val✝)

Tactic:
simp [Equiv.sumAssoc]

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

Goal state before:
pp: case inl.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : α
val✝ : γ
⊢ (Equiv.sumAssoc α β γ) (inl (inl val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inr val✝) ↔ inl (inl val✝¹) ≤ inr val✝

Tactic:
simp [Equiv.sumAssoc]

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

Goal state before:
pp: case inl.inr.inl.inl
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ : β
val✝ : α
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inl val✝)) ↔ inl (inr val✝¹) ≤ inl (inl val✝)

Tactic:
simp [Equiv.sumAssoc]

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

Goal state before:
pp: case inl.inr.inl.inr
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
α₁ : Type u_4
α₂ : Type u_5
β₁ : Type u_6
β₂ : Type u_7
γ₁ : Type u_8
γ₂ : Type u_9
inst✝¹¹ : LE α✝
inst✝¹⁰ : LE β✝
inst✝⁹ : LE γ✝
inst✝⁸ : LE α₁
inst✝⁷ : LE α₂
inst✝⁶ : LE β₁
inst✝⁵ : LE β₂
inst✝⁴ : LE γ₁
inst✝³ : LE γ₂
a : α✝
b : β✝
c : γ✝
α : Type u_10
β : Type u_11
γ : Type u_12
inst✝² : LE α
inst✝¹ : LE β
inst✝ : LE γ
val✝¹ val✝ : β
⊢ (Equiv.sumAssoc α β γ) (inl (inr val✝¹)) ≤ (Equiv.sumAssoc α β γ) (inl (inr val✝)) ↔ inl (inr val✝¹) ≤ inl (inr val✝)

Tactic:
simp [Equiv.sumAssoc]

Goal state after: