mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Function.Basic

Goal state before:
pp: α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x y : α
⊢ x ≠ y → ∃ f, f ∈ B ∧ f x ≠ f y

Tactic:
hne

Goal state after:
α : Type u_3
β : Type u_4
A B : Set (α → β)
hAB : A ⊆ B
hA : A.SeparatesPoints
x y : α
hne : x ≠ y
⊢ ∃ f, f ∈ B ∧ f x ≠ f y
Module: Mathlib.Logic.Relation

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
inst✝ : Std.Refl r
f : α → β
hf : Surjective f
x : β
⊢ Relation.Map r f f x x

Tactic:
by
    obtain ⟨y, rfl⟩ := hf x
    exact ⟨y, y, refl y, rfl, rfl⟩

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

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

Tactic:
exact ⟨a, inl_injective h⟩

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

Goal state before:
pp: I : Type u
α : Type u_1
β : Type u_2
γ : Type u_3
f : I → Type v₁
g : I → Type v₂
h : I → Type v₃
x y : (i : I) → f i
i : I
inst✝ : (i : I) → DivInvMonoid (f i)
⊢ ∀ (a b : (i : I) → f i), a / b = a * b⁻¹

Tactic:
intros; ext; exact div_eq_mul_inv _ _

Goal state after:
Module: Mathlib.Data.Nat.Init

Goal state before:
pp: a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P (lo + (x - lo))
⊢ P x

Tactic:
Nat.add_sub_cancel' hl

Goal state after:
a b c d e m n k : ℕ
p : ℕ → Prop
lo hi : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
al : ∀ (x : ℕ), x < hi - lo → P (lo + x)
x : ℕ
hl : lo ≤ x
hh : x < hi
this : P x
⊢ P x
Module: Mathlib.Tactic.Lift

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
⊢ ∀ (x : α × γ), condβα x.fst ∧ condδγ x.snd → ∃ y, map coeβα coeδγ y = x

Tactic:
rintro ⟨x, y⟩ ⟨hx, hy⟩

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
coeβα : β → α
condβα : α → Prop
coeδγ : δ → γ
condδγ : γ → Prop
inst✝¹ : CanLift α β coeβα condβα
inst✝ : CanLift γ δ coeδγ condδγ
x : α
y : γ
hx : condβα (x, y).fst
hy : condδγ (x, y).snd
⊢ ∃ y_1, map coeβα coeδγ y_1 = (x, y)
Module: Mathlib.Control.EquivFunctor

Goal state before:
pp: f : Type u₀ → Type u₁
inst✝¹ : Applicative f
inst✝ : LawfulApplicative f
α β : Type u₀
h : ∀ (γ : Type u₀), Injective pure
e₁ e₂ : α ≃ β
H : mapEquiv f e₁ = mapEquiv f e₂
x : α
⊢ pure (e₁ x) = pure (e₂ x)

Tactic:
by simpa [EquivFunctor.map] using Equiv.congr_fun H (pure x)

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.18
β : Type ?u.17
γ : Type ?u.15
⊢ RightInverse (Sum.elim (inl ∘ inl) (Sum.elim (inl ∘ inr) inr)) (Sum.elim (Sum.elim inl (inr ∘ inl)) (inr ∘ inr))

Tactic:
rintro (_ | ⟨_ | _⟩) <;> rfl

Goal state after:
Module: Mathlib.Order.SymmDiff

Goal state before:
pp: α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c \ ⊥

Tactic:
sdiff_bot

Goal state after:
α : Type u_2
inst✝ : BooleanAlgebra α
a b c : α
h : Disjoint a b
⊢ c ≤ c
Module: Mathlib.Data.Set.Prod

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ True ∧ t = t₁

Tactic:
true_and,

Goal state after:
case mp
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s.Nonempty ∧ t.Nonempty
heq : s ×ˢ t = s₁ ×ˢ t₁
h₁ : s₁.Nonempty ∧ t₁.Nonempty
⊢ t = t₁
Module: Mathlib.Data.Set.Prod

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

Tactic:
true_and,

Goal state after:
case inl
α : Type u_1
β : Type u_2
s s₁ : Set α
t t₁ : Set β
h : s ×ˢ t = ∅
⊢ s = s₁ ∧ t = t₁ ∨ s₁ = ∅ ∨ t₁ = ∅ ↔ s₁ = ∅ ∨ t₁ = ∅
Module: Mathlib.Data.Set.Function

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β
s t u : Set α
hf : InjOn f u
hs : s ⊆ u
ht : t ⊆ u
x : β
y : α
ys : y ∈ s
hy : f y = x
z : α
zt : y ∈ t
hz : f z = x
this : y = z
⊢ x ∈ f '' (s ∩ t)

Tactic:
exact ⟨y, ⟨ys, zt⟩, hy⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
a : α
ha : a ∈ s
hb : f a ∈ t
h : p (f a)
⊢ ∃ a, a ∈ s ∧ p (f a)

Tactic:
exact ⟨a, ha, h⟩

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
p : β → Prop
hf : BijOn f s t
⊢ (∃ b, b ∈ t ∧ p b) → ∃ a, a ∈ s ∧ p (f a)

Tactic:
rintro ⟨b, hb, h⟩; obtain ⟨a, ha, rfl⟩ := hf.surjOn hb; exact ⟨a, ha, h⟩

Goal state after:
Module: Mathlib.Data.Int.Init

Goal state before:
pp: m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ Int.leInductionDown base pred (n - 1) ⋯ = pred n hnm (Int.leInductionDown base pred n hnm)

Tactic:
rw [Int.leInductionDown, inductionOn'_sub_one hnm]

Goal state after:
m : ℤ
motive : (n : ℤ) → n ≤ m → Sort u_1
base : motive m ⋯
pred : (n : ℤ) → (hnm : n ≤ m) → motive n hnm → motive (n - 1) ⋯
n : ℤ
hnm : n ≤ m
⊢ pred n hnm
      (Int.inductionOn' (motive := fun x ↦ (hnm : x ≤ m) → motive x hnm) n m (fun x ↦ base) (fun x x_1 x_2 x_3 ↦ ⋯.elim)
        (fun k hle ih x ↦ pred k hle (ih hle)) hnm) =
    pred n hnm (Int.leInductionDown base pred n hnm)
Module: Mathlib.Algebra.Group.Basic

Goal state before:
pp: case mp
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ a = 1 → b = 1

Tactic:
rintro rfl; simpa using h

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

Goal state before:
pp: case mpr
M : Type u_4
inst✝ : MulOneClass M
a b : M
h : a * b = 1
⊢ b = 1 → a = 1

Tactic:
rintro rfl; simpa using h

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

Goal state before:
pp: α : Type u_1
inst✝ : MulOne α
⊢ (∀ {a b : αᵐᵒᵖ}, a * b = 1 → b * a = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1

Tactic:
← opEquiv.forall_congr_right

Goal state after:
α : Type u_1
inst✝ : MulOne α
⊢ (∀ (a a_1 : α), opEquiv a * opEquiv a_1 = 1 → opEquiv a_1 * opEquiv a = 1) ↔ ∀ {a b : α}, a * b = 1 → b * a = 1
Module: Mathlib.Algebra.Group.Basic

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

Tactic:
by
  rw [mul_left_comm, div_mul_cancel, mul_comm]

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

Goal state before:
pp: α : Type u
inst✝ : Monoid α
a : α
b : αˣ
⊢ a * ↑b * ↑b⁻¹ = a

Tactic:
rw [mul_assoc, mul_inv, mul_one]

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

Goal state before:
pp: n : ℕ
S : Type u_5
inst✝ : MonoidWithZero S
x : S
hx : IsNilpotent x
hn : n ≠ 0
⊢ IsNilpotent (x ^ n)

Tactic:
by
  cases n with
  | zero => contradiction
  | succ => exact IsNilpotent.pow_succ _ hx

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

Goal state before:
pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b x a : G₀
h : ¬a = 0
⊢ a⁻¹⁻¹ = a

Tactic:
· exact left_inv_eq_right_inv (inv_mul_cancel₀ <| inv_ne_zero h) (inv_mul_cancel₀ h)

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

Goal state before:
pp: case pos
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

pp: case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹

Tactic:
· simp [ha]

Goal state after:
case neg
M₀ : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
a✝ b✝ x a b : G₀
ha : ¬a = 0
⊢ (a * b)⁻¹ = b⁻¹ * a⁻¹
Module: Mathlib.Data.Nat.Cast.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(1 + 2 * ((k + 1) / 2))

Tactic:
Nat.add_comm 1,

Goal state after:
case neg
R : Type u_1
inst✝ : AddMonoidWithOne R
k : ℕ
hk : ∀ (m : ℕ), m < k + 1 → m.binCast = ↑m
h : ¬(k + 1) % 2 = 0
h1 : k.succ % 2 = 1
⊢ ↑((k + 1) / 2 + (k + 1) / 2) + 1 = ↑(2 * ((k + 1) / 2) + 1)
Module: Mathlib.Data.Int.Cast.Basic

Goal state before:
pp: R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m - ↑n.succ = ↑m + -↑(n + 1)

Tactic:
sub_eq_add_neg

Goal state after:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
⊢ ↑m + -↑n.succ = ↑m + -↑(n + 1)
Module: Mathlib.Data.List.TFAE

Goal state before:
pp: α : Type u_1
l : List (α → Prop)
H : ∀ (a : α), (map (fun p ↦ p a) l).TFAE
⊢ (map (fun p ↦ ∃ a, p a) l).TFAE

Tactic:
simp only [TFAE, List.forall_mem_map]
  intro p₁ hp₁ p₂ hp₂
  exact exists_congr fun a ↦ H a (p₁ a) (mem_map_of_mem hp₁)
    (p₂ a) (mem_map_of_mem hp₂)

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * -(1 / a) = -(b * (1 / a))

Tactic:
neg_mul_eq_mul_neg

Goal state after:
R : Type u_1
inst✝¹ : DivisionMonoid R
inst✝ : HasDistribNeg R
a b : R
⊢ b * -(1 / a) = b * -(1 / a)
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y + (f y * f x + f y * f y)) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← sub_sub,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y) - (f y * f x + f y * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y) - (f y * f x + f y * f y) = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← sub_sub,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y) - f y * f x - f y * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.Ring.Hom.Defs

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - (f x * f x + f x * f y) - f y * f x - f y * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y

Tactic:
← sub_sub,

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : CommRing α
inst✝¹ : IsDomain α
inst✝ : CommRing β
f : β →+ α
h : ∀ (x : β), f (x * x) = f x * f x
h_two : 2 ≠ 0
h_one : f 1 = 1
x y : β
hxy : f (x * y) + f y * f y + (f x * f x + f (y * x)) - f x * f x - f x * f y - f y * f x - f y * f y = 0
⊢ (↑f).toFun (x * y) = (↑f).toFun x * (↑f).toFun y
Module: Mathlib.Algebra.GroupWithZero.Semiconj

Goal state before:
pp: case pos
G₀ : Type u_1
inst✝ : GroupWithZero G₀
a x y : G₀
h : SemiconjBy a x y
ha : ¬a = 0
hx : x = 0
⊢ SemiconjBy a x⁻¹ y⁻¹

Tactic:
subst x
    simp only [SemiconjBy, mul_zero, @eq_comm _ _ (y * a), mul_eq_zero] at h
    simp [h.resolve_right ha]

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:
sub_eq_add_neg

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Even b
⊢ Odd (a + -b)
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Even a
hb : Odd b
⊢ Odd (a + -b)
Module: Mathlib.Algebra.Ring.Parity

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

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_2
inst✝ : Ring α
a b : α
ha : Odd a
hb : Odd b
⊢ Even (a + -b)
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: α : Type u_2
inst✝ : Ring α
a : α
⊢ Odd (a + 1 + 1) ↔ Odd a

Tactic:
odd_add_one,

Goal state after:
α : Type u_2
inst✝ : Ring α
a : α
⊢ Even (a + 1) ↔ Odd a
Module: Mathlib.Algebra.Ring.Parity

Goal state before:
pp: case inl
k : ℕ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k
    grind

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

Goal state before:
pp: case inr
k : ℕ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k
    grind

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

Goal state before:
pp: α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ c⁻¹ * a < b ↔ a < b * c

Tactic:
inv_mul_lt_iff_lt_mul,

Goal state after:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ a < c * b ↔ a < b * c
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ True ∧ c * d ≤ a * b ↔ a = c ∧ b = d

Tactic:
true_and,

Goal state after:
α : Type u_1
inst✝³ : Mul α
inst✝² : PartialOrder α
inst✝¹ : MulLeftStrictMono α
inst✝ : MulRightStrictMono α
a b c d : α
hac : a ≤ c
hbd : b ≤ d
this✝ : MulLeftMono α
this : MulRightMono α
⊢ c * d ≤ a * b ↔ a = c ∧ b = d
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosMono G₀
⊢ Contravariant { x // 0 < x } G₀ (fun x y ↦ y * ↑x) fun x1 x2 ↦ x1 ≤ x2

Tactic:
by
    rintro ⟨a, ha⟩ b c h
    simpa [ha.ne'] using mul_le_mul_of_nonneg_right h (inv_nonneg.2 ha.le)

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

Goal state before:
pp: G₀ : Type u_3
inst✝² : GroupWithZero G₀
inst✝¹ : PartialOrder G₀
inst✝ : PosMulReflectLT G₀
a b : G₀
ha : 0 < a
⊢ a⁻¹ < b ↔ 1 < a * b

Tactic:
by
  rw [← inv_mul_lt_iff₀ ha, mul_one]

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

Goal state before:
pp: case mp
R : Type u
inst✝⁶ : Semiring R
inst✝⁵ : LinearOrder R
inst✝⁴ : ExistsAddOfLE R
inst✝³ : PosMulStrictMono R
inst✝² : MulPosStrictMono R
inst✝¹ : AddLeftStrictMono R
inst✝ : AddLeftReflectLT R
a : R
⊢ 0 < a * a → a ≠ 0

Tactic:
rintro h rfl
    rw [mul_zero] at h
    exact h.false

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

Goal state before:
pp: G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : MulPosReflectLT G₀
a b c d : G₀
hac : a ≤ c
hdb : d < b
hc : 0 < c
hd : 0 < d
⊢ a / b < c / d

Tactic:
by
  rw [div_eq_mul_inv, div_eq_mul_inv]
  exact mul_lt_mul' hac ((inv_lt_inv₀ (hd.trans hdb) hd).2 hdb)
    (inv_nonneg.2 <| hd.le.trans hdb.le) hc

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

Goal state before:
pp: α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax (f x) ↔ IsMax x

Tactic:
refine ⟨f.strictMono.isMax_of_apply, ?_⟩

Goal state after:
α : Type u_6
β : Type u_7
inst✝¹ : Preorder α
inst✝ : Preorder β
f : α ≃o β
x : α
⊢ IsMax x → IsMax (f x)
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a b : ℤ
H : b ≠ 0
⊢ a % |b| < |b|

Tactic:
exact emod_lt_of_pos _ (abs_pos.2 H)

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Int

Goal state before:
pp: a : ℤ
n : ℕ
⊢ |a / ↑n| ≤ |a|

Tactic:
rw [abs_eq_natAbs, abs_eq_natAbs]

Goal state after:
a : ℤ
n : ℕ
⊢ ↑(a / ↑n).natAbs ≤ ↑a.natAbs
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: case inl
k : ℤ
⊢ ∃ k_1, Xor (k + k = 2 * k_1) (k + k = 2 * k_1 + 1)

Tactic:
use k
    grind

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

Goal state before:
pp: case inr
k : ℤ
⊢ ∃ k_1, Xor (2 * k + 1 = 2 * k_1) (2 * k + 1 = 2 * k_1 + 1)

Tactic:
use k
    grind

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

Goal state before:
pp: b p : ℕ
w : 0 < b
⊢ ↑(b ^ p - 1) = ↑b ^ p - 1

Tactic:
by
  have : 1 ≤ b ^ p := Nat.one_le_pow p b w
  norm_cast

Goal state after:
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: ι : Type u_2
α : ι → Type u_3
inst✝³ : (i : ι) → Group (α i)
f : (i : ι) → α i
inst✝² : (i : ι) → LinearOrder (α i)
inst✝¹ : ∀ (i : ι), MulLeftMono (α i)
inst✝ : ∀ (i : ι), MulRightMono (α i)
h : |f|ₘ = 1
i : ι
⊢ f i = 1 i

Tactic:
simpa using congr_fun h i

Goal state after:
Module: Mathlib.Data.Int.GCD

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
a : M
m n : ℕ
hm : a ^ m = 1
hn : a ^ n = 1
⊢ a ^ m.gcd n = 1

Tactic:
by
    obtain _ | m := m
    · simpa
    obtain ⟨y, rfl⟩ := IsUnit.of_pow_eq_one hm m.succ_ne_zero
    rw [← Units.val_pow_eq_pow_val, ← Units.val_one (α := M), ← zpow_natCast, ← Units.ext_iff] at *
    rw [Nat.gcd_eq_gcd_ab, zpow_add, zpow_mul, zpow_mul, hn, hm, one_zpow, one_zpow, one_mul]

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
inst✝¹ : Preorder α
x y : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), y ≤ ↑a → x ≤ ↑a) ↔ x ≤ y

Tactic:
obtain _ | y := y

Goal state after:
case none
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
⊢ (∀ (a : α), none ≤ ↑a → x ≤ ↑a) ↔ x ≤ none

case some
α : Type u_1
inst✝¹ : Preorder α
x : WithBot α
inst✝ : NoBotOrder α
y : α
⊢ (∀ (a : α), Option.some y ≤ ↑a → x ≤ ↑a) ↔ x ≤ Option.some y
Module: Mathlib.Algebra.Group.Invertible.Basic

Goal state before:
pp: R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
ifr : Invertible (f r)
⊢ f ⅟r = ⅟(f r)

Tactic:
obtain rfl : ifr = Invertible.map f r := Subsingleton.elim _ _

Goal state after:
R : Type u_1
S : Type u_2
F : Type u_3
inst✝⁴ : MulOneClass R
inst✝³ : Monoid S
inst✝² : FunLike F R S
inst✝¹ : MonoidHomClass F R S
f : F
r : R
inst✝ : Invertible r
⊢ f ⅟r = ⅟(f r)
Module: Mathlib.Algebra.Order.Ring.Basic

Goal state before:
pp: R : Type u_3
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
a b : R
inst✝ : ExistsAddOfLE R
ha : 0 ≤ a
hb : 0 ≤ b
n : ℕ
⊢ (a + b) ^ (n + 2) ≤ 2 ^ (n + 2 - 1) * (a ^ (n + 2) + b ^ (n + 2))

Tactic:
by
    rw [pow_succ]
    calc
      _ ≤ 2 ^ n * (a ^ (n + 1) + b ^ (n + 1)) * (a + b) :=
          mul_le_mul_of_nonneg_right (add_pow_le ha hb (n + 1)) <| add_nonneg ha hb
      _ = 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * b + b ^ (n + 1) * a)) := by
          rw [mul_assoc, mul_add, add_mul, add_mul, ← pow_succ, ← pow_succ, add_comm _ (b ^ _),
            add_add_add_comm, add_comm (_ * a)]
      _ ≤ 2 ^ n * (a ^ (n + 2) + b ^ (n + 2) + (a ^ (n + 1) * a + b ^ (n + 1) * b)) := by
        gcongr _ * (_ + _ + ?_)
        · exact pow_nonneg zero_le_two _
        obtain hab | hba := le_total a b
        · exact mul_add_mul_le_mul_add_mul (by gcongr) hab
        · exact mul_add_mul_le_mul_add_mul' (by gcongr) hba
      _ = _ := by simp only [← pow_succ, ← two_mul, ← mul_assoc]; rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ True ∧ True ∧ a = EquivLike.inv f a₁ * EquivLike.inv f a₂

Tactic:
true_and,

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁴ : Semigroup α
inst✝³ : Semigroup β
F : Type u_3
inst✝² : EquivLike F α β
inst✝¹ : MulEquivClass F α β
f : F
inst✝ : DecompositionMonoid β
a b c : α
h✝ : f a ∣ f b * f c
a₁ a₂ : β
h : a₁ ∣ f b ∧ a₂ ∣ f c ∧ f a = a₁ * a₂
⊢ a = EquivLike.inv f a₁ * EquivLike.inv f a₂
Module: Mathlib.Algebra.Ring.Divisibility.Basic

Goal state before:
pp: α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ b - c ↔ a ∣ c - b

Tactic:
← dvd_neg,

Goal state after:
α : Type u_1
inst✝ : NonUnitalRing α
a b c : α
⊢ a ∣ -(b - c) ↔ a ∣ c - b
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c + -(b / c) = (a - b) / c

Tactic:
← neg_div,

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ a / c + -b / c = (a - b) / c
Module: Mathlib.Algebra.Field.Basic

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ (a + -b) / c = (a - b) / c

Tactic:
sub_eq_add_neg

Goal state after:
K : Type u_1
inst✝ : DivisionRing K
a b c : K
⊢ (a + -b) / c = (a + -b) / c
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_1
β : Type u_2
e : α ≃ β
s : Set β
x✝ : α
⊢ x✝ ∈ ⇑e.symm '' s ↔ x✝ ∈ ⇑e ⁻¹' s

Tactic:
exact mem_image_iff_of_inverse e.right_inv e.left_inv

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

Goal state before:
pp: α : Type u_3
β : Type u_4
e : α ≃ β
s : Set α
t : Set β
⊢ ⇑e.symm.symm '' s ⊆ t ↔ ⇑e '' s ⊆ t

Tactic:
by rw [e.symm_symm]

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

Goal state before:
pp: α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf).symm ⟨f a, ⋯⟩ = a

Tactic:
apply (ofInjective f hf).injective

Goal state after:
α : Sort u_3
β : Type u_4
f : α → β
hf : Injective f
a : α
⊢ (ofInjective f hf) ((ofInjective f hf).symm ⟨f a, ⋯⟩) = (ofInjective f hf) a
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: case neg.refine_2
α : Type u_1
inst✝ : PartialOrder α
a b : α
s : Set α
ho : Ioo a b ⊆ s
hc : s ⊆ Icc a b
ha : a ∈ s
hb : ¬b ∈ s
⊢ Ico a b ⊆ s

Tactic:
rwa [← Ico_sdiff_left, sdiff_singleton_subset_iff, insert_eq_of_mem ha] at ho

Goal state after:
Module: Mathlib.Tactic.NormNum.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a - b) nc dc

Tactic:
sub_eq_add_neg

Goal state after:
α : Type u_1
inst✝ : Ring α
f : α → α → α
a b : α
na nb nc : ℤ
da db dc k : ℕ
hf : f = HSub.hSub
ra : IsRat a na da
rb : IsRat b nb db
h₁ : (na.mul ↑db).sub (nb.mul ↑da) = (↑k).mul nc
h₂ : da.mul db = k.mul dc
⊢ IsRat (a + -b) nc dc
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0 * ε
⊢ a ≤ 0

Tactic:
simp_rw [zero_mul] at h

Goal state after:
case inl
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
hb : 0 ≤ 0
h : ∀ (ε : α), 1 < ε → a ≤ 0
⊢ a ≤ 0
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop (l.length + 1 - 1) (a :: l) = [(a :: l).getLast h]

Tactic:
Nat.add_one_sub_one,

Goal state after:
case neg
α : Type u
a : α
l : List α
ih : ∀ (h : l ≠ []), drop (l.length - 1) l = [l.getLast h]
h : a :: l ≠ []
hl : ¬l = []
⊢ drop l.length (a :: l) = [(a :: l).getLast h]
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ a / c < b / c ↔ b < a

Tactic:
div_lt_iff_of_neg hc,

Goal state after:
α : Type u_2
inst✝³ : Field α
inst✝² : PartialOrder α
inst✝¹ : PosMulReflectLT α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : c < 0
⊢ b / c * c < a ↔ b < a