mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x✝ : (α × β) × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ) ⁻¹' s ×ˢ t ×ˢ u ↔ x✝ ∈ (s ×ˢ t) ×ˢ u
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
⊢ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Set α
t : Set β
u : Set γ
x✝ : α × β × γ
⊢ x✝ ∈ ⇑(prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u ↔ x✝ ∈ s ×ˢ t ×ˢ u
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
⊢ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) = x

Tactic:
ext

Goal state after:
α✝¹ : Sort u
β✝ : Sort v
γ : Sort w
α✝ : Type u_1
β : Type u_2
α : Type ?u.8
S : Set α
x : Set ↑S
x✝ : ↑S
⊢ x✝ ∈ (fun x ↦ Subtype.val ⁻¹' ↑x) ((fun x ↦ ⟨Subtype.val '' x, ⋯⟩) x) ↔ x✝ ∈ x
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
⊢ ofLeftInverse f f_inv hf = ofInjective f ⋯

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
f_inv : Nonempty α → β → α
hf : ∀ (h : Nonempty α), LeftInverse (f_inv h) f
x✝ : α
⊢ ↑((ofLeftInverse f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)
Module: Mathlib.Logic.Equiv.Set

Goal state before:
pp: α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
⊢ ofLeftInverse' f f_inv hf = ofInjective f ⋯

Tactic:
ext

Goal state after:
α : Type u_3
β : Type u_4
f : α → β
f_inv : β → α
hf : LeftInverse f_inv f
x✝ : α
⊢ ↑((ofLeftInverse' f f_inv hf) x✝) = ↑((ofInjective f ⋯) x✝)
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ Iio 1 = ∅

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Iio 1 ↔ x✝ ∈ ∅
Module: Mathlib.Order.Interval.Set.Basic

Goal state before:
pp: α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
⊢ Ici 1 = univ

Tactic:
ext

Goal state after:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : One α
inst✝ : IsBotOneClass α
x✝ : α
⊢ x✝ ∈ Ici 1 ↔ x✝ ∈ univ
Module: Mathlib.Order.Interval.Set.Basic

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

Tactic:
by
  simp only [Ici_inter_Iic.symm, Ici_inter_Ici.symm, Iic_inter_Iic.symm]; ac_rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
⊢ upperBounds (s ×ˢ t) = upperBounds s ×ˢ upperBounds t

Tactic:
ext

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
hs : s.Nonempty
ht : t.Nonempty
x✝ : α × β
⊢ x✝ ∈ upperBounds (s ×ˢ t) ↔ x✝ ∈ upperBounds s ×ˢ upperBounds t
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
simp only [div_eq_mul_inv, mul_pos_iff_of_pos_left ha, inv_pos]

Goal state after:
Module: Mathlib.Control.Functor

Goal state before:
pp: γ : Type u_1
⊢ LawfulFunctor (Const γ)

Tactic:
constructor

Goal state after:
case map_const
γ : Type u_1
⊢ ∀ {α β : Type u_2}, mapConst = map ∘ Function.const β

case id_map
γ : Type u_1
⊢ ∀ {α : Type u_2} (x : Const γ α), id <$> x = x

case comp_map
γ : Type u_1
⊢ ∀ {α β γ_1 : Type u_2} (g : α → β) (h : β → γ_1) (x : Const γ α), (h ∘ g) <$> x = h <$> g <$> x
Module: Mathlib.Data.List.Defs

Goal state before:
pp: α : Type u_1
f : α → α
a : α
n : ℕ
l : List α
⊢ iterateTR.loop f a n l = l.reverse ++ iterate f a n

Tactic:
induction n generalizing a l

Goal state after:
case zero
α : Type u_1
f : α → α
a : α
l : List α
⊢ iterateTR.loop f a 0 l = l.reverse ++ iterate f a 0

case succ
α : Type u_1
f : α → α
n✝ : ℕ
a✝ : ∀ (a : α) (l : List α), iterateTR.loop f a n✝ l = l.reverse ++ iterate f a n✝
a : α
l : List α
⊢ iterateTR.loop f a (n✝ + 1) l = l.reverse ++ iterate f a (n✝ + 1)
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).tail = take (n - 1) l.tail

Tactic:
ext

Goal state after:
α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (take n l).tail[i✝]? = some a✝ ↔ (take (n - 1) l.tail)[i✝]? = some a✝
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (take n l).dropLast = take (n - 1) l.dropLast

Tactic:
ext

Goal state after:
α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (take n l).dropLast[i✝]? = some a✝ ↔ (take (n - 1) l.dropLast)[i✝]? = some a✝
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).tail = drop n l.tail

Tactic:
ext

Goal state after:
α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (drop n l).tail[i✝]? = some a✝ ↔ (drop n l.tail)[i✝]? = some a✝
Module: Mathlib.Data.List.TakeDrop

Goal state before:
pp: α : Type u
l : List α
n : ℕ
⊢ (drop n l).dropLast = drop n l.dropLast

Tactic:
ext

Goal state after:
α : Type u
l : List α
n i✝ : ℕ
a✝ : α
⊢ (drop n l).dropLast[i✝]? = some a✝ ↔ (drop n l.dropLast)[i✝]? = some a✝
Module: Mathlib.Algebra.Order.Field.Basic

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

Tactic:
by
  simpa [one_div] using inv_lt_inv_of_neg ha hb

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

Goal state before:
pp: case nil
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
⊢ Forall₂ S [] []

Tactic:
constructor

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

Goal state before:
pp: case cons
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S (a✝² :: l₁✝) (b✝ :: l₂✝)

Tactic:
constructor

Goal state after:
case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ S a✝² b✝

case cons.a
α : Type u_1
β : Type u_2
R S : α → β → Prop
H : ∀ (a : α) (b : β), R a b → S a b
l₁ : List α
l₂ : List β
a✝² : α
b✝ : β
l₁✝ : List α
l₂✝ : List β
a✝¹ : R a✝² b✝
a✝ : Forall₂ R l₁✝ l₂✝
a_ih✝ : Forall₂ S l₁✝ l₂✝
⊢ Forall₂ S l₁✝ l₂✝
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b ↔ a = b

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
a b : List α
⊢ Forall₂ (fun x1 x2 ↦ x1 = x2) a b → a = b

case mpr
α : Type u_1
a b : List α
⊢ a = b → Forall₂ (fun x1 x2 ↦ x1 = x2) a b
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: case nil.refl
α : Type u_1
β : Type u_2
R : α → β → Prop
h₁ : [].length = [].length
h₂ : ∀ {a : α} {b : β}, (a, b) ∈ [].zip [] → R a b
⊢ Forall₂ R [] []

Tactic:
constructor

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ ↔ ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ SublistForall₂ R l₁ l₂ → ∃ l, Forall₂ R l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
R : α → β → Prop
l₁ : List α
l₂ : List β
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ l₂) → SublistForall₂ R l₁ l₂
Module: Mathlib.Data.List.Forall2

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) ↔ ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂) → ∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂

case mpr
α : Type u_1
β : Type u_2
γ : Type u_3
R : α → β → Prop
f : γ → β
l₁ : List α
l₂ : List γ
⊢ (∃ l, Forall₂ (fun a c ↦ R a (f c)) l₁ l ∧ l <+ l₂) → ∃ l, Forall₂ R l₁ l ∧ l <+ map f l₂
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: case inl
α : Type u_1
l₁ l₂ : List α
m n : ℕ
h : l₁[m]? = l₂[n]?
hm : m < l₁.length
⊢ l₁.eraseIdx m ~ l₂.eraseIdx n ↔ l₁ ~ l₂

Tactic:
| inl hm =>

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

Goal state before:
pp: α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c ↔ a ~ c

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
a c : List α
⊢ (Perm ∘r Perm) a c → a ~ c

case mpr
α : Type u_1
a c : List α
⊢ a ~ c → (Perm ∘r Perm) a c
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
⊢ Injective length ↔ Subsingleton α

Tactic:
constructor

Goal state after:
case mp
α : Type u
⊢ Injective length → Subsingleton α

case mpr
α : Type u
⊢ Subsingleton α → Injective length
Module: Mathlib.Data.List.Perm.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ ↔ (Perm ∘r Forall₂ r) l₁ l₃

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Forall₂ r ∘r Perm) l₁ l₃ → (Perm ∘r Forall₂ r) l₁ l₃

