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

Goal state before:
pp: case inr
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
inj : Injective ⇑k
⊢ f z' = w * f ↑x

Tactic:
hxw,

Goal state after:
case inr
M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
f : S.LocalizationMap N
g : M →* P
T : Submonoid P
hy : ∀ (y : ↥S), g ↑y ∈ T
Q : Type u_4
inst✝ : CommMonoid Q
k : T.LocalizationMap Q
hg : Injective ⇑g
z w : N
i : N →* Q := f.map hy k
hizw : i z = i w
ifkg : ∀ (a : M), i (f a) = k (g a)
z' w' : M
x : ↥S
hxz : z * f ↑x = f z'
hxw : w * f ↑x = f w'
this : k (g z') = k (g w')
inj : Injective ⇑k
⊢ f z' = f w'
Module: Mathlib.GroupTheory.MonoidLocalization.Basic

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

Tactic:
rw [H, mk'_spec]

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

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

Tactic:
rw [mul_comm, mk'_mul_cancel_right]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝² : CommMonoid N
P : Type u_3
inst✝¹ : CommMonoid P
inst✝ : IsMulTorsionFree M
n : ℕ
hn : n ≠ 0
⊢ Injective fun a ↦ a ^ n

Tactic:
by
    rintro ⟨a⟩ ⟨b⟩ (hab : mk a.1 a.2 ^ n = mk b.1 b.2 ^ n)
    change mk a.1 a.2 = mk b.1 b.2
    simp only [mk_pow, mk_eq_mk_iff, r_iff_exists, SubmonoidClass.coe_pow, Subtype.exists,
      exists_prop] at hab ⊢
    obtain ⟨c, hc, hab⟩ := hab
    refine ⟨c, hc, pow_left_injective hn ?_⟩
    obtain _ | n := n
    · simp
    · simp [mul_pow, pow_succ c, mul_assoc, hab]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (n₁ * f ↑ms₁.2 * f ↑ms₂.2) = f m * (n₂ * (f ↑ms₁.2 * f ↑ms₂.2))
⊢ n₁ * f ↑ms₁.2 * f ↑ms₂.2 = n₂ * (f ↑ms₁.2 * f ↑ms₂.2)

Tactic:
eq₁,

Goal state after:
M : Type u_1
N : Type u_2
inst✝¹ : CommMonoid M
S : Submonoid M
inst✝ : CommMonoid N
f : S.LocalizationMap N
m : M
hm : IsRegular m
n₁ n₂ : N
ms₁ : M × ↥S
eq₁ : n₁ * f ↑ms₁.2 = f ms₁.1
ms₂ : M × ↥S
eq₂ : n₂ * f ↑ms₂.2 = f ms₂.1
eq : f m * (f ms₁.1 * f ↑ms₂.2) = f m * (n₂ * (f ↑ms₁.2 * f ↑ms₂.2))
⊢ f ms₁.1 * f ↑ms₂.2 = n₂ * (f ↑ms₁.2 * f ↑ms₂.2)
Module: Mathlib.Algebra.Order.Ring.WithTop

Goal state before:
pp: α : Type u_1
inst✝³ : DecidableEq α
inst✝² : CommMonoidWithZero α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
a b : WithTop α
⊢ a * b = b * a

Tactic:
simp_rw [mul_def]; exact if_congr or_comm rfl (Option.map₂_comm mul_comm)

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

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SuccOrder α
a b : α
h : a ⩿ b
hab : a ⋖ b
⊢ b ≤ succ a

Tactic:
by_contra hba
    exact h.2 (lt_succ_of_not_isMax hab.lt.not_isMax) <| hab.lt.succ_le.lt_of_not_ge hba

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

Goal state before:
pp: α : Type u_1
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
x : α
⊢ pred x ⩿ x

Tactic:
exact pred_wcovBy x

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

Goal state before:
pp: a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑y
⊢ x = default

Tactic:
this.1,

Goal state after:
a b c d m n : ℕ∞
x : ℕ∞ˣ
x_top : ↑x ≠ ⊤
x_inv_top : x.inv ≠ ⊤
y z : ℕ
this : y = 1 ∧ z = 1
x_z : ↑z = x.inv
x_y : ↑x = ↑1
⊢ x = default
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ ≤ ↑↑m ↔ ↑a✝ ≤ ↑m

Tactic:
WithBot.coe_natCast

Goal state after:
case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ ≤ ↑m ↔ ↑a✝ ≤ ↑m
Module: Mathlib.Data.ENat.Basic

Goal state before:
pp: case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑↑n < ↑a✝ ↔ ↑n < ↑a✝

Tactic:
WithBot.coe_natCast

Goal state after:
case coe
n : ℕ
a✝ : ℕ∞
⊢ ↑n < ↑a✝ ↔ ↑n < ↑a✝
Module: Mathlib.Data.Fintype.Sum

Goal state before:
pp: case empty
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq β
t : Finset β
hαt : Fintype.card α = #t
f : α → β
hfst : image f ∅ ⊆ t
hfs : Set.InjOn f ↑∅
⊢ ∃ g, ∀ i ∈ ∅, ↑(g i) = f i

Tactic:
obtain ⟨e⟩ : Nonempty (α ≃ ↥t) := by rwa [← Fintype.card_eq, Fintype.card_coe]
      use e
      simp

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

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).head = f v.head

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).head = f v.head
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
⊢ (map f v).tail = map f v.tail

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Goal state after:
α : Type u_1
n : ℕ
β : Type u_6
v : Vector α (n + 1)
f : α → β
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (map f v).tail = map f v.tail
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).head = f v.head ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
⊢ (pmap f v hp).tail = pmap f v.tail ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Goal state after:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ (x : α), x ∈ v.toList → p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).tail = pmap f v.tail ⋯
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
β : Type u_6
v : Vector α n
f : α → β
i : Fin n
⊢ (map f v).get i = f (v.get i)

Tactic:
by
  cases v; simp [Vector.map, get_eq_get_toList]

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

Goal state before:
pp: α : Type u
ι : Sort x
t : ι → Set α
inst✝ : Countable ι
ht : ∀ (i : ι), (t i).Countable
⊢ (⋃ i, t i).Countable

Tactic:
have := fun i ↦ (ht i).to_subtype
  rw [iUnion_eq_range_psigma]
  apply countable_range

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

Goal state before:
pp: α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
⊢ sSup (Iio x) = x ↔ IsSuccPrelimit x

Tactic:
refine ⟨fun h ↦ ?_, IsSuccPrelimit.sSup_Iio⟩

Goal state after:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot α
x : α
h : sSup (Iio x) = x
⊢ IsSuccPrelimit x
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: case mk
ι : Type u
f : ι → Cardinal.{v}
α : Type v
⊢ lift.{u, v} #α ^ sum f = prod fun i ↦ #α ^ f i

Tactic:
induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm

Goal state after:
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
inst✝¹ : LE α
inst✝ : LE β
a : α
b : β
⊢ (Equiv.sumComm α β) (inl a) ≤ (Equiv.sumComm α β) (inr b) ↔ inl a ≤ inr b

pp: case inr.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 : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ inl b

pp: 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
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ inr b

Tactic:
· exact iff_of_false (@Lex.not_inr_le_inl (OrderDual β) (OrderDual α) _ _ _ _)
          Lex.not_inr_le_inl

Goal state after:
case inr.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 : α
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inl b) ↔ inr a ≤ inl b

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
inst✝¹ : LE α
inst✝ : LE β
a b : β
⊢ (Equiv.sumComm α β) (inr a) ≤ (Equiv.sumComm α β) (inr b) ↔ inr a ≤ inr b
Module: Mathlib.Order.InitialSeg

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
γ : Type u_3
r✝ : α → α → Prop
s✝ : β → β → Prop
t : γ → γ → Prop
r : α → α → Prop
s : β → β → Prop
a : α
val✝ : β
⊢ Sum.Lex r s (Sum.inr val✝) ({ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ } a) →
    Sum.inr val✝ ∈ Set.range ⇑{ toFun := Sum.inl, inj' := ⋯, map_rel_iff' := ⋯ }

Tactic:
exact False.elim ∘ Sum.lex_inr_inl

Goal state after:
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 β s
inst✝ : IsTrans γ t
f : r ≼i s
g : s ≺i t
a : α
⊢ (f.transPrincipal g).toRelEmbedding a = g.toRelEmbedding (f a)

Tactic:
rw [InitialSeg.transPrincipal]
  obtain f' | f' := f.principalSumRelIso
  · rw [PrincipalSeg.trans_apply, f.eq_principalSeg]
  · rw [PrincipalSeg.relIsoTrans_apply, f.eq_relIso]

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
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x ↦ (f x).bind (g x)) x → a ∈ (fun x ↦ (f x).bind (g x)) y

Tactic:
simp only [and_imp, Part.mem_bind_iff, exists_imp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Monotone f
hg : Monotone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f x → a ∈ g x x_1 → ∃ a_3, a_3 ∈ f y ∧ a ∈ g y a_3
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
x y : α
h : x ≤ y
a : γ
⊢ a ∈ (fun x ↦ (f x).bind (g x)) y → a ∈ (fun x ↦ (f x).bind (g x)) x

Tactic:
simp only [and_imp, Part.mem_bind_iff, exists_imp]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Preorder α
f : α → Part β
g : α → β → Part γ
hf : Antitone f
hg : Antitone g
x y : α
h : x ≤ y
a : γ
⊢ ∀ (x_1 : β), x_1 ∈ f y → a ∈ g y x_1 → ∃ a_3, a_3 ∈ f x ∧ a ∈ g x a_3
Module: Mathlib.Data.Part

Goal state before:
pp: case pos
α : Type u_1
o : Part α
inst✝ : Decidable o.Dom
a : α
h : o.Dom
⊢ (a ∈ if h : o.Dom then Option.some (o.get h) else Option.none) ↔ a ∈ o

Tactic:
simpa [h] using ⟨fun h => ⟨_, h⟩, fun ⟨_, h⟩ => h⟩

Goal state after:
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case base_isLeast.left.left
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
⊢ x ∈ bot x f

Tactic:
exact (bot_isAdmissible le_map).base_isLeast.1

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsLUB (Set.range ⇑c) (ωSup c)

Tactic:
by
  constructor
  · simp only [upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
      Set.mem_ofPred_eq]
    exact fun a ↦ le_ωSup c a
  · simp only [lowerBounds, upperBounds, Set.mem_range, forall_exists_index,
      forall_apply_eq_imp_iff, Set.mem_ofPred_eq]
    exact fun ⦃a⦄ a_1 ↦ ωSup_le c a a_1

Goal state after:
Module: Mathlib.Order.CompleteLattice.Chain

Goal state before:
pp: case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ⋃₀ s✝ ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝

Tactic:
apply by_contradiction

Goal state after:
case union
α : Type u_1
r : α → α → Prop
c₂ : Set α
s✝ : Set (Set α)
a✝ : ∀ a ∈ s✝, ChainClosure r a
ih : ∀ a ∈ s✝, ∀ {c₁ : Set α}, ChainClosure r c₁ → c₁ ⊆ a → a = c₁ ∨ SuccChain r c₁ ⊆ a
c₁ : Set α
hc₁ : ChainClosure r c₁
h : c₁ ⊆ ⋃₀ s✝
⊢ ¬(⋃₀ s✝ ⊆ c₁ ∨ SuccChain r c₁ ⊆ ⋃₀ s✝) → False
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: case cSup_mem
α : Type u_1
inst✝ : ChainCompletePartialOrder α
x : α
f : α → α
y : α
le_map : ∀ (x : α), x ≤ f x
hy : IsExtremePt x f y
c : NonemptyChain α
hc : ↑c ⊆ {z | z ∈ bot x f ∧ (z ≤ y ∨ f y ≤ z)}
⊢ cSup c ≤ y ∨ f y ≤ cSup c

Tactic:
by_cases! h : ∀ z ∈ c, z ≤ y
        · left; apply cSup_le c y h
        · rcases h with ⟨z, hz, hzy⟩
          have h' := Or.resolve_left (hc hz).2 hzy
          right
          apply le_trans h' (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
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
⊢ Function.Injective fun f ↦ f.toFun

Tactic:
rintro ⟨⟩ ⟨⟩ h; congr; exact DFunLike.ext' h

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ f x <*> g x

Tactic:
simp only [seq_eq_bind_map]

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part (β → γ)
g : α → Part β
hf : ωScottContinuous f
hg : ωScottContinuous g
⊢ ωScottContinuous fun x ↦ do
    let x_1 ← f x
    x_1 <$> g 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
⊢ Monotone fun x ↦ (f x) (g x)

Tactic:
intro x y 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.ENat

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy

Goal state after:
case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x * y).toENatAux = (↑x).toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x y : Cardinal.{u}
hle : x ≤ y
hy : y < ℵ₀
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
lift x to ℕ using hle.trans_lt hy

Goal state after:
case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x + y).toENatAux = (↑x).toENatAux + y.toENatAux
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:
by
  refine ⟨?_, ?_⟩
  · rintro ⟨ab, ba⟩
    exact ⟨ba.of_mul, ab.of_mul⟩
  · rintro ⟨ha, hb⟩
    exact ⟨ha.mul hb, hb.mul ha⟩

Goal state after:
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}
⊢ prod f = lift.{u, v} (∏ i, f i)

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

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) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a ↦ f (some a)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case h
s : Set Cardinal.{u}
ι : Type u
e : ↑s ≃ ι
a : Cardinal.{u}
ha : a ∈ s
⊢ a ≤ sum fun x ↦ ↑(e.symm x)

Tactic:
simpa using le_sum (fun x ↦ e.symm x) (e ⟨a, ha⟩)

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

Goal state before:
pp: a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀

Tactic:
by
    rcases lt_aleph0.1 ha with ⟨n, rfl⟩
    rw [succ_natCast, ← Nat.cast_add_one]
    apply natCast_lt_aleph0

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

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ (T \ S).Nonempty

Tactic:
← mk_set_ne_zero_iff

Goal state after:
α : Type u
S T : Set α
h : #↑S < #↑T
⊢ #↑(T \ S) ≠ 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
h' : #↑(T \ S) = 0
⊢ False

Tactic:
exact h.not_ge ((le_mk_sdiff_add_mk T S).trans (by simp [h']))

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

Goal state before:
pp: M : Type u_1
inst✝ : NonAssocSemiring M
n : ℕ
x✝¹ x✝ : M
⊢ ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝

Tactic:
induction n with
    | zero => rw [Nat.cast_zero, zero_mul, zero_mul, zero_mul]
    | succ n ihn => rw [Nat.cast_succ, add_mul, one_mul, ihn, add_mul, add_mul, one_mul]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocSemiring R
ι : Sort u_1
S : ι → NonUnitalSubsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Goal state after:
Module: Mathlib.RingTheory.NonUnitalSubring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonUnitalNonAssocRing R
ι : Sort u_1
S : ι → NonUnitalSubring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Goal state after:
Module: Mathlib.Algebra.Ring.Subsemiring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocSemiring R
ι : Sort u_1
S : ι → Subsemiring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: F : Type u_1
E : Type u_2
inst✝² : CommSemiring F
inst✝¹ : Semiring E
inst✝ : Algebra F E
b : F →ₗ[F] E
hb : Injective ⇑b
x y : F
e : (algebraMap F E) x = (algebraMap F E) y
⊢ b x = b y

Tactic:
rw [← mul_one x, ← mul_one y, ← smul_eq_mul, ← smul_eq_mul,
    map_smul, map_smul, Algebra.smul_def, Algebra.smul_def, e]

Goal state after:
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
inst✝ : NonAssocRing R
ι : Sort u_1
S : ι → Subring R
x : R
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

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

Goal state before:
pp: R : Type u_1
inst✝⁴ : Semiring R
M : Type u_10
P : Type u_11
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] P
g : P →ₗ[R] M
h : f ∘ₗ g = id
x : M
hx : x ∈ f.ker
⊢ x - g (f x) = x

Tactic:
rw [hx, map_zero, sub_zero]

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

Goal state before:
pp: case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₁ : ∃ y_1, f y_1 = y
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
⊢ z ∈ p

Tactic:
obtain ⟨x, hx⟩ := h₁

Goal state after:
case mpr
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Ring R
inst✝⁵ : Ring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
f : M →ₛₗ[τ₁₂] M₂
inst✝ : RingHomSurjective τ₁₂
p : Submodule R M
y : M₂
h₂ : ⇑f ⁻¹' {y} ⊆ ↑p
z : M
hz : f z = 0
x : M
hx : f x = y
⊢ z ∈ p
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr.inl
ι : Sort u_1
α✝ : Type u_2
β : Type u_3
inst✝⁵ : PartialOrder α✝
inst✝⁴ : BoundedOrder α✝
inst✝³ : IsSimpleOrder α✝
α : Type ?u.12
inst✝² : LE α
inst✝¹ : BoundedOrder α
inst✝ : IsSimpleOrder α
c : α
⊢ ⊤ ≤ ⊥ → ⊥ ≤ c → ⊤ ≤ c

Tactic:
rcases eq_bot_or_eq_top c with (rfl | rfl) <;> simp

Goal state after:
Module: Mathlib.LinearAlgebra.Span.Defs

Goal state before:
pp: case refine_1.inl
R : Type u_1
M : Type u_4
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_8
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
v : ι → M
r : R
⊢ v j + r • v i ∈ span R (range v)

Tactic:
exact add_mem (subset_span ⟨j, rfl⟩) <| smul_mem _ _ <| subset_span ⟨i, rfl⟩

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
ha'b : ⊥ ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨⊥, ha'b⟩
⊢ a = b

Tactic:
by simpa [codisjoint_bot, ← Subtype.coe_inj] using ha'.codisjoint

Goal state after:
Module: Mathlib.Order.Atoms

Goal state before:
pp: case inr
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ d ⊓ a ⋖ d

Tactic:
convert! hd.1.bot_covBy

Goal state after:
α : Type u_2
inst✝⁴ : Lattice α
inst✝³ : BoundedOrder α
inst✝² : IsModularLattice α
inst✝¹ : ComplementedLattice α
inst✝ : IsAtomic α
a b : α
hab : a < b
a' : α
ha'b : a' ≤ b
ha' : IsCompl ⟨a, ⋯⟩ ⟨a', ha'b⟩
d : α
hd : IsAtom d ∧ d ≤ a'
⊢ d ⊓ a = ⊥
Module: Mathlib.Order.SupIndep

Goal state before:
pp: case hg
α : Type u_1
ι : Type u_3
ι' : Type u_4
inst✝² : Lattice α
inst✝¹ : IsModularLattice α
inst✝ : OrderBot α
s : Finset ι
t : Finset ι'
f : ι × ι' → α
hs : s.SupIndep fun i ↦ t.sup fun i' ↦ f (i, i')
ht : t.SupIndep fun i' ↦ s.sup fun i ↦ f (i, i')
⊢ ∀ i' ∈ s, (image (fun b ↦ (i', b)) t).SupIndep f

Tactic:
exact fun i' hi' ↦ (ht.mono fun i hi ↦ Finset.le_sup (f := fun i' ↦ f (i', i)) hi').image

Goal state after: