mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Group.Commute.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
a b : M
h : Commute a b
n : ℕ
⊢ (a * b) ^ (n + 1) = a ^ (n + 1) * b ^ (n + 1)

Tactic:
simp only [pow_succ', h.mul_pow n, ← mul_assoc, (h.pow_left n).right_comm]

Goal state after:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ c = c'

Tactic:
classical have := inj (a₁ := fun _ ↦ c) (a₂ := (if · = b₀ then c' else c)) ?_

Goal state after:
case refine_2
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
this : (fun x ↦ c) = fun x ↦ if x = b₀ then c' else c
⊢ c = c'

case refine_1
α : Sort u_1
β : Sort u_2
f : α → β
γ : Type u_4
inst✝ : Nontrivial γ
not_surj : ¬Surjective f
inj : Injective fun g ↦ g ∘ f
c c' : γ
b₀ : β
hb : ¬∃ a, f a = b₀
⊢ ((fun g ↦ g ∘ f) fun x ↦ c) = (fun g ↦ g ∘ f) fun x ↦ if x = b₀ then c' else c
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Sort u_1
β : Sort u_2
f : α → β
hf : Bijective f
p : β → Prop
x✝ : ∃! y, p y
y : β
hpy : (fun y ↦ p y) y
hy : ∀ (y_1 : β), (fun y ↦ p y) y_1 → y_1 = y
x : α
hx : f x = y
⊢ (fun x ↦ p (f x)) x

Tactic:
by simpa [hx]

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

Goal state before:
pp: F : Sort u_1
α : Sort u_2
β : Sort u_3
i : FunLike F α β
P : Prop
inst✝ : Decidable P
f : P → F
g : ¬P → F
x : α
⊢ (if h : P then f h else g h) x = if h : P then (f h) x else (g h) x

Tactic:
by
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: case refine_2
α : Type u_1
r : α → α → Prop
x y : α
h : ReflTransGen r x y
⊢ TransGen (ReflGen r) x y

Tactic:
obtain (rfl | h) := reflTransGen_iff_eq_or_transGen.mp h
    · exact .single .refl
    · exact h.mono (fun _ _ ↦ .single) x y

Goal state after:
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β✝ : Sort v
γ : Sort w
inst✝ : Unique α
β : α → Sort u_1
f : (i : α) → β i
⊢ uniqueElim ((fun f ↦ f default) f) = f

Tactic:
ext i; cases Unique.eq_default i; rfl

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

Goal state before:
pp: M : Type u_1
N : Type u_2
G : Type u_3
H : Type u_4
α : Type u_5
β : Type u_6
γ : Type u_7
δ : Type u_8
inst✝³ : SMul M α
inst✝² : SMul M β
inst✝¹ : SMul α β
inst✝ : IsScalarTower M α β
g : N → M
this✝ : SMul N α
this : SMul N β
⊢ Sort ?u.25

Tactic:
exact IsScalarTower N α β

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

Goal state before:
pp: G : Type u_3
α : Type u_5
inst✝¹ : Group G
inst✝ : MulAction G α
g : G
a b : α
h : a = g⁻¹ • b
⊢ g • a = b

Tactic:
by rw [h, smul_inv_smul]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
f : α → γ
g : β → δ
h : Surjective (Sum.map f g)
c : γ
⊢ ∃ a, f a = c

Tactic:
obtain ⟨a | b, h⟩ := h (inl c)
        · exact ⟨a, inl_injective h⟩
        · cases h

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

Goal state before:
pp: case negSucc.zero
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
⊢ (casesOn -[0+1] f fun n ↦ g (n + 1)) < casesOn (-[0+1] + 1) f fun n ↦ g (n + 1)

pp: case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)

Tactic:
· change g 1 < f 0
    rw [hf₀, ← hg₀]
    exact hg Nat.zero_lt_one

Goal state after:
case negSucc.succ
α : Type u
inst✝³ : Preorder α
inst✝² : Nonempty α
inst✝¹ : NoMinOrder α
inst✝ : NoMaxOrder α
inhabited_h : Inhabited α
f : ℕ → α
hf : StrictMono f
hf₀ : f 0 = default
g : ℕ → α
hg : StrictAnti g
hg₀ : g 0 = default
n : ℕ
⊢ (casesOn -[n + 1+1] f fun n ↦ g (n + 1)) < casesOn (-[n + 1+1] + 1) f fun n ↦ g (n + 1)
Module: Mathlib.Data.Set.Insert

Goal state before:
pp: α : Type u_1
s t : Set α
a : α
⊢ Disjoint (insert a s) t ↔ ¬a ∈ t ∧ Disjoint s t

Tactic:
by
  simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]

Goal state after:
Module: Mathlib.Order.Lattice

Goal state before:
pp: α : Type u
inst✝ : Lattice α
a b c : α
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

Tactic:
by
  refine ⟨fun h ↦ ?_, ?_⟩
  · obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)
    simpa using h
  · rintro ⟨rfl, rfl⟩
    exact ⟨inf_idem _, sup_idem _⟩

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

