internlm/Lean-Github huggingface dataset:
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
let pj := p * j
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * (n——m + k——j) ≃ q——p * n——m + q——p * k——j
Tactic:
show q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q——p * n_k——m_j ≃ (qn + pm)——(qm + pn) + (qk + pj)——(qj + pk)
Tactic:
show (q * n_k + p * m_j)——(q * m_j + p * n_k)
   ≃ ((qn + pm) + (qk + pj))——((qm + pn) + (qj + pk))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j)——(q * m_j + p * n_k) ≃ (qn + pm + (qk + pj))——(qm + pn + (qj + pk))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j)——(q * m_j + p * n_k) ≃ (qn + pm + (qk + pj))——(qm + pn + (qj + pk))
Tactic:
show from_prod (q * n_k + p * m_j, q * m_j + p * n_k)
   ≃ from_prod ((qn + pm) + (qk + pj), (qm + pn) + (qj + pk))
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ from_prod (q * n_k + p * m_j, q * m_j + p * n_k) ≃ from_prod (qn + pm + (qk + pj), qm + pn + (qj + pk))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ from_prod (q * n_k + p * m_j, q * m_j + p * n_k) ≃ from_prod (qn + pm + (qk + pj), qm + pn + (qj + pk))
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j, q * m_j + p * n_k) ≃ (qn + pm + (qk + pj), qm + pn + (qj + pk))
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ (q * n_k + p * m_j, q * m_j + p * n_k) ≃ (qn + pm + (qk + pj), qm + pn + (qj + pk))
Tactic:
apply Relation.Equivalence.Impl.Prod.eqv_defn.mpr
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
have distrib_swap (w x y z : ℕ)
    : q * (w + y) + p * (x + z) ≃ (q * w + p * x) + (q * y + p * z)
    := calc
  q * (w + y) + p * (x + z)         ≃ _ := AA.substL AA.distribL
  (q * w + q * y) + p * (x + z)     ≃ _ := AA.substR AA.distribL
  (q * w + q * y) + (p * x + p * z) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (q * w + p * x) + (q * y + p * z) ≃ _ := Rel.refl
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj) ∧ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
apply And.intro
Proof state after:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj)

case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
case a.left
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * n_k + p * m_j ≃ qn + pm + (qk + pj)
Tactic:
exact distrib_swap n m k j
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_distribL
Proof state before:
case a.right
ℕ : Type
inst✝ : Natural ℕ
q p n m k j : ℕ
n_k : ℕ := n + k
m_j : ℕ := m + j
qn : ℕ := q * n
qm : ℕ := q * m
qk : ℕ := q * k
qj : ℕ := q * j
pn : ℕ := p * n
pm : ℕ := p * m
pk : ℕ := p * k
pj : ℕ := p * j
distrib_swap : ∀ (w x y z : ℕ), q * (w + y) + p * (x + z) ≃ q * w + p * x + (q * y + p * z)
⊢ q * m_j + p * n_k ≃ qm + pn + (qj + pk)
Tactic:
exact distrib_swap m n j k
Proof state after:
no goals
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m)——0 ≃ n——0 * m——0
Tactic:
show (n * m)——0 ≃ (n * m + 0 * 0)——(n * 0 + 0 * m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m)——0 ≃ (n * m + 0 * 0)——(n * 0 + 0 * m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m)——0 ≃ (n * m + 0 * 0)——(n * 0 + 0 * m)
Tactic:
show from_prod (n * m, 0) ≃ from_prod (n * m + 0 * 0, n * 0 + 0 * m)
Proof state after:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (n * m, 0) ≃ from_prod (n * m + 0 * 0, n * 0 + 0 * m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_compat_natural
Proof state before:
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ from_prod (n * m, 0) ≃ from_prod (n * m + 0 * 0, n * 0 + 0 * m)
Tactic:
apply AA.subst₁
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m, 0) ≃ (n * m + 0 * 0, n * 0 + 0 * m)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_compat_natural
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m, 0) ≃ (n * m + 0 * 0, n * 0 + 0 * m)
Tactic:
apply Rel.symm (α := ℕ × ℕ)
Proof state after:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m + 0 * 0, n * 0 + 0 * m) ≃ (n * m, 0)
Theorem: Lean4Axiomatic.Integer.Impl.Difference.mul_compat_natural
Proof state before:
case a
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
⊢ (n * m + 0 * 0, n * 0 + 0 * m) ≃ (n * m, 0)
Tactic:
calc
  (n * m + 0 * 0, n * 0 + 0 * m) ≃ _ := AA.substL (AA.substR AA.absorbL)
  (n * m + 0, n * 0 + 0 * m)     ≃ _ := AA.substL Natural.add_zero
  (n * m, n * 0 + 0 * m)         ≃ _ := AA.substR (AA.substL AA.absorbR)
  (n * m, 0 + 0 * m)             ≃ _ := AA.substR Natural.zero_add
  (n * m, 0 * m)                 ≃ _ := AA.substR AA.absorbL
  (n * m, 0)                     ≃ _ := Rel.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.iff_subst_covar
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
⊢ (p₁ ↔ p₂) → (f p₁ ↔ f p₂)
Tactic:
intro (Iff.intro (_ : p₁ → p₂) (_ : p₂ → p₁))
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_covar
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₁ → f p₂ := f_subst ‹p₁ → p₂›
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_covar
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₂ → f p₁ := f_subst ‹p₂ → p₁›
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₁ → f p₂
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_covar
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₁ → f a₂
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₁ → f p₂
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
Tactic:
exact Iff.intro ‹f p₁ → f p₂› ‹f p₂ → f p₁›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.iff_subst_contra
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
⊢ (p₁ ↔ p₂) → (f p₁ ↔ f p₂)
Tactic:
intro (Iff.intro (_ : p₁ → p₂) (_ : p₂ → p₁))
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_contra
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₂ → f p₁ := f_subst ‹p₁ → p₂›
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_contra
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this : f p₂ → f p₁
⊢ f p₁ ↔ f p₂
Tactic:
have : f p₁ → f p₂ := f_subst ‹p₂ → p₁›
Proof state after:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₂ → f p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂
Theorem: Lean4Axiomatic.Logic.iff_subst_contra
Proof state before:
f : Prop → Prop
f_subst : ∀ {a₁ a₂ : Prop}, (a₁ → a₂) → f a₂ → f a₁
p₁ p₂ : Prop
mp✝ : p₁ → p₂
mpr✝ : p₂ → p₁
this✝ : f p₂ → f p₁
this : f p₁ → f p₂
⊢ f p₁ ↔ f p₂
Tactic:
exact Iff.intro ‹f p₁ → f p₂› ‹f p₂ → f p₁›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.and_mapL
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
⊢ p₁ ∧ q → p₂ ∧ q
Tactic:
intro (And.intro (_ : p₁) (_ : q))
Proof state after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
⊢ p₂ ∧ q
Theorem: Lean4Axiomatic.Logic.and_mapL
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
⊢ p₂ ∧ q
Tactic:
have : p₂ := f ‹p₁›
Proof state after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
this : p₂
⊢ p₂ ∧ q
Theorem: Lean4Axiomatic.Logic.and_mapL
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : p₁
right✝ : q
this : p₂
⊢ p₂ ∧ q
Tactic:
exact And.intro ‹p₂› ‹q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.and_mapR
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
⊢ q ∧ p₁ → q ∧ p₂
Tactic:
intro (And.intro (_ : q) (_ : p₁))
Proof state after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : q
right✝ : p₁
⊢ q ∧ p₂
Theorem: Lean4Axiomatic.Logic.and_mapR
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : q
right✝ : p₁
⊢ q ∧ p₂
Tactic:
have : p₂ := f ‹p₁›
Proof state after:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : q
right✝ : p₁
this : p₂
⊢ q ∧ p₂
Theorem: Lean4Axiomatic.Logic.and_mapR
Proof state before:
p₁ p₂ q : Prop
f : p₁ → p₂
left✝ : q
right✝ : p₁
this : p₂
⊢ q ∧ p₂
Tactic:
exact And.intro ‹q› ‹p₂›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
⊢ p ∨ q ∧ r ↔ (p ∨ q) ∧ (p ∨ r)
Tactic:
apply Iff.intro
Proof state after:
case mp
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)

case mpr
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)
Tactic:
case mp =>
  intro (_ : p ∨ (q ∧ r))
  show (p ∨ q) ∧ (p ∨ r)
  match ‹p ∨ (q ∧ r)› with
  | Or.inl (_ : p) =>
    have : p ∨ q := Or.inl ‹p›
    have : p ∨ r := Or.inl ‹p›
    exact And.intro ‹p ∨ q› ‹p ∨ r›
  | Or.inr (And.intro (_ : q) (_ : r)) =>
    have : p ∨ q := Or.inr ‹q›
    have : p ∨ r := Or.inr ‹r›
    exact And.intro ‹p ∨ q› ‹p ∨ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r
Tactic:
case mpr =>
  intro (And.intro (_ : p ∨ q) (_ : p ∨ r))
  show p ∨ (q ∧ r)
  match ‹p ∨ q› with
  | Or.inl (_ : p) =>
    exact Or.inl ‹p›
  | Or.inr (_ : q) =>
    match ‹p ∨ r› with
    | Or.inl (_ : p) =>
      exact Or.inl ‹p›
    | Or.inr (_ : r) =>
      have : q ∧ r := And.intro ‹q› ‹r›
      exact Or.inr ‹q ∧ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
⊢ p ∨ q ∧ r → (p ∨ q) ∧ (p ∨ r)
Tactic:
intro (_ : p ∨ (q ∧ r))
Proof state after:
p q r : Prop
x✝ : p ∨ q ∧ r
⊢ (p ∨ q) ∧ (p ∨ r)
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
match ‹p ∨ (q ∧ r)› with
| Or.inl (_ : p) =>
  have : p ∨ q := Or.inl ‹p›
  have : p ∨ r := Or.inl ‹p›
  exact And.intro ‹p ∨ q› ‹p ∨ r›
| Or.inr (And.intro (_ : q) (_ : r)) =>
  have : p ∨ q := Or.inr ‹q›
  have : p ∨ r := Or.inr ‹r›
  exact And.intro ‹p ∨ q› ‹p ∨ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ q := Or.inl ‹p›
Proof state after:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ r := Or.inl ‹p›
Proof state after:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
h✝ : p
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
exact And.intro ‹p ∨ q› ‹p ∨ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ q := Or.inr ‹q›
Proof state after:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this : p ∨ q
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
have : p ∨ r := Or.inr ‹r›
Proof state after:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
x✝ : p ∨ q ∧ r
left✝ : q
right✝ : r
this✝ : p ∨ q
this : p ∨ r
⊢ (p ∨ q) ∧ (p ∨ r)
Tactic:
exact And.intro ‹p ∨ q› ‹p ∨ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
⊢ (p ∨ q) ∧ (p ∨ r) → p ∨ q ∧ r
Tactic:
intro (And.intro (_ : p ∨ q) (_ : p ∨ r))
Proof state after:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
⊢ p ∨ q ∧ r
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
⊢ p ∨ q ∧ r
Tactic:
match ‹p ∨ q› with
| Or.inl (_ : p) =>
  exact Or.inl ‹p›
| Or.inr (_ : q) =>
  match ‹p ∨ r› with
  | Or.inl (_ : p) =>
    exact Or.inl ‹p›
  | Or.inr (_ : r) =>
    have : q ∧ r := And.intro ‹q› ‹r›
    exact Or.inr ‹q ∧ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝ : p
⊢ p ∨ q ∧ r
Tactic:
exact Or.inl ‹p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝ : q
⊢ p ∨ q ∧ r
Tactic:
match ‹p ∨ r› with
| Or.inl (_ : p) =>
  exact Or.inl ‹p›
| Or.inr (_ : r) =>
  have : q ∧ r := And.intro ‹q› ‹r›
  exact Or.inr ‹q ∧ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : p
⊢ p ∨ q ∧ r
Tactic:
exact Or.inl ‹p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
⊢ p ∨ q ∧ r
Tactic:
have : q ∧ r := And.intro ‹q› ‹r›
Proof state after:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
this : q ∧ r
⊢ p ∨ q ∧ r
Theorem: Lean4Axiomatic.Logic.or_distribL_and
Proof state before:
p q r : Prop
left✝ : p ∨ q
right✝ : p ∨ r
h✝¹ : q
h✝ : r
this : q ∧ r
⊢ p ∨ q ∧ r
Tactic:
exact Or.inr ‹q ∧ r›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
⊢ ¬(p ∨ q) ↔ ¬p ∧ ¬q
Tactic:
apply Iff.intro
Proof state after:
case mp
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q

case mpr
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
case mp =>
  intro (_ : ¬(p ∨ q))
  show ¬p ∧ ¬q
  have : ¬p := by
    intro (_ : p)
    show False
    have : p ∨ q := Or.inl ‹p›
    exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
  have : ¬q := by
    intro (_ : q)
    show False
    have : p ∨ q := Or.inr ‹q›
    exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
  exact And.intro ‹¬p› ‹¬q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
case mpr =>
  intro (And.intro (_ : ¬p) (_ : ¬q)) (_ : p ∨ q)
  show False
  match ‹p ∨ q› with
  | Or.inl (_ : p) => exact absurd ‹p› ‹¬p›
  | Or.inr (_ : q) => exact absurd ‹q› ‹¬q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
⊢ ¬(p ∨ q) → ¬p ∧ ¬q
Tactic:
intro (_ : ¬(p ∨ q))
Proof state after:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p ∧ ¬q
Tactic:
have : ¬p := by
  intro (_ : p)
  show False
  have : p ∨ q := Or.inl ‹p›
  exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
Proof state after:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬p ∧ ¬q
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬p ∧ ¬q
Tactic:
have : ¬q := by
  intro (_ : q)
  show False
  have : p ∨ q := Or.inr ‹q›
  exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
Proof state after:
p q : Prop
x✝ : ¬(p ∨ q)
this✝ : ¬p
this : ¬q
⊢ ¬p ∧ ¬q
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝ : ¬(p ∨ q)
this✝ : ¬p
this : ¬q
⊢ ¬p ∧ ¬q
Tactic:
exact And.intro ‹¬p› ‹¬q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝ : ¬(p ∨ q)
⊢ ¬p
Tactic:
intro (_ : p)
Proof state after:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
⊢ False
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
⊢ False
Tactic:
have : p ∨ q := Or.inl ‹p›
Proof state after:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
this : p ∨ q
⊢ False
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝¹ : ¬(p ∨ q)
x✝ : p
this : p ∨ q
⊢ False
Tactic:
exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝ : ¬(p ∨ q)
this : ¬p
⊢ ¬q
Tactic:
intro (_ : q)
Proof state after:
p q : Prop
x✝¹ : ¬(p ∨ q)
this : ¬p
x✝ : q
⊢ False
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝¹ : ¬(p ∨ q)
this : ¬p
x✝ : q
⊢ False
Tactic:
have : p ∨ q := Or.inr ‹q›
Proof state after:
p q : Prop
x✝¹ : ¬(p ∨ q)
this✝ : ¬p
x✝ : q
this : p ∨ q
⊢ False
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
x✝¹ : ¬(p ∨ q)
this✝ : ¬p
x✝ : q
this : p ∨ q
⊢ False
Tactic:
exact absurd ‹p ∨ q› ‹¬(p ∨ q)›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
⊢ ¬p ∧ ¬q → ¬(p ∨ q)
Tactic:
intro (And.intro (_ : ¬p) (_ : ¬q)) (_ : p ∨ q)
Proof state after:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
⊢ False
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
⊢ False
Tactic:
match ‹p ∨ q› with
| Or.inl (_ : p) => exact absurd ‹p› ‹¬p›
| Or.inr (_ : q) => exact absurd ‹q› ‹¬q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
h✝ : p
⊢ False
Tactic:
exact absurd ‹p› ‹¬p›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Logic.not_or_iff_and_not
Proof state before:
p q : Prop
left✝ : ¬p
right✝ : ¬q
x✝ : p ∨ q
h✝ : q
⊢ False
Tactic:
exact absurd ‹q› ‹¬q›
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.refl
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
⊢ f ≃ f
Tactic:
show ∀ (x : α), f x ≃ f x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
⊢ ∀ (x : α), f x ≃ f x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.refl
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
⊢ ∀ (x : α), f x ≃ f x
Tactic:
intro x
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
x : α
⊢ f x ≃ f x
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.refl
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f : (x : α) → β x
x : α
⊢ f x ≃ f x
Tactic:
exact indexed_eqvOp.refl
Proof state after:
no goals
Theorem: Lean4Axiomatic.Relation.Equivalence.Impl.DepFn.symm
Proof state before:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
⊢ f ≃ g → g ≃ f
Tactic:
intro (_ : ∀ (x : α), f x ≃ g x)
Proof state after:
α : Sort u
β : α → Sort v
indexed_eqvOp : {x : α} → EqvOp (β x)
f g : (x : α) → β x
x✝ : ∀ (x : α), f x ≃ g x
⊢ g ≃ f