case mpr
α : Type u_1
β : Type u_2
r : α → β → Prop
l₁ : List α
l₃ : List β
⊢ (Perm ∘r Forall₂ r) l₁ l₃ → (Forall₂ r ∘r Perm) l₁ l₃
Module: Mathlib.Tactic.FieldSimp.Lemmas

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

Tactic:
unfold eval cons

Goal state after:
M : Type u_1
inst✝ : CommGroupWithZero M
p : ℤ × M
l : NF M
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        (p :: l)).prod =
    (map
          (fun x ↦
            match x with
            | (r, x) => zpow' x r)
          l).prod *
      zpow' p.2 p.1
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ ((r, x) ::ᵣ l).eval ≠ 0

Tactic:
unfold eval cons

Goal state after:
M : Type u_1
inst✝ : GroupWithZero M
r : ℤ
x : M
hx : x ≠ 0
l : NF M
hl : l.eval ≠ 0
⊢ (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)).prod ≠
    0
Module: Mathlib.Tactic.FieldSimp.Lemmas

Goal state before:
pp: M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 < ((r, x) ::ᵣ l).eval

Tactic:
unfold eval cons

Goal state after:
M : Type u_1
inst✝⁴ : GroupWithZero M
inst✝³ : PartialOrder M
inst✝² : PosMulStrictMono M
inst✝¹ : PosMulReflectLT M
inst✝ : ZeroLEOneClass M
r : ℤ
x : M
hx : 0 < x
l : NF M
hl : 0 < l.eval
⊢ 0 <
    (map
        (fun x ↦
          match x with
          | (r, x) => zpow' x r)
        ((r, x) :: l)).prod
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l : List α
a : α
⊢ l <+ [a] ↔ l = [] ∨ l = [a]

Tactic:
constructor

Goal state after:
case mp
α : Type u
l : List α
a : α
⊢ l <+ [a] → l = [] ∨ l = [a]

case mpr
α : Type u
l : List α
a : α
⊢ l = [] ∨ l = [a] → l <+ [a]
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
l : List α
x✝ : b = a
e : b = a := x✝
⊢ idxOf a (b :: l) = 0

Tactic:
rw [← e]; exact idxOf_cons_self

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

Goal state before:
pp: case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ f a' * f a ^ count a as = f a ^ (count a as + 0)

Tactic:
hf a' ha' mem_cons_self,

Goal state after:
case neg
α : Type u_2
M : Type u_4
inst✝¹ : Monoid M
inst✝ : DecidableEq α
f : α → M
a' : α
as : List α
a : α
h : (map f as).prod = f a ^ count a as
hf : ∀ (a'_1 : α), a'_1 ≠ a → a'_1 ∈ a' :: as → f a'_1 = 1
ha' : ¬a' = a
⊢ 1 * f a ^ count a as = f a ^ (count a as + 0)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ ↔ l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

Tactic:
constructor

Goal state after:
case mp
α : Type u
l₁ l₂ : List α
⊢ l₁ = l₂ → l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩

case mpr
α : Type u
l₁ l₂ : List α
⊢ (l₁.length = l₂.length ∧ ∀ (n : ℕ) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁.get ⟨n, h₁⟩ = l₂.get ⟨n, h₂⟩) →
    l₁ = l₂
Module: Mathlib.Algebra.BigOperators.Group.List.Basic

Goal state before:
pp: G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
⊢ ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) = fun k ↦ f k / f (k + 1)

Tactic:
ext

Goal state after:
G : Type u_7
inst✝ : CommGroup G
n : ℕ
f : ℕ → G
x✝ : ℕ
⊢ ((fun x ↦ x⁻¹) ∘ fun k ↦ f (k + 1) / f k) x✝ = f x✝ / f (x✝ + 1)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
β : Type v
f : β → α → β
b : β
x : α
xs : List α
⊢ foldl f b (xs ++ [x]) = f (foldl f b xs) x

Tactic:
by
  simp only [List.foldl_append, List.foldl]

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

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ ↑0 = 0

Tactic:
ext

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
⊢ ↑↑0 = ↑0
Module: Mathlib.Algebra.Order.Nonneg.Basic

Goal state before:
pp: α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
x✝ : ℕ
⊢ ↑(x✝ + 1) = ↑x✝ + 1

Tactic:
ext

Goal state after:
α : Type u_1
inst✝³ : AddMonoidWithOne α
inst✝² : PartialOrder α
inst✝¹ : AddLeftMono α
inst✝ : ZeroLEOneClass α
x✝ : ℕ
⊢ ↑↑(x✝ + 1) = ↑(↑x✝ + 1)
Module: Mathlib.Data.List.Basic

Goal state before:
pp: α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ ↔ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

Tactic:
constructor

Goal state after:
case mp
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂ → x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂

case mpr
α : Type u
x₁ x₂ z₁ z₂ : List α
a₁ a₂ : α
notin_x : ¬a₂ ∈ x₁
notin_z : ¬a₂ ∈ z₁
⊢ x₁ = x₂ ∧ a₁ = a₂ ∧ z₁ = z₂ → x₁ ++ a₁ :: z₁ = x₂ ++ a₂ :: z₂
Module: Mathlib.Data.Rat.Defs

Goal state before:
pp: f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ }
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d