Goal state before:
pp: α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) \ a = ⊥

Tactic:
by rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

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

Goal state before:
pp: α : Type u_2
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇨ aᶜ = aᶜ

Tactic:
rw [← himp_bot, himp_himp, inf_idem]

Goal state after:
Module: Mathlib.Order.BooleanAlgebra.Set

Goal state before:
pp: α : Type u_1
s t : Set α
⊢ s \ t ∪ s ∩ t = s

Tactic:
rw [union_comm]
  exact sup_inf_sdiff _ _

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

Goal state before:
pp: α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊔ y \ z ⊓ y = x ⊓ y ⊔ y \ z

Tactic:
inf_sdiff_left

Goal state after:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊔ y \ z = x ⊓ y ⊔ y \ z
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
s : α ⊕' β
⊢ Sum.elim PSum.inl PSum.inr ((fun s ↦ PSum.casesOn s inl inr) s) = s

Tactic:
cases s <;> rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α : Type ?u.17
β : Type ?u.16
s : α ⊕ β
⊢ (fun s ↦ PSum.casesOn s inl inr) (Sum.elim PSum.inl PSum.inr s) = s

Tactic:
cases s <;> rfl

Goal state after:
Module: Mathlib.Logic.Equiv.Sum

Goal state before:
pp: α✝ : Sort u_1
α₁ : Sort u_2
α₂ : Sort u_3
β✝ : Sort u_4
β₁ : Sort u_5
β₂ : Sort u_6
γ : Sort u_7
δ : Sort u_8
α β : Type ?u.15
s : α ⊕ β
⊢ (fun s ↦
        match s with
        | ⟨false, a⟩ => inl a
        | ⟨true, b⟩ => inr b)
      ((fun s ↦ Sum.elim (fun x ↦ ⟨false, x⟩) (fun x ↦ ⟨true, x⟩) s) s) =
    s

Tactic:
cases s <;> rfl

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

Goal state before:
pp: α : Type u
β : Type u_1
x y z : α
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : OrderTop α
a b : α
⊢ a \ b = a ⊓ ⊤ \ b

Tactic:
change _ = a ⊓ (⊤ \ b)

Goal state after:
α : Type u
β : Type u_1
x y z : α
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : OrderTop α
a b : α
⊢ a \ b = a ⊓ ⊤ \ b
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
s₁ s₂ : Set α
t : Set β
x : α
y : β
⊢ (x, y) ∈ (s₁ ∪ s₂) ×ˢ t ↔ (x, y) ∈ s₁ ×ˢ t ∪ s₂ ×ˢ t

Tactic:
simp [or_and_right]

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

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s ×ˢ t = s₁ ×ˢ t₁

Tactic:
prod_eq_prod_iff_of_nonempty h

Goal state after:
case inr
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : (s ×ˢ t).Nonempty
⊢ s = s₁ ∧ t = t₁ ∨ (s = ∅ ∨ t = ∅) ∧ (s₁ = ∅ ∨ t₁ = ∅) ↔ s = s₁ ∧ t = t₁
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ (f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i) ↔ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

Tactic:
refine ⟨fun h => ?_, ?_⟩

Goal state after:
case refine_1
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h✝ : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
h : f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂

case refine_2
ι : Type u_1
α : ι → Type u_2
p : ι → Prop
h : DecidablePred p
s : Set ι
t₁ t₂ : (i : ι) → Set (α i)
f : (i : ι) → α i
⊢ f ∈ {i | i ∈ s ∧ p i}.pi t₁ ∩ {i | i ∈ s ∧ ¬p i}.pi t₂ → f ∈ s.pi fun i ↦ if p i then t₁ i else t₂ i
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
⊢ e₂ (e₁ h) = h

