mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case inl
n : Nat
h : n % 2 = 0
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa using

Goal state after:
case inl
n : Nat
h : n % 2 = 0
⊢ 2 * (n / 2) = n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case inr
n : Nat
h : n % 2 = 1
⊢ (bif decide (n % 2 = 1) then 2 * (n / 2) + 1 else 2 * (n / 2)) = n

Tactic:
simpa using

Goal state after:
case inr
n : Nat
h : n % 2 = 1
⊢ 2 * (n / 2) + 1 = n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
this : (n + 1 + 1) >>> 1 ≠ 0
⊢ (if (n + 1 + 1) >>> 1 = 0 then 0 else ((n + 1 + 1) >>> 1).log2.succ) <
    if n + 1 + 1 = 0 then 0 else (n + 1 + 1).log2.succ

Tactic:
simpa using

Goal state after:
case succ.succ
n : Nat
n0 : ¬n + 1 + 1 = 0
this : (n + 1 + 1) >>> 1 ≠ 0
⊢ ((n + 1 + 1) >>> 1).log2.succ < ((n + 1 + 1) >>> 1).log2.succ.succ
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Irrefl r
a : α
⊢ ¬Decidable.decide (r a a) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Irrefl r
a : α
⊢ ¬r a a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Refl r
a : α
⊢ Decidable.decide (r a a) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b c : α
inst✝¹ : DecidableRel r
inst✝ : Refl r
a : α
⊢ r a a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
a b c : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b c) = true → Decidable.decide (r a c) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c✝ : α
inst✝¹ : DecidableRel r
inst✝ : IsTrans α r
a b c : α
⊢ r a b → r b c → r a c
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Symm r
a b : α
⊢ Decidable.decide (r a b) = true → Decidable.decide (r b a) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Symm r
a b : α
⊢ r a b → r b a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r a b
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Antisymm r
a b : α
h₁ : Decidable.decide (r a b) = true
h₂ : Decidable.decide (r b a) = true
⊢ r b a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Asymm r
a b : α
⊢ Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Asymm r
a b : α
⊢ r a b → ¬r b a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Total r
a b : α
⊢ Decidable.decide (r a b) = true ∨ Decidable.decide (r b a) = true

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Total r
a b : α
⊢ r a b ∨ r b a
Module: Mathlib.Order.Defs.Unbundled

Goal state before:
pp: α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Trichotomous r
a b : α
⊢ ¬Decidable.decide (r a b) = true → ¬Decidable.decide (r b a) = true → a = b

Tactic:
simpa using

Goal state after:
α : Sort u_1
r : α → α → Prop
a✝ b✝ c : α
inst✝¹ : DecidableRel r
inst✝ : Trichotomous r
a b : α
⊢ ¬r a b → ¬r b a → a = b
Module: Mathlib.Logic.ExistsUnique

Goal state before:
pp: α : Sort u_1
a' : α
⊢ ∃! a, a' = a

Tactic:
by
  simp only [ExistsUnique, and_self, forall_eq', exists_eq']

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

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ x = z

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, y * z = 1
x y : M
h : x * y = 1
z : M
hz : y * z = 1
⊢ x = z
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y = z

Tactic:
simpa using

Goal state after:
M : Type u_2
inst✝ : Monoid M
ex : ∀ (x y : M), x * y = 1 → ∃ z, z * x = 1
x y : M
h : x * y = 1
z : M
hz : z * x = 1
⊢ y = z
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ f a = f b

Tactic:
simpa using

Goal state after:
case pos
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : (a == b) = true
⊢ a = b
Module: Mathlib.Logic.Function.Defs

Goal state before:
pp: case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬f a = f b

Tactic:
simpa using

Goal state after:
case neg
α : Type u_1
β : Type u_2
inst✝³ : BEq α
inst✝² : LawfulBEq α
inst✝¹ : BEq β
inst✝ : LawfulBEq β
f : α → β
I : Injective f
a b : α
h : ¬(a == b) = true
⊢ ¬a = b
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True

Tactic:
simpa using

Goal state after:
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : h₁
⊢ p True
Module: Mathlib.Logic.Basic

Goal state before:
pp: p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False

Tactic:
simpa using

Goal state after:
p : Prop → Prop
x✝ : ∃ h, p h
h₁ : Prop
h₂ : p h₁
H : ¬h₁
⊢ p False
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: 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'

Tactic:
simpa using

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'
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y

Tactic:
simpa using

Goal state after:
case refine_2
ι : Sort u_1
α : ι → Sort u_2
β : ι → Sort u_3
inst✝ : ∀ (i : ι), Nonempty (α i)
f : (i : ι) → α i → β i
i : ι
x y : α i
hxy : f i x = f i y
this : Inhabited ((i : ι) → α i)
h : update default i x = update default i y
⊢ x = y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r✝ : α → β → Prop
f✝ : α → γ
g : β → δ
c : γ
d : δ
r : α → α → Prop
inst✝ : Std.Symm r
f : α → β
x✝¹ x✝ : β
⊢ Relation.Map r f f x✝¹ x✝ → Relation.Map r f f x✝ x✝¹

Tactic:
rintro ⟨x, y, hxy, rfl, rfl⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ε : Type u_5
ζ : Type u_6
r✝ : α → β → Prop
f✝ : α → γ
g : β → δ
c : γ
d : δ
r : α → α → Prop
inst✝ : Std.Symm r
f : α → β
x y : α
hxy : r x y
⊢ Relation.Map r f f (f y) (f x)
Module: Mathlib.Logic.Relation

Goal state before:
pp: case mpr.inr
α : Type u_1
r : α → α → Prop
a b c : α
hac : r a c
hcb : ReflTransGen r c b
⊢ ReflTransGen r a b

Tactic:
exact head hac hcb

Goal state after:
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
x y : α
⊢ ReflGen r x y ↔ r x y

Tactic:
simpa using

Goal state after:
α : Type u_1
r : α → α → Prop
inst✝ : Std.Refl r
x y : α
⊢ y = x → r x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : Std.Refl r'
h : r ≤ r'
⊢ ReflGen r ≤ r'

Tactic:
simpa using

Goal state after:
α : Type u_1
r r' : α → α → Prop
inst✝ : Std.Refl r'
h : r ≤ r'
⊢ ReflGen r ≤ r'
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
hab : TransGen r i✝¹ i✝
⊢ (TransGen p on f) i✝¹ i✝

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (TransGen p on f)
i✝¹ i✝ : α
hab : TransGen r i✝¹ i✝
⊢ (TransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝ : IsTrans α r'
h : r ≤ r'
⊢ TransGen r ≤ r'

Tactic:
simpa using

Goal state after:
α : Type u_1
r r' : α → α → Prop
inst✝ : IsTrans α r'
h : r ≤ r'
⊢ TransGen r ≤ r'
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
hab : ReflTransGen r i✝¹ i✝
⊢ (ReflTransGen p on f) i✝¹ i✝

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
r : α → α → Prop
p : β → β → Prop
f : α → β
h : r ≤ (ReflTransGen p on f)
i✝¹ i✝ : α
hab : ReflTransGen r i✝¹ i✝
⊢ (ReflTransGen p on f) i✝¹ i✝
Module: Mathlib.Logic.Relation

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

Tactic:
simpa using

Goal state after:
case refine_1
α : Type u_1
r : α → α → Prop
x y : α
h : TransGen (ReflGen r) x y
⊢ ReflTransGen r x y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
r r' : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
h : r' ≤ r
⊢ ReflTransGen r' ≤ r

Tactic:
simpa using

Goal state after:
α : Type u_1
r r' : α → α → Prop
inst✝¹ : Std.Refl r
inst✝ : IsTrans α r
h : r' ≤ r
⊢ ReflTransGen r' ≤ r
Module: Mathlib.Logic.Function.Iterate

Goal state before:
pp: α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id^[n] ∘ id = id

Tactic:
ihn,

Goal state after:
α : Type u
n✝ n : ℕ
ihn : id^[n] = id
⊢ id ∘ id = id
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h : ∀ (a : α), q (e a)
a : β
⊢ q a

Tactic:
simpa using

Goal state after:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
h : ∀ (a : α), q (e a)
a : β
⊢ q a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝ : ∃ b, q b
a : β
h : q a
⊢ q (e (e.symm a))

Tactic:
simpa using

Goal state after:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
x✝ : ∃ b, q b
a : β
h : q a
⊢ q a
Module: Mathlib.Logic.Equiv.Defs

Goal state before:
pp: α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α),
    ((fun a ↦ q (e a)) a ∧ ∀ (y : α), (fun a ↦ q (e a)) y → y = a) ↔
      (fun b ↦ q b) (e a) ∧ ∀ (y : β), (fun b ↦ q b) y → y = e a

Tactic:
simpa using

Goal state after:
α : Sort u
β : Sort v
q : β → Prop
e : α ≃ β
⊢ ∀ (a : α), q (e a) → ((∀ (y : α), q (e y) → y = a) ↔ ∀ (y : β), q y → y = e a)
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝ : MulOneClass R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsRightCancelMul R
r₁ r₂ : R
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsLeftCancelMul R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂

Tactic:
simpa using

Goal state after:
M : Type u_1
G : Type u_2
α : Type u_3
R : Type u_4
inst✝¹ : Mul R
inst✝ : IsLeftCancelMul R
r₁ r₂ : Rᵐᵒᵖ
h : ∀ (a : R), r₁ • a = r₂ • a
⊢ r₁ = r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_1
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
· simp only at hr
    rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]

Goal state after:
case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r ↦ r • 1) r₁ = (fun r ↦ r • 1) r₂

Tactic:
simpa using

Goal state after:
case refine_2
R : Type u_4
A : Type u_5
inst✝² : MulOneClass A
inst✝¹ : SMul R A
inst✝ : IsScalarTower R A A
h : Injective fun r ↦ r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ r₁ • 1 = r₂ • 1
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), (a₂⁻¹ * a₁) • a = a

Tactic:
simpa using

Goal state after:
G : Type u_2
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
h : ∀ (g : G), (∀ (a : α), g • a = a) → g = 1
a₁ a₂ : G
h' : ∀ (a : α), a₁ • a = a₂ • a
⊢ ∀ (a : α), a₁ • a = a₂ • a
Module: Mathlib.Algebra.Group.Action.Faithful

Goal state before:
pp: R : Type u_4
S : Type u_5
T : Type u_6
inst✝¹⁰ : Monoid S
inst✝⁹ : MulOneClass T
inst✝⁸ : SMul R S
inst✝⁷ : IsScalarTower R S S
inst✝⁶ : MulAction S T
inst✝⁵ : IsScalarTower S T T
inst✝⁴ : SMul R T
inst✝³ : IsScalarTower R T T
inst✝² : IsScalarTower R S T
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S T
⊢ FaithfulSMul R T

Tactic:
simpa using

Goal state after:
R : Type u_4
S : Type u_5
T : Type u_6
inst✝¹⁰ : Monoid S
inst✝⁹ : MulOneClass T
inst✝⁸ : SMul R S
inst✝⁷ : IsScalarTower R S S
inst✝⁶ : MulAction S T
inst✝⁵ : IsScalarTower S T T
inst✝⁴ : SMul R T
inst✝³ : IsScalarTower R T T
inst✝² : IsScalarTower R S T
inst✝¹ : FaithfulSMul R S
inst✝ : FaithfulSMul S T
⊢ Injective fun r ↦ r • 1
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy x (r • a) (r • b)
⊢ SemiconjBy x a b

Tactic:
simpa using

Goal state after:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy x (r • a) (r • b)
⊢ SemiconjBy x a b
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b

Tactic:
simpa using

Goal state after:
G : Type u_3
H : Type u_4
inst✝⁴ : Group G
inst✝³ : Mul H
inst✝² : MulAction G H
inst✝¹ : SMulCommClass G H H
inst✝ : IsScalarTower G H H
a b x : H
r : G
h : SemiconjBy (r • x) a b
⊢ SemiconjBy x a b
Module: Mathlib.Data.Sum.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b

Tactic:
simpa using

Goal state after:
α : Type u
β : Type v
γ : Sort u_3
f : α → γ
g₁ g₂ : β → γ
hg : Sum.elim f g₁ = Sum.elim f g₂
b : β
⊢ g₁ b = g₂ b
Module: Mathlib.Algebra.Group.Action.Defs

Goal state before:
pp: M : Type u_9
N : Type u_10
P : Type u_11
Q : Type u_12
inst✝⁹ : SMul M N
inst✝⁸ : SMul M P
inst✝⁷ : SMul M Q
inst✝⁶ : SMul P Q
inst✝⁵ : Monoid N
inst✝⁴ : MulAction N P
inst✝³ : MulAction N Q
inst✝² : IsScalarTower M N P
inst✝¹ : IsScalarTower M N Q
inst✝ : IsScalarTower M P Q
h : Surjective fun m ↦ m • 1
n : N
p : P
q : Q
⊢ (n • p) • q = n • p • q

Tactic:
by obtain ⟨m, rfl⟩ := h n; simp_rw [smul_one_smul, smul_assoc]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : One β
inst✝ : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f = 1 ↔ f = 1

Tactic:
simpa using

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝¹ : One β
inst✝ : One γ
f : α → β
g : β → γ
hg : Injective g
hg0 : g 1 = 1
⊢ g ∘ f = 1 ↔ f = 1
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂

Tactic:
simpa using

Goal state after:
α : Type u_5
β : Type u_6
a : α
b₁ b₂ : β
h : (a, b₁) = (a, b₂)
⊢ b₁ = b₂
Module: Mathlib.Data.Prod.Basic

Goal state before:
pp: α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂
⊢ b₁ = b₂

Tactic:
simpa using

Goal state after:
α : Type u_5
β : Type u_6
b : β
b₁ b₂ : α
h : (fun a ↦ (a, b)) b₁ = (fun a ↦ (a, b)) b₂
⊢ b₁ = b₂
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ a ≤ b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.gt ↔ a ≤ b

Tactic:
simpa using

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b < a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ Ordering.lt ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using

Goal state after:
case lt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.lt
⊢ a < b
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ Ordering.eq ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using

Goal state after:
case eq
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.eq
⊢ b ≤ a
Module: Mathlib.Order.Defs.LinearOrder

Goal state before:
pp: case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ Ordering.gt ≠ Ordering.lt ↔ b ≤ a

Tactic:
simpa using

Goal state after:
case gt
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : compare a b = Ordering.gt
⊢ b ≤ a
Module: Mathlib.Order.Max

Goal state before:
pp: α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a

Tactic:
simpa using

Goal state after:
α : Type u_3
inst✝¹ : LinearOrder α
inst✝ : NoBotOrder α
a : α
⊢ ∃ b, b < a
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then a else b) = if a < b then a else b

Tactic:
simp only [not_le]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
inst✝ : LinearOrder α
a b : α
⊢ (if ¬b ≤ a then b else a) = if a < b then b else a

Tactic:
simp only [not_le]

Goal state after:
Module: Mathlib.Order.Basic

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ const β a < const β b ↔ a < b

Tactic:
simpa using

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Nonempty β
a b : α
⊢ a < b → a ≤ b
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: case self
a b c d e m n k : ℕ
p : ℕ → Prop
P : ℕ → Sort u_1
hP : P n
h : (k : ℕ) → k < n → n ≤ k → P (k + 1) → P k
⊢ P n

Tactic:
| self =>

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
δ : Type u_2
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : α → γ
g : β → δ
hf : StrictAnti f
hg : StrictAnti g
a b : α × β
⊢ a < b → Prod.map f g b < Prod.map f g a

Tactic:
simp only [Prod.lt_iff]
  exact Or.imp (And.imp hf.imp hg.antitone.imp) (And.imp hf.antitone.imp hg.imp)

Goal state after:
Module: Mathlib.Order.RelClasses

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Subsingleton α
⊢ ∀ (a b : α), r a b = emptyRelation a b

Tactic:
simpa using

Goal state after:
α : Type u
r : α → α → Prop
inst✝¹ : Std.Irrefl r
inst✝ : Subsingleton α
⊢ ∀ (i : α), ¬r i i
Module: Mathlib.Order.PropInstances

Goal state before:
pp: p q : Prop
⊢ p ≤ q ∨ q ≤ p

Tactic:
by_cases h : q <;> simp [h]

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

Goal state before:
pp: case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ (fun x ↦ if p x then f x else g x) x < (fun x ↦ if p x then f x else g x) y

Tactic:
simpa using

Goal state after:
case pos
α : Type u
β : Type v
inst✝² : Preorder α
inst✝¹ : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst✝ : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
hx : p x
⊢ f x < f y
Module: Mathlib.Order.Disjoint

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥

Tactic:
simpa using

Goal state after:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : OrderBot α
a b : α
h : Disjoint a b
x : α
h₁ : x ≤ a
h₂ : x ≤ b
⊢ x = ⊥