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

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a * b h✝ = a * b h✝

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a * c h✝ = a * c h✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a * b h✝ = a * b h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a * c h✝ = a * c h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ * c = a h✝ * c

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ * c = b h✝ * c

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ * c = a h✝ * c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ * c = b h✝ * c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ * c h✝ = a h✝ * c h✝

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ * d h✝ = b h✝ * d h✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ * c h✝ = a h✝ * c h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ * d h✝ = b h✝ * d h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : P
⊢ a * c = a * c

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : ¬P
⊢ b * d = b * d

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : P
⊢ a * c = a * c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Mul α
a b c d : α
h✝ : ¬P
⊢ b * d = b * d
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : P
⊢ -b = -b

pp: case isFalse
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : ¬P
⊢ -c = -c

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : P
⊢ -b = -b

case isFalse
α : Type u_3
P : Prop
inst✝¹ : Decidable P
inst✝ : Neg α
b c : α
h✝ : ¬P
⊢ -c = -c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a / b h✝ = a / b h✝

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a / c h✝ = a / c h✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : P
⊢ a / b h✝ = a / b h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : α
b : P → α
c : ¬P → α
h✝ : ¬P
⊢ a / c h✝ = a / c h✝
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ / c = a h✝ / c

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ / c = b h✝ / c

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : P
⊢ a h✝ / c = a h✝ / c

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : α
h✝ : ¬P
⊢ b h✝ / c = b h✝ / c
Module: Mathlib.Algebra.Notation.Defs

Goal state before:
pp: case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ / c h✝ = a h✝ / c h✝

pp: case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ / d h✝ = b h✝ / d h✝

Tactic:
<;>

Goal state after:
case isTrue
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : P
⊢ a h✝ / c h✝ = a h✝ / c h✝

case isFalse
α : Type u_2
P : Prop
inst✝¹ : Decidable P
inst✝ : Div α
a : P → α
b : ¬P → α
c : P → α
d : ¬P → α
h✝ : ¬P
⊢ b h✝ / d h✝ = b h✝ / d h✝
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero
b : Bool
⊢ bit b 0 = 0 ↔ 0 = 0 ∧ b = false

pp: case succ
b : Bool
n✝ : Nat
⊢ bit b (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ b = false

Tactic:
<;>

Goal state after:
case zero
b : Bool
⊢ bit b 0 = 0 ↔ 0 = 0 ∧ b = false

case succ
b : Bool
n✝ : Nat
⊢ bit b (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ b = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero.false
⊢ bit false 0 = 0 ↔ 0 = 0 ∧ false = false

pp: case zero.true
⊢ bit true 0 = 0 ↔ 0 = 0 ∧ true = false

pp: case succ.false
n✝ : Nat
⊢ bit false (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ false = false

pp: case succ.true
n✝ : Nat
⊢ bit true (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ true = false

Tactic:
<;>

Goal state after:
case zero.false
⊢ bit false 0 = 0 ↔ 0 = 0 ∧ false = false

case zero.true
⊢ bit true 0 = 0 ↔ 0 = 0 ∧ true = false

case succ.false
n✝ : Nat
⊢ bit false (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ false = false

case succ.true
n✝ : Nat
⊢ bit true (n✝ + 1) = 0 ↔ n✝ + 1 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
x n : Nat
⊢ bit false x < 2 ^ (n + 1) ↔ x < 2 ^ n

pp: case true
x n : Nat
⊢ bit true x < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
<;>

Goal state after:
case false
x n : Nat
⊢ bit false x < 2 ^ (n + 1) ↔ x < 2 ^ n

case true
x n : Nat
⊢ bit true x < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
x n : Nat
⊢ 2 * x < 2 ^ (n + 1) ↔ x < 2 ^ n

pp: case true
x n : Nat
⊢ 2 * x + 1 < 2 ^ (n + 1) ↔ x < 2 ^ n

Tactic:
<;>

Goal state after:
case false
x n : Nat
⊢ 2 * x < 2 ^ (n + 1) ↔ x < 2 ^ n

case true
x n : Nat
⊢ 2 * x + 1 < 2 ^ (n + 1) ↔ x < 2 ^ n
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
ih : motive 0
h : ¬(0 = 0 → b = true)
⊢ 0 = 0 ∧ b = false

pp: case succ
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → b = true)
⊢ n✝ + 1 = 0 ∧ b = false

Tactic:
<;>

Goal state after:
case zero
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
ih : motive 0
h : ¬(0 = 0 → b = true)
⊢ 0 = 0 ∧ b = false

case succ
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
b : Bool
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → b = true)
⊢ n✝ + 1 = 0 ∧ b = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case zero.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → false = true)
⊢ 0 = 0 ∧ false = false

pp: case zero.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → true = true)
⊢ 0 = 0 ∧ true = false

pp: case succ.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → false = true)
⊢ n✝ + 1 = 0 ∧ false = false