Tactic:
← he₁₂

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β × γ
hf₁ : Surjective (Prod.fst ∘ f)
hf₂ : Surjective (Prod.snd ∘ f)
hf : ∀ (g₁ g₂ : α), (f g₁).1 = (f g₂).1 ↔ (f g₁).2 = (f g₂).2
e₁ : β → γ
he₁ : range f = graphOn e₁ univ
e₂ : γ → β
he₂ : range (⇑(Equiv.prodComm β γ) ∘ f) = graphOn e₂ univ
he₁₂ : ∀ (h : β) (i : γ), e₁ h = i ↔ e₂ i = h
h : β
⊢ e₁ h = e₁ h
Module: Mathlib.Algebra.Group.Hom.Defs

Goal state before:
pp: M : Type u_4
N : Type u_5
inst✝¹ : Mul M
inst✝ : Mul N
f : M →ₙ* N
is_surj : Surjective ⇑f
is_comm : IsMulCommutative M
a b : N
⊢ a * b = b * a

Tactic:
by
    have ⟨a', ha'⟩ := is_surj a
    have ⟨b', hb'⟩ := is_surj b
    simp [← ha', ← hb', ← map_mul, mul_comm']

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

Goal state before:
pp: case h₂
α : Type u_1
β : Type u_2
s s₁ : Set α
f : α → β
f' : β → α
hf : LeftInvOn f' f s
⊢ f' ⁻¹' s₁ ∩ f '' s ⊆ f '' (s₁ ∩ s)

Tactic:
· rintro _ ⟨h₁, ⟨x, h, rfl⟩⟩
    exact mem_image_of_mem _ ⟨by rwa [← hf h], h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ e (e.symm b) ∈ t

Tactic:
rwa [apply_symm_apply]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (b * c) = a * c * b

Tactic:
mul_comm b,

Goal state after:
G : Type u_3
inst✝ : CommSemigroup G
a b c : G
⊢ a * (c * b) = a * c * b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ 1 / (1 / b) = b

Tactic:
one_div_one_div

Goal state after:
α : Type u_1
inst✝ : DivisionMonoid α
a b : α
h : 1 / a = 1 / b
⊢ b = b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: G : Type u_3
inst✝ : Group G
a : G
m n : ℤ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
by
  rw [← zpow_add, Int.add_comm, zpow_add]

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

Goal state before:
pp: G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b / d = a ↔ a * d = c * b

Tactic:
div_eq_iff_eq_mul'

Goal state after:
G : Type u_3
inst✝ : CommGroup G
a b c d : G
⊢ c * b = d * a ↔ a * d = c * b
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c : α
pab : p a b✝
pbc : p b✝ c
pac : p a c
b : α
⊢ ∀ {c : α}, r b c → p a b → p b c → p a c → f a c = f a b * f b c

Tactic:
c

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Monoid β
p r : α → α → Prop
inst✝¹ : Std.Total r
f : α → α → β
inst✝ : Std.Symm p
hf_swap : ∀ {a b : α}, p a b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a b → p b c → p a c → f a c = f a b * f b c
a b✝ c✝ : α
pab : p a b✝
pbc : p b✝ c✝
pac : p a c✝
b c : α
⊢ r b c → p a b → p b c → p a c → f a c = f a b * f b c
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case pab
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p a ∧ p b

pp: case pbc
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p b ∧ p c

pp: case pac
α : Type u_1
β : Type u_2
inst✝¹ : Monoid β
r : α → α → Prop
inst✝ : Std.Total r
f : α → α → β
p : α → Prop
hswap : ∀ {a b : α}, p a → p b → f a b * f b a = 1
hmul : ∀ {a b c : α}, r a b → r b c → p a → p b → p c → f a c = f a b * f b c
a b c : α
pa : p a
pb : p b
pc : p c
this : Std.Symm fun x1 x2 ↦ p x1 ∧ p x2
⊢ p a ∧ p c

Tactic:
exacts [⟨pa, pb⟩, ⟨pb, pc⟩, ⟨pa, pc⟩]

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

Goal state before:
pp: α : Type u
inst✝ : DivisionMonoid α
a b c : α
h : IsUnit c
⊢ a / c = b / c ↔ a = b

Tactic:
by
  simp only [div_eq_mul_inv]
  exact Units.mul_left_inj h.inv.unit'

Goal state after:
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : AddMonoidWithOne R
P : Prop
inst✝ : Decidable P
m n : ℕ
⊢ ↑(if P then m else n) = if P then ↑m else ↑n

Tactic:
by
  split_ifs <;> rfl

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

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x * x_1) y = (fun x_1 ↦ x * x_1) z
⊢ y = z

Tactic:
dsimp only at h

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : x * y = x * z
⊢ y = z
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : (fun x_1 ↦ x_1 * x) y = (fun x_1 ↦ x_1 * x) z
⊢ y = z

Tactic:
dsimp only at h

Goal state after:
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a b x✝ x : G₀
hx : x ≠ 0
y z : G₀
h : y * x = z * x
⊢ y = z
Module: Mathlib.Algebra.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]

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

Goal state before:
pp: M : Type u_1
A : Type u_7
inst✝¹ : AddGroup A
inst✝ : DistribSMul M A
r : M
x : A
⊢ r • -x + r • x = 0

Tactic:
by rw [← smul_add, neg_add_cancel, smul_zero]

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

Goal state before:
pp: α : Type u_1
inst✝ : CommSemigroup α
a b : α
⊢ (∃ c, b = c * a) → a ∣ b

Tactic:
by
    rintro ⟨c, rfl⟩
    exact ⟨c, mul_comm _ _⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Defs

Goal state before:
pp: M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b : N
⊢ ∀ {n₂ : N}, (fun x1 x2 ↦ x1 ≤ x2) b n₂ → (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a n₂)

Tactic:
c

Goal state after:
M : Type u_1
N : Type u_2
μ : M → N → N
inst✝ : PartialOrder N
h : Covariant M N μ fun x1 x2 ↦ x1 < x2
a : M
b c : N
⊢ (fun x1 x2 ↦ x1 ≤ x2) b c → (fun x1 x2 ↦ x1 ≤ x2) (μ a b) (μ a c)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Semiring α
a b : α
⊢ Odd a → Odd b → Odd (a * b)

Tactic:
by
  rintro ⟨a, rfl⟩ ⟨b, rfl⟩
  refine ⟨2 * a * b + b + a, ?_⟩
  rw [mul_add, add_mul, mul_one, ← add_assoc, one_mul, mul_assoc, ← mul_add, ← mul_add, ← mul_assoc,
    ← Nat.cast_two, ← Nat.cast_comm]

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

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)

Tactic:
exact ha.add_even hb.neg

Goal state after:
Module: Mathlib.Order.MinMax

Goal state before:
pp: α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a (min b c) = min (min a c) b

Tactic:
min_comm b,

Goal state after:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ min a (min c b) = min (min a c) b
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f 0 ≤ f a

Tactic:
le

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : PosMulMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ a
Module: Mathlib.Algebra.Order.GroupWithZero.Defs

Goal state before:
pp: α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ f 0 ≤ f a

Tactic:
le

Goal state after:
α : Type u_1
inst✝⁶ : Mul α
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : MulPosMono α
β : Type u_2
inst✝² : Zero β
inst✝¹ : Mul β
inst✝ : Preorder β
f : β → α
zero : f 0 = 0
mul : ∀ (x y : β), f (x * y) = f x * f y
le : ∀ {x y : β}, f x ≤ f y ↔ x ≤ y
a : β
ha : 0 ≤ a
b c : β
hbc : b ≤ c
⊢ 0 ≤ a
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d⁻¹ ≤ b * c⁻¹

Tactic:
mul_comm b,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftMono α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
⊢ a * d⁻¹ ≤ c⁻¹ * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < b * c⁻¹

Tactic:
mul_comm b,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a * d⁻¹ < c⁻¹ * b
Module: Mathlib.Algebra.Order.Group.Unbundled.Basic

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : Preorder α
inst✝ : MulLeftStrictMono α
a b c d : α
hab : a < b
hcd : c < d
⊢ a / d < b / c

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv, mul_comm b, mul_inv_lt_inv_mul_iff, mul_comm]
  exact mul_lt_mul_of_lt_of_lt hab hcd

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : b ≤ a * b
⊢ 1 * b ≤ a * b

Tactic:
simpa only [one_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LE α
inst✝ : MulRightReflectLE α
a b : α
h : a * b ≤ b
⊢ a * b ≤ 1 * b

Tactic:
simpa only [one_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : b < a * b
⊢ 1 * b < a * b

Tactic:
simpa only [one_mul]

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : MulRightReflectLT α
a b : α
h : a * b < b
⊢ a * b < 1 * b

Tactic:
simpa only [one_mul]

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : MulZeroClass α
inst✝ : PartialOrder α
h : CovariantClass α>0 α (fun x y ↦ ↑x * y) fun x1 x2 ↦ x1 ≤ x2
a : α
ha✝ : 0 ≤ a
b c : α
hbc : b ≤ c
ha : 0 < a
⊢ a * b ≤ a * c

Tactic:
· exact @CovariantClass.elim α>0 α (fun x y => x * y) (· ≤ ·) _ ⟨_, ha⟩ _ _ hbc

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝³ : MulZeroClass α
a b c d : α
inst✝² : PartialOrder α
inst✝¹ : PosMulStrictMono α
inst✝ : MulPosStrictMono α
hab✝ : a ≤ b
hcd : c ≤ d
b0 : 0 < b
c0 : 0 < c
h : a * c = b * d
hab : a < b
⊢ a * c < b * d

Tactic:
exact (mul_lt_mul_of_pos_right hab c0).trans_le (mul_le_mul_of_nonneg_left hcd b0.le)

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

Goal state before:
pp: case inr
G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb✝ : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
hb : 0 < b
⊢ a * b⁻¹ ≤ c

Tactic:
rwa [mul_inv_le_iff₀ hb]

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : MulPosReflectLT G₀
a b c : G₀
hb : 0 ≤ b
hc : 0 ≤ c
h : a ≤ c * b
⊢ a * b⁻¹ ≤ c

Tactic:
obtain rfl | hb := hb.eq_or_lt
  · simp [hc]
  · rwa [mul_inv_le_iff₀ hb]

Goal state after:
Module: Mathlib.Algebra.Order.Ring.Unbundled.Basic

Goal state before:
pp: case c0
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ a

pp: case b0
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ 0 ≤ max d b

pp: case h₁
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ b ≤ max d b

pp: case h₂
R : Type u
inst✝³ : CommSemiring R
inst✝² : LinearOrder R
a d : R
inst✝¹ : PosMulMono R
inst✝ : MulPosMono R
b c : R
ha : 0 ≤ a
hd : 0 ≤ d
⊢ a ≤ max c a

Tactic:
exacts [ha, hd.trans <| le_max_left d b, le_max_right d b, le_max_right c a]

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

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝³ : SemilatticeInf α
inst✝² : OrderBot α
inst✝¹ : SemilatticeInf β
inst✝ : OrderBot β
a b : α
f : α ≃o β
ha : Disjoint a b
⊢ Disjoint (f a) (f b)

Tactic:
by
  rw [disjoint_iff_inf_le, ← f.map_inf, ← f.map_bot]
  exact f.monotone ha.le_bot

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
hx : 1 < x
n : ℤ
hn : 0 < n
⊢ 1 < x ^ n

Tactic:
lift n to ℕ using Int.le_of_lt hn

Goal state after:
G : Type u_2
inst✝² : DivInvMonoid G
inst✝¹ : Preorder G
inst✝ : MulLeftMono G
x : G
hx : 1 < x
n : ℕ
hn : 0 < ↑n
⊢ 1 < x ^ ↑n
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: s : ℕ
h : s ≠ 0
⊢ s.gcdB 0 = 0

Tactic:
obtain ⟨s, rfl⟩ := Nat.exists_eq_succ_of_ne_zero h
  simp [gcdB, xgcd, xgcdAux, Nat.strongRec_eq]

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

Goal state before:
pp: case zero
q n : ℕ
dvd : gcd 0 q ∣ n
le : pred 0 * q.pred ≤ n
⊢ ∃ a b, a * 0 + b * q = n

Tactic:
have ⟨b, eq⟩ := q.gcd_zero_left ▸ dvd
    exact ⟨0, b, by simpa [mul_comm, eq_comm] using eq⟩

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Unbundled.WithTop

Goal state before:
pp: α : Type u
β : Type v
inst✝² : Add α
w x✝ y✝ z✝ : WithTop α
a b : α
inst✝¹ : LE α
inst✝ : AddLeftMono α
x y z : WithTop α
⊢ (fun x1 x2 ↦ x1 ≤ x2) y z → (fun x1 x2 ↦ x1 ≤ x2) ((fun x1 x2 ↦ x1 + x2) x y) ((fun x1 x2 ↦ x1 + x2) x z)

Tactic:
cases x <;> cases y <;> cases z <;> simp [← coe_add]; simpa using fun _ ↦ by gcongr

Goal state after:
Module: Mathlib.Algebra.Order.Sub.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝⁵ : AddCommSemigroup α
inst✝⁴ : PartialOrder α
inst✝³ : ExistsAddOfLE α
inst✝² : AddLeftMono α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
h : c ≤ b
h2 : a - c < b - c
⊢ a < b

Tactic:
refine ((tsub_le_tsub_iff_right h).mp h2.le).lt_of_ne ?_
  rintro rfl
  exact h2.false

Goal state after: