mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.BigOperators.Group.Finset.Basic

Goal state before:
pp: ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
⊢ ∏ x ∈ s \ {a}, f x = ∏ x ∈ s, f x

Tactic:
refine prod_subset sdiff_subset fun x hx hnx => ?_

Goal state after:
ι : Type u_1
M : Type u_4
inst✝¹ : CommMonoid M
inst✝ : DecidableEq ι
s : Finset ι
f : ι → M
a : ι
h : f a = 1
x : ι
hx : x ∈ s
hnx : x ∉ s \ {a}
⊢ f x = 1
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
b₁ b₂ : M
a : ι
ha : a ∈ s
h : f a * b₁ = f a * b₂
⊢ (∏ a ∈ s, f a) * b₁ = (∏ a ∈ s, f a) * b₂

Tactic:
rw [← insert_erase ha]
  simp only [mem_erase, ne_eq, not_true_eq_false, false_and, not_false_eq_true, prod_insert]
  rw [mul_assoc, mul_comm, mul_assoc, mul_comm b₁, h, ← mul_assoc, mul_comm _ (f a)]

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
⊢ ⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆ ≤ center G

Tactic:
rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]

Goal state after:
G : Type u_1
inst✝ : Group G
⊢ ⁅⁅centralizer ↑(commutator G), centralizer ↑(commutator G)⁆, ⊤⁆ = ⊥
Module: Mathlib.GroupTheory.Commutator.Basic

Goal state before:
pp: G : Type u_1
inst✝ : Group G
g : G
hg : IsConj g (g ^ 2)
⊢ g ∈ commutatorSet G

Tactic:
obtain ⟨h, hg⟩ := hg
  use h, g
  rw [commutatorElement_def, hg]
  simp only [IsUnit.mul_inv_cancel_right, Units.isUnit, mul_inv_eq_iff_eq_mul, pow_two]

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ Subgroup.map H.subtype ⊤ ⊔ N = ⊤ ⊔ N

Tactic:
sup_comm,