Tactic:
rw [mk_eq_divInt] at hc

Goal state after:
f : ℚ → ℚ → ℚ
f₁ f₂ : ℤ → ℤ → ℤ → ℤ → ℤ
fv :
  ∀ {n₁ : ℤ} {d₁ : ℕ} {h₁ : d₁ ≠ 0} {c₁ : n₁.natAbs.Coprime d₁} {n₂ : ℤ} {d₂ : ℕ} {h₂ : d₂ ≠ 0}
    {c₂ : n₂.natAbs.Coprime d₂},
    f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
      f₁ n₁ (↑d₁) n₂ ↑d₂ /. f₂ n₁ (↑d₁) n₂ ↑d₂
f0 : ∀ {n₁ d₁ n₂ d₂ : ℤ}, d₁ ≠ 0 → d₂ ≠ 0 → f₂ n₁ d₁ n₂ d₂ ≠ 0
a b c d : ℤ
b0 : b ≠ 0
d0 : d ≠ 0
H : ∀ {n₁ d₁ n₂ d₂ : ℤ}, a * d₁ = n₁ * b → c * d₂ = n₂ * d → f₁ n₁ d₁ n₂ d₂ * f₂ a b c d = f₁ a b c d * f₂ n₁ d₁ n₂ d₂
n₁ : ℤ
d₁ : ℕ
h₁ : d₁ ≠ 0
c₁ : n₁.natAbs.Coprime d₁
ha : a /. b = n₁ /. ↑d₁
n₂ : ℤ
d₂ : ℕ
h₂ : d₂ ≠ 0
c₂ : n₂.natAbs.Coprime d₂
hc : c /. d = n₂ /. ↑d₂
⊢ f { num := n₁, den := d₁, den_nz := h₁, reduced := c₁ } { num := n₂, den := d₂, den_nz := h₂, reduced := c₂ } =
    f₁ a b c d /. f₂ a b c d
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
⊢ q⁻¹ = divNat q.den q.num

