mathlib-initiative/mathlib-tactics huggingface dataset:
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)
⊢ Function.RightInverse g f

Tactic:
by
      intro
      rw [← cmp_eq_eq_iff, ← h, cmp_self_eq_eq]

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

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

Tactic:
rw [codisjoint_iff_le_sup, ← f.map_sup, ← f.map_top]
  exact f.monotone ha.top_le

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

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : Group α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a : α
⊢ 1 ≤ |a|ₘ

Tactic:
by
  apply pow_two_semiclosed _
  rw [mabs, pow_two, mul_sup, sup_mul, ← pow_two, inv_mul_cancel, sup_comm, ← sup_assoc]
  apply le_sup_right

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

Goal state before:
pp: a : ℤ
⊢ |a|.natAbs = a.natAbs

Tactic:
grind

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

Goal state before:
pp: i j : ℤ
⊢ 0 < (i - j).natAbs ↔ i ≠ j

Tactic:
grind

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

Goal state before:
pp: a : ℤ
⊢ |a| < 1 ↔ a = 0

Tactic:
grind

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

Goal state before:
pp: a : ℤ
⊢ |a| ≤ 1 ↔ a = 0 ∨ a = 1 ∨ a = -1

Tactic:
grind

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

Goal state before:
pp: m a b : ℕ
ha : a < m
hb : b < m
⊢ |↑b - ↑a| < ↑m

Tactic:
grind

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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ |n| = 1 ↔ a ^ n = 1

Tactic:
← Int.natCast_natAbs,

Goal state after:
G : Type u_1
inst✝ : Group G
a : G
n : ℤ
⊢ a ^ ↑n.natAbs = 1 ↔ a ^ n = 1
Module: Mathlib.Algebra.Order.Group.Unbundled.Abs

Goal state before:
pp: α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
⊢ |a|ₘ = |b|ₘ ↔ a = b ∨ a = b⁻¹

Tactic:
refine ⟨fun h ↦ ?_, by rintro (h | h) <;> simp [h]⟩

Goal state after:
α : Type u_1
inst✝¹ : Group α
inst✝ : LinearOrder α
a b : α
h : |a|ₘ = |b|ₘ
⊢ a = b ∨ a = b⁻¹
Module: Mathlib.Algebra.Ring.Int.Parity

Goal state before:
pp: n : ℤ
x✝ : Odd n
m : ℤ
hm : n = 2 * m + 1
⊢ n % 2 = 1

Tactic:
grind

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

Goal state before:
pp: n : ℤ
h : n % 2 = 1
⊢ n = 2 * (n / 2) + 1

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ n % 2 = 0

Tactic:
grind

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

Goal state before:
pp: ⊢ ¬Odd 0

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Odd n ↔ Even n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Even n ↔ Odd n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even n ∨ Odd n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Xor (Even n) (Odd n)

Tactic:
grind

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

Goal state before:
pp: case h
k : ℤ
⊢ Xor (k + k = 2 * k) (k + k = 2 * k + 1)

Tactic:
grind

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

Goal state before:
pp: case h
k : ℤ
⊢ Xor (2 * k + 1 = 2 * k) (2 * k + 1 = 2 * k + 1)

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Even (m + n) ↔ (Odd m ↔ Odd n)

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ ¬Even (2 * n + 1)

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Even (m - n) ↔ (Odd m ↔ Odd n)

Tactic:
grind

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

Goal state before:
pp: m : ℤ
n : ℕ
⊢ Odd (m ^ n) ↔ Odd m ∨ n = 0

Tactic:
grind

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

Goal state before:
pp: m : ℤ
n : ℕ
h : n ≠ 0
⊢ Odd (m ^ n) ↔ Odd m

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m + n) ↔ (Odd n ↔ Even m)

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
h : Odd (m + n)
⊢ m ≠ n

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd m ↔ Even n)

Tactic:
grind

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

Goal state before:
pp: m n : ℤ
⊢ Odd (m - n) ↔ (Odd n ↔ Even m)

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n * (n + 1))

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even (n * (n - 1))

Tactic:
grind

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

Goal state before:
pp: n : ℕ
⊢ Odd ↑n ↔ Odd n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Even n.natAbs ↔ Even n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n.natAbs ↔ Odd n

Tactic:
grind

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

Goal state before:
pp: a b : ℤ
ha : Odd a
hb : Odd b
⊢ 4 ∣ a + b ∨ 4 ∣ a - b

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → 2 * (n / 2) + 1 = n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → n / 2 * 2 + 1 = n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
⊢ Odd n → 1 + n / 2 * 2 = n

