mathlib-initiative/mathlib-tactics huggingface dataset:
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 ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ (↑(insert j s)).piecewise f g x✝ = (insert j ↑s).piecewise f g x✝

Tactic:
congr

Goal state after:
case e_s
ι : Type u_1
π : ι → Sort u_2
s : Finset ι
f g : (i : ι) → π i
inst✝² : (j : ι) → Decidable (j ∈ s)
inst✝¹ : DecidableEq ι
j : ι
inst✝ : (i : ι) → Decidable (i ∈ insert j s)
x✝ : ι
⊢ ↑(insert j s) = insert j ↑s
Module: Mathlib.Algebra.BigOperators.Group.Finset.Piecewise

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ ∏ i ∈ s.attach, f i = ∏ x ∈ {x | x ∈ s}.attach, f ⟨↑x, ⋯⟩

Tactic:
congr

Goal state after:
case e_1
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun x ↦ x ∈ s) = fun x ↦ x ∈ {x | x ∈ s}

case e_4.e_2
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ s = {x | x ∈ s}

case e_5
ι : Type u_1
M : Type u_3
inst✝² : CommMonoid M
inst✝¹ : Fintype ι
s : Finset ι
f : ↥s → M
inst✝ : DecidablePred fun x ↦ x ∈ s
⊢ (fun i ↦ f i) ≍ fun x ↦ f ⟨↑x, ⋯⟩
Module: Mathlib.Control.Traversable.Basic

Goal state before:
pp: case mk.mk
F : Type u → Type v
inst✝¹ : Applicative F
G : Type u → Type w
inst✝ : Applicative G
app✝¹ : (α : Type u) → F α → G α
preserves_pure'✝¹ : ∀ {α : Type u} (x : α), app✝¹ α (pure x) = pure x
preserves_seq'✝¹ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝¹ β (x <*> y) = app✝¹ (α → β) x <*> app✝¹ α y
app✝ : (α : Type u) → F α → G α
preserves_pure'✝ : ∀ {α : Type u} (x : α), app✝ α (pure x) = pure x
preserves_seq'✝ : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app✝ β (x <*> y) = app✝ (α → β) x <*> app✝ α y
h :
  (fun {α} ↦ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ }.app α) =
    fun {α} ↦ { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }.app α
⊢ { app := app✝¹, preserves_pure' := preserves_pure'✝¹, preserves_seq' := preserves_seq'✝¹ } =
    { app := app✝, preserves_pure' := preserves_pure'✝, preserves_seq' := preserves_seq'✝ }

Tactic:
congr

Goal state after:
Module: Mathlib.Control.Applicative

Goal state before:
pp: F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ (fun a x ↦ Prod.mk <$> x <*> a) <$> x✝ <*> x✝¹ = (fun a x2 ↦ (fun b a ↦ (a, b)) <$> a <*> x2) <$> x✝ <*> x✝¹

Tactic:
congr

Goal state after:
case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
⊢ (fun a x ↦ Prod.mk <$> x <*> a) = fun a x2 ↦ (fun b a ↦ (a, b)) <$> a <*> x2
Module: Mathlib.Control.Applicative

Goal state before:
pp: case e_a.e_a
F : Type u → Type w
G : Type v → Type u
inst✝⁷ : Applicative F
inst✝⁶ : Applicative G
inst✝⁵ : LawfulApplicative F
inst✝⁴ : LawfulApplicative G
α β γ : Type v
f : Type u → Type w
g : Type v → Type u
inst✝³ : Applicative f
inst✝² : Applicative g
inst✝¹ : CommApplicative f
inst✝ : CommApplicative g
α✝ β✝ : Type v
x✝¹ : Comp f g α✝
x✝ : Comp f g β✝
x : g β✝
y : g α✝
⊢ flip Prod.mk <$> x <*> y = (fun b a ↦ (a, b)) <$> x <*> y

Tactic:
congr

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

Goal state before:
pp: α : Sort u
β : Sort v
π : α → Sort w
inst✝¹ : Finite α
inst✝ : ∀ (a : α), Countable (π a)
this : ∀ (n : ℕ), Countable (Fin n → ℕ)
n : ℕ
e : α ≃ Fin n
f : (a : α) → π a ↪ ℕ
⊢ Countable ((a : α) → π a)

Tactic:
exact ((Embedding.piCongrRight f).trans (Equiv.piCongrLeft' _ e).toEmbedding).countable

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

Goal state before:
pp: α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ ofFn (ofFn f).tail.get = ofFn fun i ↦ f i.succ

Tactic:
congr

Goal state after:
α : Type u_1
n : ℕ
f : Fin n.succ → α
⊢ (ofFn f).tail.get = fun i ↦ f i.succ
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: case succ.succ
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (scanl f b (v.head ::ᵥ v.tail)).get i.succ =
    f ((scanl f b (v.head ::ᵥ v.tail)).get i.castSucc) ((v.head ::ᵥ v.tail).get i)

Tactic:
scanl_cons,

Goal state after:
case succ.succ
α : Type u_1
β : Type u_6
f : β → α → β
n : ℕ
hn :
  ∀ (b : β) (v : Vector α (n + 1)) (i : Fin (n + 1)),
    (scanl f b v).get i.succ = f ((scanl f b v).get i.castSucc) (v.get i)
b : β
v : Vector α (n + 1 + 1)
i : Fin (n + 1 + 1)
⊢ (b ::ᵥ scanl f (f b v.head) v.tail).get i.succ =
    f ((b ::ᵥ scanl f (f b v.head) v.tail).get i.castSucc) ((v.head ::ᵥ v.tail).get i)
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
a b : α
i j : Fin (n + 1)
h : i ≤ j
l : List α
hl : l.length = n
⊢ insertIdx b j.succ (insertIdx a i ⟨l, hl⟩) = insertIdx a i.castSucc (insertIdx b j ⟨l, hl⟩)

Tactic:
refine Subtype.ext ?_
    simp only [insertIdx_val, Fin.val_succ, Fin.castSucc, Fin.val_castAdd]
    apply List.insertIdx_comm
    · assumption
    · rw [hl]
      exact Nat.le_of_succ_le_succ j.2

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

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
x y : α
h : y < x
⊢ (sumLexIioIci x).symm y = toLex (Sum.inl ⟨y, h⟩)

Tactic:
rw [symm_apply_eq, sumLexIioIci_apply_inl]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LT α
inst✝ : LT β
x✝ : DenselyOrdered (α ⊕ β)
a b : α
h : a < b
⊢ ∃ a_1, a < a_1 ∧ a_1 < b

Tactic:
by
        obtain ⟨c | c, ha, hb⟩ := @exists_between (α ⊕ β) _ _ _ _ (inl_lt_inl_iff.2 h)
        · exact ⟨c, inl_lt_inl_iff.1 ha, inl_lt_inl_iff.1 hb⟩
        · exact (not_inl_lt_inr ha).elim

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

Goal state before:
pp: α : Type u_1
inst✝ : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = sᶜᶜ

Tactic:
rw [compl_compl]

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
⊢ (¬∃ b, ∀ (x : β), x ∈ Set.range ⇑f ↔ s x b) → Surjective ⇑f

Tactic:
intro h b

Goal state after:
α : 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
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf } =
    { toRelEmbedding := { toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding, top := b,
      mem_range_iff_rel' := hg }

Tactic:
congr

Goal state after:
case e_top
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝¹ : Std.Irrefl s
inst✝ : Std.Trichotomous s
f : r ↪r s
a : β
hf : ∀ (b : β), b ∈ Set.range ⇑f ↔ s b a
b : β
hg : ∀ (b_1 : β), b_1 ∈ Set.range ⇑{ toRelEmbedding := f, top := a, mem_range_iff_rel' := hf }.toRelEmbedding ↔ s b_1 b
⊢ a = b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ f.top = g.top

Tactic:
Subsingleton.elim f (PrincipalSeg.relIsoTrans e g)

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder γ t
e : r ≃r s
f : r ≺i t
g : s ≺i t
⊢ (relIsoTrans e g).top = g.top
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
γ : Type u_3
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
inst✝ : IsWellOrder β s
f : r ↪r s
H : IsWellOrder α r
a : α
b : β
h✝ : s b ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a)
m : α
hm : m ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}
hm' : ∀ x ∈ {a | ¬s ((ofMonotone (fun a ↦ ↑(collapseF f a)) ⋯) a) b}, ¬r x m
lt : s b ↑(collapseF f m)
c : α
h : r c m
hn : ¬s (↑(collapseF f c)) b
⊢ False

Tactic:
exact hm' _ hn h

Goal state after:
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
⊢ Monotone fun x ↦ (f x).bind (g x)

Tactic:
rintro x y h a
  simp only [and_imp, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Goal state after:
Module: Mathlib.Order.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
⊢ Antitone fun x ↦ (f x).bind (g x)

Tactic:
rintro x y h a
  simp only [and_imp, Part.mem_bind_iff, exists_imp]
  exact fun b hb ha ↦ ⟨b, hf h _ hb, hg h _ _ ha⟩

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
a : Part α
ha : a.Dom
b : Part α
h : a = b
⊢ a.get ha = b.get ⋯

Tactic:
congr

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
this : (p : Prop) → Decidable p
o : Option α
⊢ (↑o).toOption = (↑o).toOption

Tactic:
congr

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 δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } = { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }

Tactic:
congr

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
toOrderHom✝¹ : α →o β
map_ωSup'✝¹ : ∀ (c : Chain α), toOrderHom✝¹.toFun (ωSup c) = ωSup (c.map toOrderHom✝¹)
toOrderHom✝ : α →o β
map_ωSup'✝ : ∀ (c : Chain α), toOrderHom✝.toFun (ωSup c) = ωSup (c.map toOrderHom✝)
h :
  (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toOrderHom := toOrderHom✝, map_ωSup' := map_ωSup'✝ }
⊢ toOrderHom✝¹ = toOrderHom✝
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 δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
map_ωSup'✝¹ :
  ∀ (c : Chain α),
    { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝¹, monotone' := monotone'✝¹ })
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
map_ωSup'✝ :
  ∀ (c : Chain α),
    { toFun := toFun✝, monotone' := monotone'✝ }.toFun (ωSup c) =
      ωSup (c.map { toFun := toFun✝, monotone' := monotone'✝ })
h :
  (fun f ↦ f.toFun) { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    (fun f ↦ f.toFun) { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }
⊢ { toFun := toFun✝¹, monotone' := monotone'✝¹, map_ωSup' := map_ωSup'✝¹ } =
    { toFun := toFun✝, monotone' := monotone'✝, map_ωSup' := map_ωSup'✝ }

Tactic:
congr

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

Goal state before:
pp: case refine_1
α : 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ᶜ
⊢ ∀ ⦃x₂ : α⦄, x₂ ∈ sᶜ → g' x = g' x₂ → x = x₂

Tactic:
y

Goal state after:
case refine_1
α : 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 : α
⊢ y ∈ sᶜ → g' x = g' y → x = y
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
⊢ (c.map (f.partBind g)) i ≤ x

Tactic:
y

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
⊢ y ∈ (c.map (f.partBind g)) i → y ∈ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
hy : ∃ a ∈ f (c i), y ∈ g (c i) a
⊢ y ∈ x

Tactic:
rcases hy with ⟨b, hb₀, hb₁⟩

Goal state after:
case mpr
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
x : Part γ
h''' : ∀ a ∈ ωSup (c.map f), ωSup (c.map g) a ≤ x
i : ℕ
y : γ
b : β
hb₀ : b ∈ f (c i)
hb₁ : y ∈ g (c i) b
⊢ y ∈ x
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
x : α
⊢ ∀ ⦃b : α⦄, x ≤ b → (fun x ↦ (f x) (g x)) x ≤ (fun x ↦ (f x) (g x)) b

Tactic:
y

Goal state after:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
x y : α
⊢ x ≤ y → (fun x ↦ (f x) (g x)) x ≤ (fun x ↦ (f x) (g x)) y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case refine_2
α : 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 ∉ s, f x ≠ g' y

Tactic:
y

Goal state after:
case refine_2
α : 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 : α
⊢ y ∉ s → f x ≠ g' y
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
⊢ Cardinal.{u} ≤i Cardinal.{max u v}

Tactic:
by
  refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩ <;> intro a b
  · refine inductionOn₂ a b fun _ _ ↦ ?_
    rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
  · refine inductionOn₂ a b fun α β h ↦ ?_
    obtain ⟨e⟩ := h.le
    replace e := e.congr (Equiv.refl β) Equiv.ulift
    refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
    apply (e.codRestrict _ mem_range_self).equivOfSurjective
    rintro ⟨a, ⟨b, rfl⟩⟩
    exact ⟨b, rfl⟩

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

Goal state before:
pp: case inr.isFalse
α : 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
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)

Tactic:
· have : g (invFun g a) = a := by
      have : a ∈ g '' (f '' s)ᶜ := by grind
      obtain ⟨x, _, hx⟩ := mem_image _ _ _ |>.mp this
      exact Function.invFun_eq ⟨x, hx⟩
    grind

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a

Tactic:
by
  simpa using nat_lt_lift_iff (n := 0)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = χ x

Tactic:
by
  rw [← h.comp_eq, MonoidHom.comp_apply]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
refine ⟨?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) → IsSMulRegular M a ∧ IsSMulRegular M b

case refine_2
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M a ∧ IsSMulRegular M b → IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
intro f
    rw [Fintype.univ_pempty, Finset.prod_empty, lift_one, Cardinal.prod, mk_eq_one]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ 0)

Tactic:
rw [pow_zero]

Goal state after:
case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) → IsSMulRegular M a

Tactic:
rw [← Nat.succ_pred_eq_of_pos n0, pow_succ, ← smul_eq_mul]

Goal state after:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x : R
⊢ ∀ ⦃a₂ : R⦄, (fun x ↦ g • x) x = (fun x ↦ g • x) a₂ → x = a₂

Tactic:
y

Goal state after:
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
⊢ (fun x ↦ g • x) x = (fun x ↦ g • x) y → x = y
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (iInf f) = ⨅ i, lift.{u, v} (f i)

Tactic:
unfold iInf

Goal state after:
ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (sInf (range f)) = sInf (range fun i ↦ lift.{u, v} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
H : ↑n < #α
⊢ ∃ s, n < s.card

Tactic:
apply exists_finset_le_card α (n + 1)

Goal state after:
α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑(n + 1) ≤ #α
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
this : S.Finite
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
by
      lift S to Finset ℕ using this
      simp

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #↑(f ⁻¹' s) ≤ #↑s

Tactic:
← lift_id #(↑(f ⁻¹' s)),

Goal state after:
α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ lift.{u, u} #↑(f ⁻¹' s) ≤ #↑s
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ #↑(f ⁻¹' s)

Tactic:
← lift_id #(↑(f ⁻¹' s)),

Goal state after:
α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ lift.{u, u} #↑(f ⁻¹' s)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : FaithfulSMul M α
inst✝ : Nonempty β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
b : β
a : α
⊢ m₁✝ • a = m₂✝ • a

Tactic:
by injection h (a, b)

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

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : SMul M α
inst✝⁴ : SMul M β
inst✝³ : SMul N α
inst✝² : SMul N β
a✝ : M
x : α × β
inst✝¹ : Nonempty α
inst✝ : FaithfulSMul M β
m₁✝ m₂✝ : M
h : ∀ (a : α × β), m₁✝ • a = m₂✝ • a
a : α
b : β
⊢ m₁✝ • b = m₂✝ • b

Tactic:
by injection h (a, b)

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
Q : Algebra R A
algebraMap✝ : R →+* A
commutes'✝ : ∀ (r : R) (x : A), algebraMap✝ r * x = x * algebraMap✝ r
P : R → A → A
smul_def'✝ : ∀ (r : R) (x : A), r • x = algebraMap✝ r * x
h : algebraMap R A = algebraMap R A
h' : (fun x1 x2 ↦ x1 • x2) = fun x1 x2 ↦ x1 • x2
⊢ { smul := P, algebraMap := algebraMap✝, commutes' := commutes'✝, smul_def' := smul_def'✝ } = Q

Tactic:
congr

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

Goal state before:
pp: case e_4.e_2
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 α
x✝ : MulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α

Tactic:
congr

Goal state after:
case e_4.e_2.e_4.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 α
x✝ : MulAction N α
⊢ compHom α (MonoidHom.inl M N) = hM