Goal state after:
G : Type u_1
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative ↥H
φ : ↥H →ₙ* G ⧸ N := ↑((QuotientGroup.mk' N).comp H.subtype)
this : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤
⊢ N ⊔ Subgroup.map H.subtype ⊤ = ⊤ ⊔ N
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
n : ℤ
⊢ (lift fun x ↦ 1) ((fun n ↦ n • of default) n) = n

Tactic:
rw [map_zsmul, lift_apply_of]

Goal state after:
α : Type u
G : Type u_1
β : Type v
γ : Type w
T : Type u_2
inst✝ : Unique T
n : ℤ
⊢ n • 1 = n
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
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (n * f ↑s) = k (n * f ↑s)

Tactic:
hn,

Goal state after:
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
f : S.LocalizationMap N
P : Type u_4
inst✝ : Monoid P
j k : N →* P
n : N
m : M
s : ↥S
hn : n * f ↑s = f m
h : ∀ (a : M), j (f a) = k (f a)
⊢ j (f m) = k (f m)
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 t : ↥S
⊢ ↑s /ₒ t * (r /ₒ s) = r /ₒ t

Tactic:
by
  simp [oreDiv_mul_char s.1 r t s 1 1 (by simp)]

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

Goal state before:
pp: S : AddSubmonoid ℕ
hS : S ≠ ⊥
z : ℤ
⊢ ∃ x, ∃ y ∈ S, z = ↑x - ↑y

Tactic:
by
    obtain ⟨z, rfl | rfl⟩ := z.eq_nat_or_neg
    · exact ⟨z, 0, zero_mem _, by lia⟩
    have ⟨n, hnS, hn0⟩ := S.bot_or_exists_ne_zero.resolve_left hS
    have key : z < n * (z / n + 1) := Nat.lt_mul_div_succ _ <| Nat.pos_of_ne_zero hn0
    exact ⟨(z / n + 1) * n - z, (z / n + 1) * n, nsmul_mem hnS _, by lia⟩

Goal state after:
Module: Mathlib.Order.Iterate

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

Tactic:
by
  apply hf.seq_pos_lt_seq_of_le_of_lt hn
  · rfl
  · intros; rw [iterate_succ_apply']
  · simp [h.iterate_right _ _, hg.iterate _ hx]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
a b : αᵒᵈ
h : a ≤ b
⊢ ∃ n, succ^[n] a = b

Tactic:
by convert! exists_pred_iterate_of_le h.ofDual

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
⊢ False

Tactic:
have := ha ⟨b, hs hb.le a.2⟩

Goal state after:
α : Type u_1
inst✝ : Preorder α
s : Set α
hs : IsLowerSet s
a : ↑s
ha : IsSuccPrelimit a
b : α
hb : b ⋖ ↑a
this : ¬⟨b, ⋯⟩ ⋖ a
⊢ False
Module: Mathlib.Order.SuccPred.Limit

Goal state before:
pp: α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
⊢ succ a < b

Tactic:
by_cases h : IsMax a

Goal state after:
case pos
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : IsMax a
⊢ succ a < b

case neg
α : Type u_1
a b : α
inst✝¹ : PartialOrder α
inst✝ : SuccOrder α
hb : IsSuccPrelimit b
ha : a < b
h : ¬IsMax a
⊢ succ a < b
Module: Mathlib.Order.SuccPred.Basic

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

Tactic:
by_cases ha : IsMax a
  · simpa [ha.succ_eq] using le_of_eq
  · rw [succ_le_iff_of_not_isMax ha, le_iff_eq_or_lt]

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

Goal state before:
pp: α : Type u_1
a : α
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
⊢ False

Tactic:
obtain rfl := isLUB_Iic.unique ha

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) b
hb : b ⋖ b
⊢ False
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
⊢ f (succ a) = succ (f a)

Tactic:
by_cases h : IsMax a

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : IsMax a
⊢ f (succ a) = succ (f a)

case neg
α : Type u_1
β : Type u_2
inst✝³ : PartialOrder α
inst✝² : SuccOrder α
inst✝¹ : PartialOrder β
inst✝ : SuccOrder β
f : α ≃o β
a : α
h : ¬IsMax a
⊢ f (succ a) = succ (f a)
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred^[n + 1] b ∈ s
⊢ f (pred^[n + 1] b) ≤ f b

Tactic:
rw [Function.iterate_succ_apply'] at ha ⊢

Goal state after:
case succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) ≤ f a
b : α
hb : b ∈ s
n : ℕ
hn : pred^[n] b ∈ s → f (pred^[n] b) ≤ f b
ha : pred (pred^[n] b) ∈ s
⊢ f (pred (pred^[n] b)) ≤ f b
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
⊢ (if h : pred x ∈ s then ⟨pred x, h⟩ else ⟨x, hx⟩) ≤ ⟨x, hx⟩

Tactic:
split

Goal state after:
case isTrue
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h✝ : pred x ∈ s
⊢ ⟨pred x, h✝⟩ ≤ ⟨x, hx⟩

case isFalse
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝ : ↑s
x : α
hx : x ∈ s
h✝ : pred x ∉ s
⊢ ⟨x, hx⟩ ≤ ⟨x, hx⟩
Module: Mathlib.Order.SuccPred.Basic

Goal state before:
pp: α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
⊢ ⟨b, hb⟩ ≤ if h : pred c ∈ s then ⟨pred c, h⟩ else ⟨c, hc⟩

Tactic:
split

Goal state after:
case isTrue
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∈ s
⊢ ⟨b, hb⟩ ≤ ⟨pred c, h✝⟩

case isFalse
α✝ : Type u_1
β : Type u_2
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
x✝¹ x✝ : ↑s
b : α
hb : b ∈ s
c : α
hc : c ∈ s
h : b < c
h✝ : pred c ∉ s
⊢ ⟨b, hb⟩ ≤ ⟨c, hc⟩
Module: Mathlib.Order.SuccPred.Archimedean

Goal state before:
pp: case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred^[n + 1 + 1] b ∈ s
⊢ f (pred^[n + 1 + 1] b) < f b

Tactic:
rw [Function.iterate_succ_apply'] at ha ⊢

Goal state after:
case succ.succ
α : Type u_3
β : Type u_4
inst✝³ : PartialOrder α
inst✝² : Preorder β
inst✝¹ : PredOrder α
inst✝ : IsPredArchimedean α
s : Set α
f : α → β
hs : s.OrdConnected
hf : ∀ (a : α), ¬IsMin a → a ∈ s → pred a ∈ s → f (pred a) < f a
b : α
hb : b ∈ s
hab : ¬IsMin b
n : ℕ
hn : pred^[n + 1] b ∈ s → f (pred^[n + 1] b) < f b
ha : pred (pred^[n + 1] b) ∈ s
⊢ f (pred (pred^[n + 1] b)) < f b
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
⊢ (if ↑i ≤ n then n + 1 else n) = n + 1

Tactic:
split

Goal state after:
case isTrue
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ↑i ≤ n
⊢ n + 1 = n + 1

case isFalse
α : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
β : Type u_6
γ : Type u_7
a✝ a : α
i : Fin (n + 1)
v : Vector α n
h✝ : ¬↑i ≤ n
⊢ n = n + 1
Module: Mathlib.Data.Vector.Basic

Goal state before:
pp: α : Type u_1
n : ℕ
v : Vector α n
i : Fin n
a : α
⊢ (v.set i a).get i = a

Tactic:
cases v; cases i; simp [Vector.set, get_eq_get_toList]

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

Goal state before:
pp: α✝ : 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 γ
a b : (α ⊕ β) ⊕ γ
⊢ (Equiv.sumAssoc α β γ) a ≤ (Equiv.sumAssoc α β γ) b ↔ a ≤ b

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

Goal state after:
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

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

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
Module: Mathlib.SetTheory.Cardinal.Defs

Goal state before:
pp: ι : Type u
c : ι → Type v
⊢ lift.{w, max v u} (prod fun i ↦ #(c i)) = prod fun i ↦ lift.{w, v} ((fun i ↦ #(c i)) i)

Tactic:
simp only [← mk_pi, ← mk_uLift]

Goal state after:
ι : Type u
c : ι → Type v
⊢ #(ULift ((i : ι) → c i)) = #((i : ι) → ULift (c i))
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case left
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (a : ℕ), c a ≤ ωSup c

Tactic:
exact fun a ↦ le_ωSup c a

Goal state after:
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
le_antisymm_iff

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
c : Chain α
a : α
h : IsLUB (Set.range ⇑c) a
⊢ a ≤ ωSup c ∧ ωSup c ≤ a
Module: Mathlib.Order.OmegaCompletePartialOrder

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

Tactic:
exact fun a ↦ le_ωSup c a

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

Goal state before:
pp: case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ 0 ≤ 1

Tactic:
power_zero

Goal state after:
case pos
c : Cardinal.{u}
h : c = 0
⊢ 1 ≤ 1
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr
α : 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 : α
⊢ R a (if a ∈ s then f a else invFun g a)

Tactic:
split

Goal state after:
case inr.isTrue
α : 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 (f a)

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)
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a

Tactic:
simp [Cardinal.toNat_apply_of_aleph0_le h]

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 • a = 0 • b

Tactic:
repeat' rw [MulActionWithZero.zero_smul]

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ succ c = c + 1

Tactic:
hn,

Goal state after:
c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ succ ↑n = ↑n + 1
Module: Mathlib.Algebra.Module.Torsion.Free

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
r : R
m : M
inst✝¹ : IsTorsionFree R M
inst✝ : IsCancelMulZero R
⊢ r • m = 0 ↔ r = 0 ∨ m = 0

Tactic:
by
  obtain rfl | hr := eq_or_ne r 0 <;> simp [smul_eq_zero_iff_right, *]

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

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set (Submodule R M)
t : R
m : M
⊢ t • 0 ∈ ⨆ a, ↑a

Tactic:
simpa only [smul_zero] using zero_mem _

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

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
ι : Sort u_6
κ : ι → Sort u_7
inst✝¹ : FunLike F α β
inst✝ : CompleteLattice α
x : α × α
s : Set (α × α)
⊢ (sInf s).1 ⊓ (sInf s).2 = sInf ((fun x ↦ x.1 ⊓ x.2) '' s)

Tactic:
simp_rw [Prod.fst_sInf, Prod.snd_sInf, sInf_image, iInf_inf_eq]

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

Goal state before:
pp: R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomInvPair τ₁₂ τ₂₁
f : M →ₛₗ[τ₁₂] M₂
p : Submodule R M
⊢ (f.submoduleMap p).ker = comap p.subtype f.ker

Tactic:
ext; simp [Subtype.ext_iff]

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

Goal state before:
pp: R : Type u
M : Type v
N : Type w
inst✝³ : SMul R M
inst✝² : SMul M N
inst✝¹ : SMul R N
inst✝ : IsScalarTower R M N
x : R
y : M
z : ULift.{u_1, w} N
⊢ { down := (x • y) • z.down } = { down := x • y • z.down }

Tactic:
rw [smul_assoc]

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

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

Tactic:
Int.cast_natCast,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ ↑n * (x✝¹ * x✝) = ↑n * x✝¹ * x✝
Module: Mathlib.Algebra.Ring.Center

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

Tactic:
Int.cast_natCast,

Goal state after:
M : Type u_1
inst✝ : NonAssocRing M
n✝ : ℤ
x✝¹ x✝ : M
n : ℕ
⊢ x✝¹ * x✝ * ↑n = x✝¹ * (x✝ * ↑n)
Module: Mathlib.Algebra.Ring.Subring.Basic

Goal state before:
pp: R : Type u
S : Type v
T : Type w
inst✝² : NonAssocRing R
inst✝¹ : NonAssocRing S
inst✝ : NonAssocRing T
g : S →+* T
f : R →+* S
⊢ Subring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : Subring R).map_map g f

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: case left
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * a = 0
⊢ x * (a * b) = 0

pp: case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0

Tactic:
· rw [← mul_assoc, h', zero_mul]

Goal state after:
case right
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a b : M₀
h : a * b ∈ M₀⁰
x : M₀
h' : x * b = 0
⊢ x * (a * b) = 0
Module: Mathlib.Algebra.GroupWithZero.NonZeroDivisors

Goal state before:
pp: M₀✝ : ?m.1
M₀ : Type u_1
inst✝ : CommMonoidWithZero M₀
a : M₀
⊢ ∀ (x y : ↥(Associates M₀)⁰),
    (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
            ⋯).toFun
        (x * y) =
      (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          x *
        (Equiv.subtypeQuotientEquivQuotientSubtype (fun x ↦ x ∈ M₀⁰) (fun x ↦ x ∈ (Quotient (Associated.setoid M₀))⁰) ⋯
              ⋯).toFun
          y

Tactic:
by simp [Quotient.forall, Associates.mk_mul_mk]

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

Goal state before:
pp: case mp
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
h : f.ker ≤ p
⊢ ∃ y ∈ f.range, ⇑f ⁻¹' {y} ⊆ ↑p

Tactic:
use 0

Goal state after:
case h
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
h : f.ker ≤ p
⊢ 0 ∈ f.range ∧ ⇑f ⁻¹' {0} ⊆ ↑p
Module: Mathlib.Algebra.Module.Submodule.Range

Goal state before:
pp: 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
hx' : x ∈ p
⊢ z + x ∈ p

Tactic:
apply h₂

Goal state after:
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
hx' : x ∈ p
⊢ z + x ∈ ⇑f ⁻¹' {y}
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsWeakUpperModularLattice α
a b : α
⊢ b ⊓ a ⋖ a → b ⊓ a ⋖ b → b ⋖ b ⊔ a

Tactic:
exact fun ha hb => covBy_sup_of_inf_covBy_of_inf_covBy_left hb ha

Goal state after:
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ a ⊔ b

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsUpperModularLattice α
a b : α
⊢ a ⊓ b ⋖ b → a ⋖ b ⊔ a
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ z ⊓ (x✝ ⊔ y) = x✝ ⊔ y ⊓ z

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z : αᵒᵈ
xz : x✝ ≤ z
⊢ z ⊓ (y ⊔ x✝) = x✝ ⊔ y ⊓ z
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ a ⊓ (↑x ⊔ b) = ↑x

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y z a b : α
x : ↑(Icc (a ⊓ b) a)
⊢ a ⊓ (b ⊔ ↑x) = ↑x
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (b ⊔ ↑x) ≤ ↑y

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x✝ y✝ z a b : α
x y : ↑(Icc (a ⊓ b) a)
h : ↑x ⊔ b ≤ ↑y ⊔ b
⊢ a ⊓ (↑x ⊔ b) ≤ ↑y
Module: Mathlib.Order.ModularLattice

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ a ⊓ (↑c ⊔ b) = ↑c

Tactic:
sup_comm,

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : IsModularLattice α
x y z a b : α
c : ↑(Ioo (a ⊓ b) a)
⊢ a ⊓ (b ⊔ ↑c) = ↑c