Tactic:
grind

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

Goal state before:
pp: n : ℤ
h : Odd n
⊢ 2 * (n / 2) = n - 1

Tactic:
grind

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

Goal state before:
pp: z : ℤ
⊢ Even z.sign ↔ z = 0

Tactic:
grind

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

Goal state before:
pp: z : ℤ
⊢ Odd z.sign ↔ z ≠ 0

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DivisionMonoid α
inst✝ : HasDistribNeg α
a : α
k : ℕ
⊢ 2 * -(↑k + 1) + 1 = -(1 + ↑k * 2)

Tactic:
grind

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

Goal state before:
pp: s t : ℤ
r' : ℕ
s' t' : ℤ
r : ℕ
h : 0 < r.succ
⊢ (match r.succ, fun m x ↦
      Nat.strongRec (motive := fun x ↦ ℤ → ℤ → ℕ → ℤ → ℤ → ℕ × ℤ × ℤ)
        (fun n ih s t r' s' t' ↦
          match n, ih with
          | 0, ih => (r', s', t')
          | k.succ, ih =>
            have q := r' / k.succ;
            ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t)
        m with
    | 0, ih => (r', s', t')
    | k.succ, ih =>
      have q := r' / k.succ;
      ih (r' % k.succ) ⋯ (s' - ↑q * s) (t' - ↑q * t) k.succ s t) =
    (r' % r.succ).xgcdAux (s' - ↑r' / ↑r.succ * s) (t' - ↑r' / ↑r.succ * t) r.succ s t

Tactic:
rfl

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

Goal state before:
pp: m n : ℤ
even : Even (n - m)
⊢ m + 2 ≤ n ↔ m < n

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case none
α β γ : Type u
f : α → β → γ
b : Option β
⊢ map₂ f none b = f <$> none <*> b

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case some
α β γ : Type u
f : α → β → γ
b : Option β
val✝ : α
⊢ map₂ f (some val✝) b = f <$> some val✝ <*> b

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case none
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f none none = none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: case some
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
val✝ : α
⊢ map₂ f (some val✝) none = none

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : β
⊢ map₂ f a (some b) = Option.map (fun a ↦ f a b) a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : γ
⊢ c ∈ map₂ f a b ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
c : γ
⊢ map₂ f a b = some c ↔ ∃ a' b', a' ∈ a ∧ b' ∈ b ∧ f a' b' = c

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = none ↔ a = none ∨ b = none

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun a b ↦ f b a) b a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → β → γ
g : γ → δ
⊢ Option.map g (map₂ f a b) = map₂ (fun a b ↦ g (f a b)) a b

Tactic:
grind

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f 1 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f (↑a✝) 1 = 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case one
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f 1 ↑b = map (fun x ↦ f x b) 1

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Group.WithOne.Map

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝

Tactic:
rfl

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : γ → β → δ
g : α → γ
⊢ map₂ f (Option.map g a) b = map₂ (fun a b ↦ f (g a) b) a b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
f : α → γ → δ
g : β → γ
⊢ map₂ f a (Option.map g b) = map₂ (fun a b ↦ f a (g b)) a b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
a : Option α
b : Option β
⊢ map₂ (curry f) a b = Option.map f (map₂ Prod.mk a b)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
x : Option (α × β)
⊢ Option.map (uncurry f) x = map₂ f (Option.map Prod.fst x) (Option.map Prod.snd x)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
ε : Type u_8
ε' : Type u_9
f : δ → γ → ε
g : α → β → δ
f' : α → ε' → ε
g' : β → γ → ε'
h_assoc : ∀ (a : α) (b : β) (c : γ), f (g a b) c = f' a (g' b c)
⊢ map₂ f (map₂ g a b) c = map₂ f' a (map₂ g' b c)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
g : β → α → γ
h_comm : ∀ (a : α) (b : β), f a b = g b a
⊢ map₂ f a b = map₂ g b a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : α → δ → ε
g : β → γ → δ
f' : α → γ → δ'
g' : β → δ' → ε
h_left_comm : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' b (f' a c)
⊢ map₂ f a (map₂ g b c) = map₂ g' b (map₂ f' a c)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
c : Option γ
δ' : Type u_7
ε : Type u_8
f : δ → γ → ε
g : α → β → δ
f' : α → γ → δ'
g' : δ' → β → ε
h_right_comm : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f' a c) b
⊢ map₂ f (map₂ g a b) c = map₂ g' (map₂ f' a c) b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : α' → β' → δ
g₁ : α → α'
g₂ : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ a) (g₂ b)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ a) (Option.map g₂ b)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' a) b

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : α → β' → δ
g' : β → β'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' a (g' b)
⊢ Option.map g (map₂ f a b) = map₂ f' a (Option.map g' b)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : α → β → δ
g' : δ → γ
h_left_comm : ∀ (a : α) (b : β), f (g a) b = g' (f' a b)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' a b)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : α → β → δ
g' : δ → γ
h_right_comm : ∀ (a : α) (b : β), f a (g b) = g' (f' a b)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' a b)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
β' : Type u_6
g : γ → δ
f' : β' → α' → δ
g₁ : β → β'
g₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g₁ b) (g₂ a)
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g₁ b) (Option.map g₂ a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
β' : Type u_6
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ Option.map g (map₂ f a b) = map₂ f' (Option.map g' b) a

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : α → β → γ
a : Option α
b : Option β
α' : Type u_5
g : γ → δ
f' : β → α' → δ
g' : α → α'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' b (g' a)
⊢ Option.map g (map₂ f a b) = map₂ f' b (Option.map g' a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
α' : Type u_5
f : α' → β → γ
g : α → α'
f' : β → α → δ
g' : δ → γ
h_left_anticomm : ∀ (a : α) (b : β), f (g a) b = g' (f' b a)
⊢ map₂ f (Option.map g a) b = Option.map g' (map₂ f' b a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a : Option α
b : Option β
β' : Type u_6
f : α → β' → γ
g : β → β'
f' : β → α → δ
g' : δ → γ
h_right_anticomm : ∀ (a : α) (b : β), f a (g b) = g' (f' b a)
⊢ map₂ f a (Option.map g b) = Option.map g' (map₂ f' b a)

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
o : Option β
⊢ map₂ f (some a) o = o