Tactic:
ext

Goal state after:
q : ℚ≥0
⊢ ↑q⁻¹ = ↑(divNat q.den q.num)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: p q : ℚ≥0
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)

Tactic:
ext

Goal state after:
p q : ℚ≥0
⊢ ↑(p / q) = ↑(divNat (p.num * q.den) (p.den * q.num))
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: p q : ℚ≥0
⊢ p / q = divNat (p.num * q.den) (p.den * q.num)

Tactic:
by
  ext; simp [Rat.div_def', num_coe, den_coe]

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

Goal state before:
pp: a b : ℕ
⊢ divNat a b = ↑a / ↑b

Tactic:
ext

Goal state after:
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: a : ℚ≥0
⊢ a ^ 0 = 1

Tactic:
ext

Goal state after:
a : ℚ≥0
⊢ ↑(a ^ 0) = ↑1
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ ↑n.succ = a ^ ↑n * a

Tactic:
ext

Goal state after:
n : ℕ
a : ℚ≥0
⊢ ↑(a ^ ↑n.succ) = ↑(a ^ ↑n * a)
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: n : ℕ
a : ℚ≥0
⊢ a ^ Int.negSucc n = (a ^ ↑n.succ)⁻¹

Tactic:
ext

Goal state after:
n : ℕ
a : ℚ≥0
⊢ ↑(a ^ Int.negSucc n) = ↑(a ^ ↑n.succ)⁻¹
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: ⊢ 0⁻¹ = 0

Tactic:
ext

Goal state after:
⊢ ↑0⁻¹ = ↑0
Module: Mathlib.Algebra.Field.Rat

Goal state before:
pp: q : ℚ≥0
h : q ≠ 0
⊢ q * q⁻¹ = 1

Tactic:
ext

Goal state after:
q : ℚ≥0
h : q ≠ 0
⊢ ↑(q * q⁻¹) = ↑1
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ ↑q = 0 ↔ q = 0

Tactic:
by norm_cast

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

Goal state before:
pp: p : ℚ
q : ℚ≥0
hp : 0 ≤ p
⊢ q ≤ p.toNNRat ↔ ↑q ≤ p

Tactic:
by
  rw [← coe_le_coe, Rat.coe_toNNRat p hp]

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

Goal state before:
pp: case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ (p * q).toNNRat = p.toNNRat * q.toNNRat

Tactic:
ext

Goal state after:
case inl
p q : ℚ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ↑(p * q).toNNRat = ↑(p.toNNRat * q.toNNRat)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: n₁ n₂ d₁ d₂ : ℕ
⊢ divNat n₁ d₁ * divNat n₂ d₂ = divNat (n₁ * n₂) (d₁ * d₂)

Tactic:
ext

Goal state after:
n₁ n₂ d₁ d₂ : ℕ
⊢ ↑(divNat n₁ d₁ * divNat n₂ d₂) = ↑(divNat (n₁ * n₂) (d₁ * d₂))
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (a * n) (a * d) = divNat n d

Tactic:
ext

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (a * n) (a * d)) = ↑(divNat n d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (n * a) (d * a) = divNat n d

Tactic:
ext

Goal state after:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (n * a) (d * a)) = ↑(divNat n d)
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q : ℚ≥0
⊢ q * ↑q.den = ↑q.num

Tactic:
ext

Goal state after:
q : ℚ≥0
⊢ ↑(q * ↑q.den) = ↑↑q.num
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q r : ℚ≥0
⊢ q + r = divNat (q.num * r.den + r.num * q.den) (q.den * r.den)

Tactic:
ext

Goal state after:
q r : ℚ≥0
⊢ ↑(q + r) = ↑(divNat (q.num * r.den + r.num * q.den) (q.den * r.den))
Module: Mathlib.Data.NNRat.Defs

Goal state before:
pp: q r : ℚ≥0
⊢ q * r = divNat (q.num * r.num) (q.den * r.den)

Tactic:
ext

Goal state after:
q r : ℚ≥0
⊢ ↑(q * r) = ↑(divNat (q.num * r.num) (q.den * r.den))
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ DvdNotUnit a b

Tactic:
constructor

Goal state after:
case left
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ a ≠ 0

case right
α : Type u_1
inst✝ : CommMonoidWithZero α
a b : α
hd : a ∣ b
hnd : ¬b ∣ a
⊢ ∃ x, ¬IsUnit x ∧ b = a * x
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a u : α
hu : IsUnit u
⊢ u ∣ a

Tactic:
rcases hu with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : Monoid α
a : α
u : αˣ
⊢ ↑u ∣ a
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a ∣ b * u ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a ∣ b * ↑u ↔ a ∣ b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : Monoid α
a b u : α
hu : IsUnit u
⊢ a * u ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : Monoid α
a b : α
u : αˣ
⊢ a * ↑u ∣ b ↔ a ∣ b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ a ∣ u * b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ a ∣ ↑u * b ↔ a ∣ b
Module: Mathlib.Algebra.Divisibility.Units

Goal state before:
pp: α : Type u_1
inst✝ : CommMonoid α
a b u : α
hu : IsUnit u
⊢ u * a ∣ b ↔ a ∣ b

Tactic:
rcases hu with ⟨u, rfl⟩

Goal state after:
α : Type u_1
inst✝ : CommMonoid α
a b : α
u : αˣ
⊢ ↑u * a ∣ b ↔ a ∣ b
Module: Mathlib.Algebra.GroupWithZero.Divisibility

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m ↔ n ≤ m

Tactic:
constructor

Goal state after:
case mp
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ a ^ n ∣ a ^ m → n ≤ m

case mpr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : IsCancelMulZero α
a : α
m n : ℕ
ha₀ : a ≠ 0
ha : ¬IsUnit a
⊢ n ≤ m → a ^ n ∣ a ^ m
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: q : ℚ
⊢ IsSquare q ↔ IsSquare q.num ∧ IsSquare q.den

Tactic:
constructor

Goal state after:
case mp
q : ℚ
⊢ IsSquare q → IsSquare q.num ∧ IsSquare q.den

case mpr
q : ℚ
⊢ IsSquare q.num ∧ IsSquare q.den → IsSquare q
Module: Mathlib.Data.Rat.Lemmas

Goal state before:
pp: n d : ℤ
d_ne_zero : d ≠ 0
⊢ ↑n / ↑d = n /. d

Tactic:
← Rat.divInt_eq_div

Goal state after:
n d : ℤ
d_ne_zero : d ≠ 0
⊢ n /. d = n /. d
Module: Mathlib.Data.Rat.Cast.CharZero

Goal state before:
pp: α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ divNat a b = ↑a / ↑b

Tactic:
ext

Goal state after:
α : Type u_3
inst✝¹ : DivisionSemiring α
inst✝ : CharZero α
a b : ℕ
⊢ ↑(divNat a b) = ↑(↑a / ↑b)
Module: Mathlib.Tactic.NormNum.Inv

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionRing R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑qi * ↑denom✝ = 1

Tactic:
by norm_cast

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

Goal state before:
pp: R : Type u_1
inst✝¹ : DivisionSemiring R
inst✝ : CharZero R
num✝ denom✝ : ℕ
qi : ℚ≥0
invOf_mul_self✝ : qi * ↑denom✝ = 1
mul_invOf_self✝ : ↑denom✝ * qi = 1
⊢ ↑denom✝ * ↑qi = 1

Tactic:
by norm_cast

Goal state after: