mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Tactic:
induction t using Finset.induction_on

Goal state after:
case empty
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ ∅, mk (f i) (s i) = mk (∏ i ∈ ∅, f i) (∏ i ∈ ∅, s i)

case insert
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
f : ι → M
s : ι → ↥S
a✝² : ι
s✝ : Finset ι
a✝¹ : a✝² ∉ s✝
a✝ : ∏ i ∈ s✝, mk (f i) (s i) = mk (∏ i ∈ s✝, f i) (∏ i ∈ s✝, s i)
⊢ ∏ i ∈ insert a✝² s✝, mk (f i) (s i) = mk (∏ i ∈ insert a✝² s✝, f i) (∏ i ∈ insert a✝² s✝, s i)
Module: Mathlib.GroupTheory.OreLocalization.Basic

Goal state before:
pp: case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ r₁' • x /ₒ (s₁' * s) = (s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩))

Tactic:
OreLocalization.expand _ _ _ this

Goal state after:
case c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type ?u.10
inst✝ : MulAction R X
y : OreLocalization S R
r₁ r₂ : R
s : ↥S
hs : r₂ * ↑s ∈ S
x : X
s₂ : ↥S
r₁' : R
s₁' : ↥S
h₁ : ↑s₁' * r₁ = r₁' * ↑s₂
r₂' : R
s₂' : ↥S
h₂ : ↑s₂' * (r₂ * r₁) = r₂' * ↑s₂
r₃' : R
s₃' : ↥S
h₃ : ↑s₃' * (↑s₂' * r₂) = r₃' * ↑s₁'
this✝ : ↑s₃' * r₂' * ↑s₂ = r₃' * r₁' * ↑s₂
s₄' : ↥S
h₄ : ↑s₄' * (↑s₃' * r₂') = ↑s₄' * (r₃' * r₁')
this : ↑s₄' * r₃' * (↑s₁' * ↑s) ∈ S
⊢ (↑s₄' * r₃') • r₁' • x /ₒ ⟨↑s₄' * r₃' * ↑(s₁' * s), this⟩ =
    (s₄' * s₃') • r₂' • x /ₒ (s₄' * s₃' * (s₂' * ⟨r₂ * ↑s, hs⟩))
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 : M
⊢ f.mk' x 1 = f x

Tactic:
by
  rw [mk', map_one]
  exact mul_one _

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

Goal state before:
pp: case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
g : α →+*o β
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) g
⊢ { toRingHom := toRingHom✝, monotone' := monotone'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : NonAssocSemiring α
inst✝⁶ : Preorder α
inst✝⁵ : NonAssocSemiring β
inst✝⁴ : Preorder β
inst✝³ : NonAssocSemiring γ
inst✝² : Preorder γ
inst✝¹ : NonAssocSemiring δ
inst✝ : Preorder δ
toRingHom✝¹ : α →+* β
monotone'✝¹ : Monotone (↑↑toRingHom✝¹).toFun
toRingHom✝ : α →+* β
monotone'✝ : Monotone (↑↑toRingHom✝).toFun
h :
  (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } =
    (fun f ↦ (↑↑f.toRingHom).toFun) { toRingHom := toRingHom✝, monotone' := monotone'✝ }
⊢ { toRingHom := toRingHom✝¹, monotone' := monotone'✝¹ } = { toRingHom := toRingHom✝, monotone' := monotone'✝ }
Module: Mathlib.GroupTheory.OreLocalization.Basic

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

Tactic:
induction n with
  | zero =>
    rw [pow_zero, pow_zero, pow_zero, OreLocalization.one_def]
  | succ n ih =>
    rw [pow_succ', pow_succ', pow_succ, ih, oreDiv_mul_char (r' := r) (s' := s ^ n)]
    exact h.pow_right _ |>.symm

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

Goal state before:
pp: R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ f (-x) = 1 ↔ -x = 1

Tactic:
RingEquiv.map_eq_one_iff

Goal state after:
R : Type u_4
S : Type u_5
inst✝¹ : NonAssocRing R
inst✝ : NonAssocRing S
f : R ≃+* S
x : R
⊢ -x = 1 ↔ -x = 1
Module: Mathlib.Order.Iterate

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

Tactic:
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn,
    h.symm.iterate_pos_le_iff_map_le' hg hf hn]

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

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ a ≤ b ↔ a = b ∨ succ a ≤ b

Tactic:
rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]

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

Goal state before:
pp: α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ pred y ↔ x < y

Tactic:
le_pred_iff_of_not_isMin hy

Goal state after:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x < y ↔ x < y
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ succ a = sInf (Ioi a)

Tactic:
apply (le_csInf nonempty_Ioi fun b => succ_le_of_lt).antisymm

Goal state after:
α : Type u_1
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
⊢ sInf (Ioi a) ≤ succ a
Module: Mathlib.Algebra.Order.SuccPred

Goal state before:
pp: case coe
α : Type u_1
inst✝⁶ : PartialOrder α
inst✝⁵ : AddZeroClass α
inst✝⁴ : OrderBot α
inst✝³ : IsBotZeroClass α
inst✝² : One α
inst✝¹ : NoMaxOrder α
inst✝ : SuccAddOrder α
a✝ : α
⊢ (↑a✝).succ = 0 ↔ ↑a✝ = ⊥

Tactic:
· rename_i a
    simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false, succ_eq_add_one]
    by_contra h
    simpa [h] using max_of_succ_le (a := a)

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

Goal state before:
pp: α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ (x = 0 ∨ x = 1) ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2

Tactic:
or_assoc

Goal state after:
α : Type u_1
x : α
inst✝⁵ : LinearOrder α
inst✝⁴ : AddMonoidWithOne α
inst✝³ : SuccAddOrder α
inst✝² : IsBotZeroClass α
inst✝¹ : NeZero 1
inst✝ : NoMaxOrder α
⊢ x = 0 ∨ x = 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: a x y : ℕ∞
hxy : x ≤ y
ha : a ≠ 0
h_top : a ≠ ⊤
⊢ x * a ≤ y * a

Tactic:
simpa [ha, h_top]

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

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
i : ι
h : i ∈ s
f : ι → M
b : M
⊢ ∏ x ∈ s, Function.update f i b x = b * ∏ x ∈ s \ {i}, f x

Tactic:
rw [update_eq_piecewise, prod_piecewise]
  simp [h]

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

Goal state before:
pp: case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑((Equiv.swap ⟨f a, hfat⟩ (g' a)) (g' i)) = f i

Tactic:
Equiv.swap_apply_of_ne_of_ne,

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ ↑(g' i) = f i

case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ ⟨f a, hfat⟩

case h.inr.a
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
a : α
s : Finset α
has : a ∉ s
H : ∀ {f : α → β}, image f s ⊆ t → Set.InjOn f ↑s → ∃ g, ∀ i ∈ s, ↑(g i) = f i
f : α → β
hfst : image f (insert a s) ⊆ t
hfs : Set.InjOn f ↑(insert a s)
hfst' : image f s ⊆ t
hfs' : Set.InjOn f ↑s
g' : α ≃ ↥t
hg' : ∀ i ∈ s, ↑(g' i) = f i
hfat : f a ∈ t
i : α
hi : i ∈ s
⊢ g' i ≠ g' a
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
this : x ∉ Multiset.replicate (↑i) a
⊢ count x ↑(fill a i s) = count x ↑s

Tactic:
simp [coe_fill, coe_replicate, this]

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

Goal state before:
pp: α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ enumerateCountable h default n ∈ insert default s

Tactic:
enumerateCountable

Goal state after:
α : Type u
s : Set α
h : s.Countable
default : α
n : ℕ
⊢ (match decode n with
    | some y => ↑y
    | none => default) ∈
    insert default s
Module: Mathlib.Data.Sum.Order

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a b : α ⊕ₗ β
⊢ a ≤ b ∧ ¬b ≤ a → a < b

Tactic:
rintro ⟨⟨hab⟩ | ⟨hab⟩ | ⟨a, b⟩, hba⟩

Goal state after:
case refine_2.inl
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a₁✝ a₂✝ : α
hab : a₁✝ ≤ a₂✝
hba : ¬inl a₂✝ ≤ inl a₁✝
⊢ inl a₁✝ < inl a₂✝

case refine_2.inr
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
b₁✝ b₂✝ : β
hab : b₁✝ ≤ b₂✝
hba : ¬inr b₂✝ ≤ inr b₁✝
⊢ inr b₁✝ < inr b₂✝

case refine_2.sep
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
a : α
b : β
hba : ¬inr b ≤ inl a
⊢ inl a < inr b
Module: Mathlib.Dynamics.FixedPoints.Defs

Goal state before:
pp: α : Type u_1
x✝ : α
⊢ x✝ ∈ fixedPoints id ↔ x✝ ∈ Set.univ

Tactic:
by simpa using isFixedPt_id _

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
inst✝¹ : LE α
inst✝ : LE β
a b : α
⊢ inl (toDual a) ≤ inl (toDual b) ↔ toDual (inl a) ≤ toDual (inl b)

Tactic:
simp [toDual_le_toDual, inl_le_inl_iff]

Goal state after:
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst✝ : IsWellOrder β s
f : r ≼i s
b : β
h✝ : ∀ (b : β), ∃ x, x ∈ Set.range ⇑f ∧ ¬s x b ∨ x ∉ Set.range ⇑f ∧ s x b
x : β
IH : ∀ (y : β), s y x → ∃ a, f a = y
y : β
hy : y ∈ Set.range ⇑f
hs : ¬s y x
h : s x y
⊢ ∃ a, f a = x

Tactic:
obtain ⟨z, rfl⟩ := hy

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β
g : α → γ
hf : ScottContinuous f
hg : ScottContinuous g
⊢ ScottContinuous fun x ↦ (f x, g x)

Tactic:
by
  rw [← scottContinuousOn_univ] at ⊢ hf hg
  exact ScottContinuousOn.prodMk (by grind) hf hg

Goal state after:
Module: Mathlib.Data.Part

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
f : α → Part β
x : Part α
g : β → γ
⊢ map g (x.bind f) = x.bind fun y ↦ map g (f y)

Tactic:
rw [← bind_some_eq_map, bind_assoc]; simp [bind_some_eq_map]

Goal state after:
Module: Mathlib.Order.FixedPoints

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
⊢ sSup s = lfp f

Tactic:
have h : sSup s ≤ f.lfp := sSup_le fun b => And.left

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
p : α → Prop
step : ∀ (a : α), p a → a ≤ lfp f → p (f a)
s : Set α := {a | a ≤ lfp f ∧ p a}
hSup : p (sSup s)
h : sSup s ≤ lfp f
⊢ sSup s = lfp f
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case succ.inr
α : Type u_1
r : α → α → Prop
c₂ s✝ : Set α
a✝ : ChainClosure r s✝
ih : ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ s✝ → s✝ = c₁ ∨ SuccChain r c₁ ⊆ s✝
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ SuccChain r s✝
h₁ : c₁ ⊆ s✝
h₂ : SuccChain r c₁ ⊆ s✝
⊢ SuccChain r c₁ ⊆ SuccChain r s✝

Tactic:
· exact h₂.trans subset_succChain

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
f g : α → β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous (f ⊔ g)

Tactic:
rw [← sSup_pair]
  apply ωScottContinuous.sSup
  rintro f (rfl | rfl | _) <;> assumption

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ᶜ
y : α
hy : y ∈ sᶜ
⊢ g' x = g' y → x = y

Tactic:
hxy

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 : α
hy : y ∈ sᶜ
hxy : g' x = g' y
⊢ x = y
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 y : α
⊢ x ≤ y → (fun x ↦ (f x) (g x)) x ≤ (fun x ↦ (f x) (g x)) y

Tactic:
hxy

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 : α
hxy : 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_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' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g x' = g y'

Tactic:
hxy

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' : β
left✝¹ : x' ∈ (f '' s)ᶜ
hx : g x' ∈ sᶜ
y' : β
left✝ : y' ∈ (f '' s)ᶜ
hy : g y' ∈ sᶜ
hxy : x' = y'
⊢ g y' = g y'
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case refine_1
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b

Tactic:
refine inductionOn₂ a b fun _ _ ↦ ?_
    rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]

Goal state after:
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 : α
hy : y ∉ s
⊢ f x ≠ g' y

Tactic:
hxy

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 : α
hy : y ∉ s
hxy : f x = g' y
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
β

Goal state after:
case refine_1
α✝ : Type u
h : Fintype α✝
α β : Type u
⊢ ∀ [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ lift.{u, v} (f none) * lift.{v, max u v} #((a : α) → Quotient.out (f (some a))) = lift.{u, v} (∏ i, f i)

Tactic:
←
        Cardinal.prod,

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ lift.{u, v} (f none) * lift.{v, max u v} (prod fun a ↦ f (some a)) = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case e'_2
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ x = g⁻¹ • (fun x ↦ g • x) x

Tactic:
simp [← smul_assoc]

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

Goal state before:
pp: case e'_3
R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
x y : R
h : (fun x ↦ g • x) x = (fun x ↦ g • x) y
⊢ y = g⁻¹ • (fun x ↦ g • x) y

Tactic:
simp [← smul_assoc]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ Subsingleton ↑s ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton

Tactic:
Set.subsingleton_coe,

Goal state after:
α : Type u
s : Set α
⊢ s.Subsingleton ∧ s.Nonempty ↔ s.Nonempty ∧ s.Subsingleton
Module: Mathlib.Algebra.GroupWithZero.Action.Hom

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : Zero A
inst✝² : Zero B
inst✝¹ : Zero C
inst✝ : SMulZeroClass M B
r : M
f : ZeroHom A B
⊢ r • f 0 = 0

Tactic:
simp only [map_zero, smul_zero]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst✝³ : AddZeroClass A
inst✝² : AddZeroClass B
inst✝¹ : AddZeroClass C
inst✝ : DistribSMul M B
r : M
f : A →+ B
⊢ r • f 0 = 0

Tactic:
simp only [map_zero, smul_zero]

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

Goal state before:
pp: case mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
g : M →ₛₗ[σ] M₃
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h : (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = (fun f ↦ f.toFun) g
⊢ { toAddHom := toAddHom✝, map_smul' := map_smul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
S : Type u_5
S₃ : Type u_6
T : Type u_7
M : Type u_8
M₁ : Type u_9
M₂ : Type u_10
M₃ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₁
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module S M₃
σ : R →+* S
toAddHom✝¹ : M →ₙ+ M₃
map_smul'✝¹ : ∀ (m : R) (x : M), toAddHom✝¹.toFun (m • x) = σ m • toAddHom✝¹.toFun x
toAddHom✝ : M →ₙ+ M₃
map_smul'✝ : ∀ (m : R) (x : M), toAddHom✝.toFun (m • x) = σ m • toAddHom✝.toFun x
h :
  (fun f ↦ f.toFun) { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } =
    (fun f ↦ f.toFun) { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
⊢ { toAddHom := toAddHom✝¹, map_smul' := map_smul'✝¹ } = { toAddHom := toAddHom✝, map_smul' := map_smul'✝ }
Module: Mathlib.GroupTheory.GroupAction.Hom

Goal state before:
pp: case mk
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
g : X →ₑ[φ] Y
toFun✝ : X → Y
map_smul'✝ : ∀ (m : M) (x : X), toFun✝ (m • x) = φ m • toFun✝ x
h : { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, map_smul' := map_smul'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
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
toFun✝¹ : X → Y
map_smul'✝¹ : ∀ (m : M) (x : X), toFun✝¹ (m • x) = φ m • toFun✝¹ x
toFun✝ : X → Y
map_smul'✝ : ∀ (m : M) (x : X), toFun✝ (m • x) = φ m • toFun✝ x
h : { toFun := toFun✝¹, map_smul' := map_smul'✝¹ }.toFun = { toFun := toFun✝, map_smul' := map_smul'✝ }.toFun
⊢ { toFun := toFun✝¹, map_smul' := map_smul'✝¹ } = { toFun := toFun✝, map_smul' := map_smul'✝ }