Tactic:
grind

Goal state after:
Module: Mathlib.Data.Option.NAry

Goal state before:
pp: α : Type u_1
β : Type u_2
f : α → β → α
b : β
h : ∀ (a : α), f a b = a
o : Option α
⊢ map₂ f o (some b) = o

Tactic:
grind

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

Goal state before:
pp: case zero
β : Type u_2
inst✝ : MulOneClass β
⊢ ↑(map' (MonoidHom.id β)) 0 = (MonoidHom.id (WithZero β)) 0

Tactic:
rfl

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

Goal state before:
pp: case coe
β : Type u_2
inst✝ : MulOneClass β
a✝ : β
⊢ ↑(map' (MonoidHom.id β)) ↑a✝ = (MonoidHom.id (WithZero β)) ↑a✝

Tactic:
rfl

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

Goal state before:
pp: case zero
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
⊢ (map' g) ((map' f) 0) = (map' (g.comp f)) 0

Tactic:
rfl

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

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : MulOneClass α
inst✝¹ : MulOneClass β
inst✝ : MulOneClass γ
f : α →* β
g : β →* γ
a✝ : α
⊢ (map' g) ((map' f) ↑a✝) = (map' (g.comp f)) ↑a✝

Tactic:
rfl

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

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

Tactic:
grind

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : Monoid α
n : ℕ
⊢ 0 ^ (n + 1) = 0

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : DivInvMonoid α
n : ℕ
⊢ 0 ^ ↑n.succ = 0

Tactic:
rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x : Multiplicative M
⊢ exp (↑x).log = ↑x

Tactic:
rfl

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

Goal state before:
pp: M : Type u_4
inst✝ : AddMonoid M
x y : Multiplicative M
⊢ (↑x * ↑y).log = (↑x).log + (↑y).log

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case top
G : Type u_1
inst✝ : AddCommGroup G
⊢ ⊤ - ⊤ = ⊤

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ⊤ - ↑a✝ = ⊤

Tactic:
rfl

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

Goal state before:
pp: G : Type u_5
inst✝ : AddGroup G
x y : Multiplicative G
⊢ (↑x / ↑y).log = (↑x).log - (↑y).log

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.AddGroupWithTop

Goal state before:
pp: case coe
G : Type u_1
inst✝ : AddCommGroup G
a✝ : G
⊢ ↑a✝ - ⊤ = ⊤

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊔ b) = ↑(if a ≤ b then b else a)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Order.Monoid.Units

Goal state before:
pp: α : Type u_1
inst✝¹ : Monoid α
inst✝ : LinearOrder α
a b : αˣ
⊢ ↑(a ⊓ b) = ↑(if a ≤ b then a else b)

Tactic:
rfl

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

Goal state before:
pp: case top
α : Type u
inst✝ : Add α
⊢ ⊤ + ⊤ = ⊤

Tactic:
rfl

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

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊤ = ⊤

Tactic:
rfl

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

Goal state before:
pp: case coe.coe
α : Type u
β : Type v
inst✝³ : Add α
F : Type u_1
inst✝² : Add β
inst✝¹ : FunLike F α β
inst✝ : AddHomClass F α β
f : F
a✝¹ a✝ : α
⊢ map ⇑f ↑(a✝¹ + a✝) = ↑(f (a✝¹ + a✝))

Tactic:
rfl

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

Goal state before:
pp: case bot
α : Type u
inst✝ : Add α
⊢ ⊥ + ⊥ = ⊥

Tactic:
rfl

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

Goal state before:
pp: case coe
α : Type u
inst✝ : Add α
a✝ : α
⊢ ↑a✝ + ⊥ = ⊥

Tactic:
rfl

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

Goal state before:
pp: R : Type u_1
inst✝³ : AddCommGroupWithOne R
inst✝² : PartialOrder R
inst✝¹ : AddLeftMono R
inst✝ : ZeroLEOneClass R
⊢ Monotone Int.cast

Tactic:
by
  intro m n h
  rw [← sub_nonneg] at h
  lift n - m to ℕ using h with k hk
  rw [← sub_nonneg, ← cast_sub, ← hk, cast_natCast]
  exact k.cast_nonneg'

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f ⊥ ⊥ = ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a✝ : α
⊢ map₂ f ↑a✝ ⊥ = ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case bot
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f ⊥ ↑b = map (fun x ↦ f x b) ⊥

Tactic:
rfl

Goal state after:
Module: Mathlib.Order.WithBot

Goal state before:
pp: case coe
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a✝ : α
⊢ map₂ f ↑a✝ ↑b = map (fun x ↦ f x b) ↑a✝

Tactic:
rfl

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

Goal state before:
pp: α : Type u_1
inst✝¹ : LinearOrderedCommMonoidWithZero α
a : α
n : ℕ
inst✝ : IsReduced α
hn : n ≠ 0
⊢ 0 < a ^ n ↔ 0 < a

Tactic:
by
  simp_rw [pos_iff_ne_zero, pow_ne_zero_iff hn]

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

Goal state before:
pp: case mpr
m : ℕ
p : ℕ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
hm : p m
hlt : ∀ (n : ℕ), n < m → ¬p n
this : Nat.find h ≤ m
⊢ Nat.find h = m

Tactic:
grind

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

Goal state before:
pp: case neg
P : ℕ → Prop
inst✝ : DecidablePred P
k : ℕ
ihk : ∀ {m : ℕ}, findGreatest P k = m ↔ m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n
m : ℕ
hk : ¬P (k + 1)
⊢ (m ≤ k ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k → ¬P n) ↔
    m ≤ k + 1 ∧ (m ≠ 0 → P m) ∧ ∀ ⦃n : ℕ⦄, m < n → n ≤ k + 1 → ¬P n

Tactic:
grind

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

Goal state before:
pp: k : ℕ
P : ℕ → Prop
inst✝ : DecidablePred P
⊢ (Exists fun ⦃n⦄ ↦ 0 < n ∧ n ≤ k ∧ P n) ↔ Exists fun ⦃n⦄ ↦ 0 < n ∧ n ≤ k ∧ P n

Tactic:
rfl

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

Goal state before:
pp: case zero
P Q : ℕ → Prop
inst✝¹ : DecidablePred P
inst✝ : DecidablePred Q
hPQ : ∀ (n : ℕ), P n → Q n
⊢ findGreatest P 0 ≤ findGreatest Q 0

Tactic:
rfl

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

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → b ≤ z
Hb' : ∀ (z : ℤ), P z → b' ≤ z
Hinh : ∃ z, P z
⊢ ↑(b.leastOfBdd Hb Hinh) = ↑(b'.leastOfBdd Hb' Hinh)

Tactic:
grind

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

Goal state before:
pp: P : ℤ → Prop
inst✝ : DecidablePred P
b b' : ℤ
Hb : ∀ (z : ℤ), P z → z ≤ b
Hb' : ∀ (z : ℤ), P z → z ≤ b'
Hinh : ∃ z, P z
⊢ ↑(b.greatestOfBdd Hb Hinh) = ↑(b'.greatestOfBdd Hb' Hinh)

Tactic:
grind

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

Goal state before:
pp: α : Type u_3
b : α
h : ↑(ofAdd b) ≠ 0
⊢ toAdd (unzero h) = b

Tactic:
rfl

Goal state after: