mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Ring.Defs

Goal state before:
pp: R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a * b = 0
⊢ a = 0 ∨ b = 0

Tactic:
contrapose! hab

Goal state after:
R : Type u
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : IsStrictOrderedRing R
inst✝ : ExistsAddOfLE R
a b : R
hab : a ≠ 0 ∧ b ≠ 0
⊢ a * b ≠ 0
Module: Mathlib.Algebra.Order.GroupWithZero.Basic

Goal state before:
pp: case inl
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : a < 1
⊢ Injective fun n ↦ a ^ n

pp: case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun n ↦ a ^ n

Tactic:
· exact (zpow_right_strictAnti₀ ha₀ ha₁).injective

Goal state after:
case inr
G₀ : Type u_3
inst✝³ : GroupWithZero G₀
inst✝² : LinearOrder G₀
a : G₀
inst✝¹ : PosMulStrictMono G₀
inst✝ : ZeroLEOneClass G₀
ha₀ : 0 < a
ha₁✝ : a ≠ 1
ha₁ : 1 < a
⊢ Injective fun n ↦ a ^ n
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ a = b

Tactic:
apply Std.Trichotomous.trichotomous (r := r) a b

Goal state after:
case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r a b

case refine_1.a
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
e : f a = f b
⊢ ¬r b a
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b)
⊢ r a b

Tactic:
refine Not.imp_symm (Std.Trichotomous.trichotomous a b · fun h' ↦ asymm (H _ _ h') h) ?_

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
inst✝¹ : Std.Trichotomous r
inst✝ : Std.Asymm s
f : α → β
H : ∀ (a b : α), r a b → s (f a) (f b)
this : Std.Irrefl s
a b : α
h : s ({ toFun := f, inj' := ⋯ } a) ({ toFun := f, inj' := ⋯ } b)
⊢ ¬a = b
Module: Mathlib.Order.RelIso.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
u : δ → δ → Prop
α₁ : Type ?u.35
α₂ : Type ?u.38
β₁ : Type ?u.34
β₂ : Type ?u.37
r₁ : α₁ → α₁ → Prop
r₂ : α₂ → α₂ → Prop
s₁ : β₁ → β₁ → Prop
s₂ : β₂ → β₂ → Prop
e₁ : r₁ ≃r s₁
e₂ : r₂ ≃r s₂
⊢ ∀ {a b : α₁ × α₂}, Prod.Lex s₁ s₂ ((e₁.prodCongr e₂.toEquiv) a) ((e₁.prodCongr e₂.toEquiv) b) ↔ Prod.Lex r₁ r₂ a b

Tactic:
simp [Prod.lex_def, e₁.map_rel_iff, e₂.map_rel_iff,
    e₁.injective.eq_iff]

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

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a✝ : α
⊢ cmp (f a✝) (f a✝) = Ordering.eq

Tactic:
cmp_self_eq_eq

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
a✝ : α
⊢ Ordering.eq = Ordering.eq
Module: Mathlib.Order.Hom.Basic

Goal state before:
pp: F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ cmp (g x✝) (g x✝) = Ordering.eq

Tactic:
cmp_self_eq_eq

Goal state after:
F : Type u_1
α✝ : Type u_2
β✝ : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α✝
inst✝² : Preorder β✝
α : Type ?u.13
β : Type ?u.15
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
g : β → α
h : ∀ (a : α) (b : β), cmp a (g b) = cmp (f a) b
gf : ∀ (a : α), a = g (f a)
x✝ : β
⊢ Ordering.eq = Ordering.eq
Module: Mathlib.Algebra.Order.Monoid.Unbundled.Pow

Goal state before:
pp: M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftMono M
inst✝ : MulRightMono M
a b c : M
h : a ^ 2 < b * c
⊢ a < max b c

Tactic:
simpa using min_lt_max_of_mul_lt_mul ((pow_two _).symm.trans_lt h)

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:
by simpa using congr_fun h i

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

Goal state before:
pp: n p q : ℕ
dvd : ∃ x y, ↑n = ↑(p + 1) * x + ↑(q + 1) * y
le : p * q ≤ n
a_n b_n : ℤ
eq : ↑n = ↑(p + 1) * a_n + ↑(q + 1) * b_n
a : ℤ := a_n % ↑q.succ
b : ℤ := b_n + a_n / ↑q.succ * ↑p.succ
this : a * ↑p.succ + b * ↑q.succ = ↑n
hb : b ≤ -1
ha : a_n % ↑q.succ < ↑(↑q.succ).natAbs
⊢ a * ↑p.succ + b * ↑q.succ ≤ ↑q * ↑p.succ + -1 * ↑q.succ

Tactic:
gcongr <;> lia

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a : WithZero α
hab : (map' f) a = ↑b
⊢ ∃ a, f a = b

Tactic:
induction a using WithZero.recZeroCoe <;>
    simp at hab

Goal state after:
case refine_1.coe
α : Type u_1
β : Type u_2
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f : α →* β
h : (∃ a, (map' f) a = 0) ∧ ∀ (a : β), ∃ a_1, (map' f) a_1 = ↑a
b : β
a✝ : α
hab : f a✝ = b
⊢ ∃ a, f a = b
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: G : Type u_1
α : Type u_2
inst✝ : LinearOrderedAddCommGroupWithTop α
a✝ b✝ c a b : α
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ a + b + (-b + -a) = 0

Tactic:
by simp [add_assoc, add_neg_cancel_of_ne_top, add_neg_cancel_left_of_ne_top, *]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y = ⊤ ↔ x = ⊤ ∨ y = ⊤

Tactic:
by cases x <;> cases y <;> simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithTop α
⊢ x + y ≠ ⊤ ↔ x ≠ ⊤ ∧ y ≠ ⊤

Tactic:
by cases x <;> cases y <;> simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊤
⊢ x < y → x + z < y + z

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

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y = ⊥ ↔ x = ⊥ ∨ y = ⊥

Tactic:
by cases x <;> cases y <;> simp [← coe_add]

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

Goal state before:
pp: α : Type u
inst✝ : Add α
x y : WithBot α
⊢ x + y ≠ ⊥ ↔ x ≠ ⊥ ∧ y ≠ ⊥

Tactic:
by cases x <;> cases y <;> simp [← coe_add]

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

Goal state before:
pp: case refine_2
α : Type u_1
inst✝ : LinearOrderedCommGroupWithZero α
H : DenselyOrdered α
⊢ DenselyOrdered αˣ

Tactic:
refine ⟨fun x y h ↦ ?_⟩
    obtain ⟨z, hz⟩ := exists_between (Units.val_lt_val.mpr h)
    refine ⟨Units.mk0 z (ne_zero_of_lt hz.1), by simp [← Units.val_lt_val, hz]⟩

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

Goal state before:
pp: α : Type u
inst✝² : Add α
x y z : WithBot α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊥
⊢ x < y → x + z < y + z

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

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

Goal state before:
pp: case coe.coe
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
inst✝² : Preorder β
x y : WithZero α
a b : α
inst✝¹ : Mul α
inst✝ : MulLeftMono α
a✝¹ a✝ c : α
hbc' : a✝ ≤ c
hbc : ↑a✝ ≤ ↑c
⊢ a✝¹ * a✝ ≤ a✝¹ * c

Tactic:
exact mul_le_mul_right hbc' _

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

Goal state before:
pp: α : Type u_1
inst✝³ : Add α
inst✝² : LE α
inst✝¹ : AddRightMono α
inst✝ : AddRightReflectLE α
a b c : WithBot (WithTop α)
hc : c ≠ ⊥
hc' : c ≠ ⊤
⊢ a + c ≤ b + c ↔ a ≤ b

Tactic:
by
  induction a <;> induction b <;> induction c <;> norm_cast at * <;>
    aesop (add simp WithTop.add_le_add_iff_right)

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithZero α
⊢ x ≤ y ∨ y ≤ x

Tactic:
by cases x <;> cases y <;> simp; simpa using Std.Total.total ..

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a b : R
h : a ≤ b
ha : a ≤ 0
⊢ 0 ≤ ⌊b⌋₊

Tactic:
exact Nat.zero_le _

Goal state after:
Module: Mathlib.Algebra.Order.Floor.Semiring

Goal state before:
pp: case inl
R : Type u_1
inst✝³ : Semiring R
inst✝² : LinearOrder R
inst✝¹ : FloorSemiring R
inst✝ : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ 0 ≤ ⌈a⌉₊

Tactic:
exact Nat.zero_le _

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithBot α
⊢ x ≤ y ∨ y ≤ x

Tactic:
by cases x <;> cases y <;> simp; simpa using Std.Total.total ..

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst✝¹ : LE α
inst✝ : Std.Total fun x1 x2 ↦ x1 ≤ x2
x y : WithTop α
⊢ x ≤ y ∨ y ≤ x

Tactic:
by cases x <;> cases y <;> simp; simpa using Std.Total.total ..

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

Goal state before:
pp: case zero
R : Type u_3
inst✝² : Semiring R
inst✝¹ : PartialOrder R
inst✝ : IsOrderedRing R
x y : R
hx : 0 ≤ x
hy : 0 ≤ y
hn : 0 + 1 ≠ 0
⊢ x ^ (0 + 1) + y ^ (0 + 1) ≤ (x + y) ^ (0 + 1)

Tactic:
simp only [zero_add, pow_one, le_refl]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : NeZero 2
a : K
⊢ a / 2 - a = -(a / 2)

Tactic:
rw [← neg_sub, sub_half]

Goal state after:
Module: Mathlib.Order.Bounds.Image

Goal state before:
pp: case refine_3
α : Type u
π : α → Type u_1
inst✝ : (a : α) → Preorder (π a)
s : Set ((a : α) → π a)
f : (a : α) → π a
H : ∀ (a : α), IsLUB (eval a '' s) (f a)
⊢ f ∈ lowerBounds (upperBounds s)

Tactic:
exact fun g hg a => (H a).2 ((Function.monotone_eval a).mem_upperBounds_image hg)

Goal state after:
Module: Mathlib.Order.WellFounded

Goal state before:
pp: β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
⊢ InjOn range {f | StrictMono f}

Tactic:
intro f

Goal state after:
β : Type u_2
γ : Type u_3
inst✝² : LinearOrder β
inst✝¹ : Preorder γ
inst✝ : WellFoundedLT β
f : β → γ
⊢ f ∈ {f | StrictMono f} → ∀ ⦃x₂ : β → γ⦄, x₂ ∈ {f | StrictMono f} → range f = range x₂ → f = x₂
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ico a b \ {a} ∪ {a} = Ico a b

Tactic:
sdiff_union_self,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a < b
⊢ Ico a b ∪ {a} = Ico a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Icc a b \ {a} ∪ {a} = Icc a b

Tactic:
sdiff_union_self,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ Icc a b ∪ {a} = Icc a b
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
by
  rw [insert_eq, union_comm, Ico_union_right h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
s t : Set α
h : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) (s ∪ t)
⊢ IsCofinalFor t s ∨ IsCofinalFor s t

Tactic:
rw [or_iff_not_imp_left]
  intro hts x hx
  simp only [IsCofinalFor, not_forall, not_exists, not_and] at hts
  obtain ⟨y, hy, hys⟩ := hts
  obtain ⟨z, (hzs | hzt), hxz, hyz⟩ := h x (.inl hx) y (.inr hy)
  · cases hys z hzs hyz
  · exact ⟨z, hzt, hxz⟩

Goal state after:
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Lattice α
a₁ a₂ b₁ b₂ : α
⊢ Ici a₁ ∩ Iic b₁ ∩ (Ici a₂ ∩ Iic b₂) = Ici a₁ ∩ Ici a₂ ∩ (Iic b₁ ∩ Iic b₂)

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.Positivity.Core

Goal state before:
pp: A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ e ≠ 0

Tactic:
rw [NormNum.IsInt.neg_to_eq h rfl]

Goal state after:
A : Type u_1
e : A
n : ℕ
inst✝² : Ring A
inst✝¹ : PartialOrder A
inst✝ : IsStrictOrderedRing A
h : NormNum.IsInt e (Int.negOfNat n)
w : Nat.ble 1 n = true
⊢ -↑n ≠ 0
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < a / (a / max (b + 1) 1)

Tactic:
div_div_cancel₀ h.ne'

Goal state after:
α : Type u_4
inst✝² : Semifield α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a : α
h : 0 < a
b : α
this : 0 < a / max (b + 1) 1
⊢ b < max (b + 1) 1
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
x : List α
m n : ℕ
⊢ take n (drop m x) ++ drop n (drop m x) = drop m x

Tactic:
take_append_drop

Goal state after:
α : Type u
x : List α
m n : ℕ
⊢ drop m x = drop m x
Module: Mathlib.Algebra.Order.Field.Basic

Goal state before:
pp: case inr
α : Type u_2
inst✝² : Field α
inst✝¹ : LinearOrder α
inst✝ : IsStrictOrderedRing α
a b c : α
hc : a * b < c
hb : 0 < b
a' : α
ha' : a < a'
hc' : a' < c / b
⊢ ∃ a' > a, a' * b < c

Tactic:
exact ⟨a', ha', (lt_div_iff₀ hb).1 hc'⟩

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
h : Forall₂ R l₁.reverse l₂.reverse
⊢ Forall₂ R l₁.reverse.reverse l₂.reverse.reverse

Tactic:
exact rel_reverse h

Goal state after:
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case cons.cons
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a : List α
a₁✝ : α
l₁✝ : List α
h1 : SublistForall₂ Rₐ a (a₁✝ :: l₁✝)
hbc : Rₐ a₁✝ head✝
tbc : SublistForall₂ Rₐ l₁✝ tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

pp: case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)

Tactic:
· obtain - | ⟨hab, tab⟩ | atb := h1
        · exact SublistForall₂.nil
        · exact SublistForall₂.cons (_root_.trans hab hbc) (ih _ _ tab tbc)
        · exact SublistForall₂.cons_right (ih _ _ atb tbc)

Goal state after:
case cons.cons_right
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R S : α → β → Prop
P : γ → δ → Prop
Rₐ : α → α → Prop
inst✝ : IsTrans α Rₐ
head✝ : α
tail✝ : List α
ih : ∀ (a b : List α), SublistForall₂ Rₐ a b → SublistForall₂ Rₐ b tail✝ → SublistForall₂ Rₐ a tail✝
a b : List α
h1 : SublistForall₂ Rₐ a b
btc : SublistForall₂ Rₐ b tail✝
⊢ SublistForall₂ Rₐ a (head✝ :: tail✝)
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl.inr
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ l₁ ~ l₂.insertIdx n a ↔ l₁ ~ l₂

Tactic:
apply iff_of_false

Goal state after:
case inl.inr.ha
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂.insertIdx n a

case inl.inr.hb
α : Type u_1
n : ℕ
a : α
l₁ l₂ : List α
hle : l₁.length ≤ l₂.length
hn₁ : l₁.length < n
hn₂ : l₂.length ≥ n
⊢ ¬l₁ ~ l₂
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
x a : α
l : List α
h : x ∈ (a :: l).head?
⊢ a :: l = x :: (a :: l).tail

Tactic:
simp only [head?, Option.mem_def, Option.some_inj] at h
    exact h ▸ rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1) * zpow' a₁.2 a₁.1

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval * l₂.eval = l.eval
⊢ l₁.eval * zpow' x r₁ * (l₂.eval * zpow' x r₂) = l₁.eval * l₂.eval * (zpow' x r₁ * zpow' x r₂)

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : (a₁ ::ᵣ l₁).eval * l₂.eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1) = l₁.eval * zpow' a₁.2 a₁.1 * l₂.eval * zpow' a₂.2 a₂.1

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
a₁ a₂ : ℤ × M
l₁ l₂ l : NF M
h : l₁.eval / (a₂ ::ᵣ l₂).eval = l.eval
⊢ l₁.eval * zpow' a₁.2 a₁.1 * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ = l₁.eval * (l₂.eval * zpow' a₂.2 a₂.1)⁻¹ * zpow' a₁.2 a₁.1

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
r₁ r₂ : ℤ
x : M
l₁ l₂ l : NF M
h : l₁.eval / l₂.eval = l.eval
⊢ l₁.eval * zpow' x r₁ * (l₂.eval⁻¹ * zpow' x (-r₂)) = l₁.eval * l₂.eval⁻¹ * (zpow' x r₁ * zpow' x (-r₂))

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
L l l' : NF M
h : L.eval * l.eval = l'.eval
⊢ L.eval * zpow' (n, e).2 (n, e).1 * l.eval = L.eval * l.eval * zpow' (n, e).2 (n, e).1

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * zpow' e n = t_n.eval * zpow' e n * t_d.eval⁻¹

Tactic:
ac_rfl

Goal state after:
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
n : ℤ
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * (zpow' e n)⁻¹ = t_n.eval * (t_d.eval⁻¹ * (zpow' e n)⁻¹)

Tactic:
ac_rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod) =
    x * y * (zipWith (fun x1 x2 ↦ x1 * x2) xs ys).prod * (drop (y :: ys).length (x :: xs)).prod *
      (drop (x :: xs).length (y :: ys)).prod

Tactic:
lhs

Goal state after:
M : Type u_4
inst✝ : CommMonoid M
x : M
xs : List M
y : M
ys : List M
| x * xs.prod * (y * ys.prod)
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : CommGroupWithZero M
e : M
t t_n t_d : NF M
h : t.eval = t_n.eval / t_d.eval
⊢ t_n.eval * t_d.eval⁻¹ * (zpow' e 1 * zpow' e (-1)) = t_n.eval * zpow' e 1 * (t_d.eval⁻¹ * zpow' e (-1))

Tactic:
ac_rfl

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
⊢ Injective (map f) ↔ Injective f

Tactic:
refine ⟨fun h x y hxy => ?_, (·.list_map)⟩

Goal state after:
α : Type u
β : Type v
f : α → β
h : Injective (map f)
x y : α
hxy : f x = f y
⊢ x = y
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = a /. c + b /. c

Tactic:
divInt_add_divInt _ _ h h,

Goal state after:
a b c : ℤ
h : ¬c = 0
⊢ (a + b) /. c = (a * c + b * c) /. (c * c)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ l : List α
p : l₁ ~ l₂
⊢ l.Disjoint l₁ ↔ l.Disjoint l₂

Tactic:
simp_rw [List.disjoint_right, p.mem_iff]

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n : ℕ
⊢ ↑(↑n).toNNRat = ↑↑n

Tactic:
by simp only [Nat.cast_nonneg', Rat.coe_toNNRat]; rfl

Goal state after:
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: p q : ℚ
⊢ q.toNNRat < p.toNNRat ↔ q < p ∧ 0 < p

Tactic:
simp [← coe_lt_coe, toNNRat]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1 = x * (d * e)

Tactic:
lhs

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
x y : α
x✝¹ : DvdNotUnit x y
hx0 : x ≠ 0
d : α
hdu : ¬IsUnit d
hdx : y = x * d
x✝ : y ∣ x
e : α
he : x = y * e
| x * 1
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y (x * z) ↔ IsRelPrime y z

Tactic:
isRelPrime_mul_unit_left_right hu

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
x y z : α
hu : IsUnit x
⊢ IsRelPrime y z ↔ IsRelPrime y z
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : a₁ * a₂ * n ∣ a₁ * a₂ * (b * c)
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1

Tactic:
mul_dvd_mul_iff_left h0

Goal state after:
case inr
α : Type u_2
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
n : α
hn : IsPrimal n
a₁ a₂ b c : α
hm : IsPrimal (a₁ * a₂)
h0 : a₁ * a₂ ≠ 0
h : n ∣ b * c
⊢ ∃ a₁_1 a₂_1, a₁_1 ∣ a₁ * b ∧ a₂_1 ∣ a₂ * c ∧ a₁ * a₂ * n = a₁_1 * a₂_1
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: a b : ℤ
⊢ ↑(a /. b).den ∣ b

Tactic:
by_cases b0 : b = 0; · simp [b0]
  rcases e : a /. b with ⟨n, d, h, c⟩
  rw [mk_eq_divInt,
    divInt_eq_divInt_iff b0 (ne_of_gt (Int.natCast_pos.2 (Nat.pos_of_ne_zero h)))] at e
  refine Int.dvd_natAbs.1 <| Int.natCast_dvd_natCast.2 <| c.symm.dvd_of_dvd_mul_left ?_
  rw [← Int.natAbs_mul, ← Int.natCast_dvd_natCast, Int.dvd_natAbs, ← e]; simp

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ (q * q).num = q.num * q.num

Tactic:
rw [mul_num, Int.natAbs_mul, Nat.Coprime.gcd_eq_one, Int.ofNat_one, Int.ediv_one]
  exact (q.reduced.mul_right q.reduced).mul_left (q.reduced.mul_right q.reduced)

Goal state after:
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: case mp
qr : ℚ
⊢ IsSquare (qr * qr).num ∧ IsSquare (qr * qr).den

Tactic:
rw [Rat.mul_self_num, mul_self_den]

Goal state after:
case mp
qr : ℚ
⊢ IsSquare (qr.num * qr.num) ∧ IsSquare (qr.den * qr.den)