pp: case succ.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → true = true)
⊢ n✝ + 1 = 0 ∧ true = false

Tactic:
<;>

Goal state after:
case zero.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → false = true)
⊢ 0 = 0 ∧ false = false

case zero.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
ih : motive 0
h : ¬(0 = 0 → true = true)
⊢ 0 = 0 ∧ true = false

case succ.false
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → false = true)
⊢ n✝ + 1 = 0 ∧ false = false

case succ.true
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → (n = 0 → b = true) → motive n → motive (Nat.bit b n)
n✝ : Nat
ih : motive (n✝ + 1)
h : ¬(n✝ + 1 = 0 → true = true)
⊢ n✝ + 1 = 0 ∧ true = false
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
n : Nat
⊢ bit false n = 2 * n + false.toNat

pp: case true
n : Nat
⊢ bit true n = 2 * n + true.toNat

Tactic:
<;>

Goal state after:
case false
n : Nat
⊢ bit false n = 2 * n + false.toNat

case true
n : Nat
⊢ bit true n = 2 * n + true.toNat
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: b : Bool
n : Nat
⊢ bit b n = 2 * n + b.toNat

Tactic:
by
  cases b <;> rfl

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

Goal state before:
pp: case false
n : Nat
⊢ false.toNat < 2

pp: case true
n : Nat
⊢ true.toNat < 2

Tactic:
<;>

Goal state after:
case false
n : Nat
⊢ false.toNat < 2

case true
n : Nat
⊢ true.toNat < 2
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: case false
n : Nat
⊢ bit false n % 2 = false.toNat

pp: case true
n : Nat
⊢ bit true n % 2 = true.toNat

Tactic:
<;>

Goal state after:
case false
n : Nat
⊢ bit false n % 2 = false.toNat

case true
n : Nat
⊢ bit true n % 2 = true.toNat
Module: Mathlib.Data.Nat.BinaryRec

Goal state before:
pp: motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ binaryRec zero bit (Nat.bit false 0) = bit false 0 (binaryRec zero bit 0)

Tactic:
unfold binaryRec

Goal state after:
motive : Nat → Sort u
zero : motive 0
bit : (b : Bool) → (n : Nat) → motive n → motive (Nat.bit b n)
h' : Nat.bit false 0 = 0
h : bit false 0 zero = zero
⊢ (if n0 : Nat.bit false 0 = 0 then ⋯ ▸ zero
    else
      have x := bit (1 &&& Nat.bit false 0 != 0) (Nat.bit false 0 >>> 1) (binaryRec zero bit (Nat.bit false 0 >>> 1));
      ⋯ ▸ x) =
    bit false 0
      (if n0 : 0 = 0 then ⋯ ▸ zero
      else
        have x := bit (1 &&& 0 != 0) (0 >>> 1) (binaryRec zero bit (0 >>> 1));
        ⋯ ▸ x)
Module: Mathlib.Algebra.Group.Semiconj.Defs

Goal state before:
pp: S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ a * y * b = z * (a * b)

Tactic:
ha.eq,

Goal state after:
S : Type u_1
inst✝ : Semigroup S
a b x y z : S
ha : SemiconjBy a y z
hb : SemiconjBy b x y
⊢ z * a * b = z * (a * b)
Module: Mathlib.Order.Defs.Unbundled

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

Tactic:
by simpa using symm a b

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

Goal state before:
pp: M : Type u
⊢ ∀ ⦃m₁ m₂ : MulOneClass M⦄, Mul.mul = Mul.mul → m₁ = m₂

Tactic:
rintro @⟨@⟨⟨one₁⟩, ⟨mul₁⟩⟩, one_mul₁, mul_one₁⟩ @⟨@⟨⟨one₂⟩, ⟨mul₂⟩⟩, one_mul₂, mul_one₂⟩ ⟨rfl⟩

Goal state after:
M : Type u
one₁ : M
mul₁ : M → M → M
one_mul₁ : ∀ (a : M), 1 * a = a
mul_one₁ : ∀ (a : M), a * 1 = a
one₂ : M
one_mul₂ : ∀ (a : M), 1 * a = a
mul_one₂ : ∀ (a : M), a * 1 = a
⊢ { one := one₁, mul := mul₁, one_mul := one_mul₁, mul_one := mul_one₁ } =
    { one := one₂, mul := mul₁, one_mul := one_mul₂, mul_one := mul_one₂ }
Module: Mathlib.Algebra.Group.Defs

Goal state before:
pp: case bit.false
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit false k' ≠ 0
⊢ (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n

pp: case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n

Tactic:
<;>

Goal state after:
case bit.false
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit false k' ≠ 0
⊢ (bif false then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit false k') n

case bit.true
M : Type u_2
inst✝¹ : Semigroup M
inst✝ : One M
k k' : ℕ
k'0 : k' ≠ 0
ih :
  ∀ (m n : M),
    k' ≠ 0 →
      Nat.binaryRec (motive := fun x ↦ M → M → M) (fun y x ↦ y)
          (fun bn _n fn y x ↦ fn (bif bn then y * x else y) (x * x)) k' m n =
        m * npowRec' k' n
m n : M
hk : Nat.bit true k' ≠ 0
⊢ (bif true then m * n else m) * npowRec' k' (n * n) = m * npowRec' (Nat.bit true k') n
Module: Mathlib.Logic.Function.Defs

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

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

Tactic:
<;>

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

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

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

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

Tactic:
<;>

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

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

Goal state before:
pp: α : Type u_1
⊢ ¬¬Nontrivial α ↔ Nontrivial α

Tactic:
Classical.not_not

Goal state after:
α : Type u_1
⊢ Nontrivial α ↔ Nontrivial α
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
A : Prop
B : A → Prop
h : A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

pp: case neg
A : Prop
B : A → Prop
h : ¬A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

Tactic:
<;>

Goal state after:
case pos
A : Prop
B : A → Prop
h : A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h

case neg
A : Prop
B : A → Prop
h : ¬A
⊢ (A → ∀ (h : A), B h) ↔ ∀ (h : A), B h
Module: Mathlib.Logic.Basic

Goal state before:
pp: α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ∃ a, ¬P a

Tactic:
← not_forall

Goal state after:
α : Sort u_1
P : α → Prop
⊢ (∀ (a : α), P a) ∨ ¬∀ (x : α), P x
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h

pp: case neg
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h

Tactic:
<;>

Goal state after:
case pos
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : h
⊢ p h

case neg
p : Prop → Prop
x✝ : p False ∧ p True
h : Prop
h₁ : p False
h₂ : p True
H : ¬h
⊢ p h
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
h✝ : P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

pp: case neg
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
h✝ : ¬P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
h✝ : P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c

case neg
α : Sort u_1
P : Prop
inst✝ : Decidable P
c : α
A : P → α
B : ¬P → α
h✝ : ¬P
⊢ dite P A B = c ↔ (∃ h, A h = c) ∨ ∃ h, B h = c
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

pp: case neg
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

Tactic:
<;>

Goal state after:
case pos
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)

case neg
α : Sort u_3
β : Sort u_4
γ : Sort u_5
f : α → β → γ
P : Prop
inst✝ : Decidable P
a : P → α
b : ¬P → α
c : P → β
d : ¬P → β
h : ¬P
⊢ f (dite P a b) (dite P c d) = if h : P then f (a h) (c h) else f (b h) (d h)
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a

pp: case neg
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : P
⊢ dite P f g a = if h : P then f h a else g h a

case neg
α : Sort u_1
σ : α → Sort u_2
P : Prop
inst✝ : Decidable P
f : P → (a : α) → σ a
g : ¬P → (a : α) → σ a
a : α
h : ¬P
⊢ dite P f g a = if h : P then f h a else g h a
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∧ Q then a else b) = if P then if Q then a else b else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

pp: case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

pp: case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

Tactic:
<;>

Goal state after:
case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case pos
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b

case neg
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
a b : α
inst✝ : Decidable Q
hp : ¬P
hq : ¬Q
⊢ (if P ∨ Q then a else b) = if P then a else if Q then a else b
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

pp: case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

Tactic:
<;>

Goal state after:
case pos
P Q R : Prop
inst✝ : Decidable P
p : P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R

case neg
P Q R : Prop
inst✝ : Decidable P
p : ¬P
⊢ (if P then Q else R) ↔ P ∧ Q ∨ ¬P ∧ R
Module: Mathlib.Logic.Basic

Goal state before:
pp: case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

pp: case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

Tactic:
<;>

Goal state after:
case pos
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p

case neg
P : Prop
inst✝ : Decidable P
Q : P → Prop
R : ¬P → Prop
h : ¬P
⊢ dite P Q R ↔ (∃ p, Q p) ∨ ∃ p, R p