internlm/Lean-Github huggingface dataset:
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.left
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h2 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' ψ) →' (ψ ∨' χ →' ψ) →' φ ∨' (ψ ∨' χ) →' ψ
h3 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ (φ →' χ) →' (ψ ∨' χ →' χ) →' φ ∨' (ψ ∨' χ) →' χ
⊢ ∅ ⊢ φ ∧' (ψ ∨' χ) →' φ ∧' ψ ∨' φ ∧' χ
Tactic:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
⊢ {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Tactic:
have h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ := by simp;
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Tactic:
have h5 := MP (EDisj (axiomEConj₁ _ _ _) (axiomEConj₁ _ _ _)) h1
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h5 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Theorem: PropositionalLogic.HilbertSystem.HPM.distConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ χ : L
h1 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ ∧' ψ ∨' φ ∧' χ
h5 : {φ ∧' ψ ∨' φ ∧' χ} ⊢ φ
⊢ ∅ ⊢ φ ∧' ψ ∨' φ ∧' χ →' φ ∧' (ψ ∨' χ)
Tactic:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'(φ ∨' ψ) ↔' ¬'φ ∧' ¬'ψ
Tactic:
apply ILiff'
Proof state after:
case a
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ (∅ ⊢ ¬'(φ ∨' ψ) →' ¬'φ ∧' ¬'ψ) ∧ (∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ))
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ (∅ ⊢ ¬'(φ ∨' ψ) →' ¬'φ ∧' ¬'ψ) ∧ (∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ))
Tactic:
apply And.intro
Proof state after:
case a.left
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'(φ ∨' ψ) →' ¬'φ ∧' ¬'ψ

case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ)
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.left
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'(φ ∨' ψ) →' ¬'φ ∧' ¬'ψ

case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ)
Tactic:
. sorry
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ)
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ)
Tactic:
. simp [deduction];
  have h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥') := by simp;
  have h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ := by simp;
  have h3 := (EDisj (EConj₁ h1) (EConj₂ h1));
  have h4 := MP h3 h2;
  assumption;
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.left
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'(φ ∨' ψ) →' ¬'φ ∧' ¬'ψ
Tactic:
sorry
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ ∅ ⊢ ¬'φ ∧' ¬'ψ →' ¬'(φ ∨' ψ)
Tactic:
simp [deduction]
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Tactic:
have h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥') := by simp;
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Tactic:
have h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ := by simp;
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Tactic:
have h3 := (EDisj (EConj₁ h1) (EConj₂ h1))
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
h3 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ →' ⊥'
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
h3 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ →' ⊥'
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Tactic:
have h4 := MP h3 h2
Proof state after:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
h3 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ →' ⊥'
h4 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
case a.right
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
h2 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
h3 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ →' ⊥'
h4 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ ⊥'
Tactic:
assumption
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.duMorganConj
Proof state before:
L : Type u
inst✝⁸ : DecidableEq L
inst✝⁷ : HasBot L
inst✝⁶ : HasArrow L
inst✝⁵ : HasLnot L
inst✝⁴ : HasLor L
inst✝³ : HasLand L
inst✝² : HasLiff L
inst✝¹ : HilbertSystem L
inst✝ : HPM L
φ ψ : L
h1 : {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ (φ →' ⊥') ∧' (ψ →' ⊥')
⊢ {(φ →' ⊥') ∧' (ψ →' ⊥')} ∪ {φ ∨' ψ} ⊢ φ ∨' ψ
Tactic:
simp
Proof state after:
no goals
Theorem: PropositionalLogic.HilbertSystem.HPM.strongerThanHPM₀
Proof state before:
L : Type u
inst✝⁷ : DecidableEq L
inst✝⁶ : HilbertSystem L
inst✝⁵ : HasBot L
inst✝⁴ : HasArrow L
inst✝³ : HasLnot L
inst✝² : HasLor L
inst✝¹ : HasLand L
inst✝ : HasLiff L
Γ : Context L
φ : L
⊢ (HPM₀ L → (Γ ⊢ φ)) → HPM L → (Γ ⊢ φ)
Tactic:
admit
Proof state after:
no goals
Theorem: Section6Sheet3solutions.foo
Proof state before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
Tactic:
letI : DistribLattice L := { (show Lattice L by infer_instance) with le_sup_inf := fun x y z => by rw [← h] }
Proof state after:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
this : DistribLattice L :=
  let src :=
    let_fun this := inferInstance;
    this;
  DistribLattice.mk (_ : ∀ (x y z : L), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
Theorem: Section6Sheet3solutions.foo
Proof state before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
this : DistribLattice L :=
  let src :=
    let_fun this := inferInstance;
    this;
  DistribLattice.mk (_ : ∀ (x y z : L), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z)
⊢ ∀ (a b c : L), a ⊓ (b ⊔ c) = a ⊓ b ⊔ a ⊓ c
Tactic:
exact fun a b c => inf_sup_left
Proof state after:
no goals
Theorem: Section6Sheet3solutions.foo
Proof state before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
⊢ Lattice L
Tactic:
infer_instance
Proof state after:
no goals
Theorem: Section6Sheet3solutions.foo
Proof state before:
L : Type
inst✝ : Lattice L
h : ∀ (a b c : L), a ⊔ b ⊓ c = (a ⊔ b) ⊓ (a ⊔ c)
src✝ : Lattice L :=
  let_fun this := inferInstance;
  this
x y z : L
⊢ (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
Tactic:
rw [← h]
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.sum_cubes
Proof state before:
n : ℕ
⊢ ∑ i in range n, ↑i ^ 3 = (↑n * (↑n - 1) / 2) ^ 2
Tactic:
induction' n with d hd
Proof state after:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 3 = (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2

case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ ∑ i in range (Nat.succ d), ↑i ^ 3 = (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2
Theorem: Section15Sheet7Solutions.sum_cubes
Proof state before:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 3 = (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2
Tactic:
simp
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.sum_cubes
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ ∑ i in range (Nat.succ d), ↑i ^ 3 = (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2
Tactic:
rw [Finset.sum_range_succ, hd]
Proof state after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ (↑d * (↑d - 1) / 2) ^ 2 + ↑d ^ 3 = (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2
Theorem: Section15Sheet7Solutions.sum_cubes
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ (↑d * (↑d - 1) / 2) ^ 2 + ↑d ^ 3 = (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2
Tactic:
simp
Proof state after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ (↑d * (↑d - 1)) ^ 2 / 2 ^ 2 + ↑d ^ 3 = ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2
Theorem: Section15Sheet7Solutions.sum_cubes
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 3 = (↑d * (↑d - 1) / 2) ^ 2
⊢ (↑d * (↑d - 1)) ^ 2 / 2 ^ 2 + ↑d ^ 3 = ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2
Tactic:
ring
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.sum_fifths
Proof state before:
n : ℕ
⊢ ∑ i in range n, ↑i ^ 5 = (4 * (↑n * (↑n - 1) / 2) ^ 3 - (↑n * (↑n - 1) / 2) ^ 2) / 3
Tactic:
induction' n with d hd
Proof state after:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 5 =
    (4 * (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 3 - (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2) / 3

case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ ∑ i in range (Nat.succ d), ↑i ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Theorem: Section15Sheet7Solutions.sum_fifths
Proof state before:
case zero

⊢ ∑ i in range Nat.zero, ↑i ^ 5 =
    (4 * (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 3 - (↑Nat.zero * (↑Nat.zero - 1) / 2) ^ 2) / 3
Tactic:
simp
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.sum_fifths
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ ∑ i in range (Nat.succ d), ↑i ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Tactic:
rw [Finset.sum_range_succ, hd]
Proof state after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3 + ↑d ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Theorem: Section15Sheet7Solutions.sum_fifths
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3 + ↑d ^ 5 =
    (4 * (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 3 - (↑(Nat.succ d) * (↑(Nat.succ d) - 1) / 2) ^ 2) / 3
Tactic:
simp
Proof state after:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * ((↑d * (↑d - 1)) ^ 3 / 2 ^ 3) - (↑d * (↑d - 1)) ^ 2 / 2 ^ 2) / 3 + ↑d ^ 5 =
    (4 * (((↑d + 1) * ↑d) ^ 3 / 2 ^ 3) - ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2) / 3
Theorem: Section15Sheet7Solutions.sum_fifths
Proof state before:
case succ
d : ℕ
hd : ∑ i in range d, ↑i ^ 5 = (4 * (↑d * (↑d - 1) / 2) ^ 3 - (↑d * (↑d - 1) / 2) ^ 2) / 3
⊢ (4 * ((↑d * (↑d - 1)) ^ 3 / 2 ^ 3) - (↑d * (↑d - 1)) ^ 2 / 2 ^ 2) / 3 + ↑d ^ 5 =
    (4 * (((↑d + 1) * ↑d) ^ 3 / 2 ^ 3) - ((↑d + 1) * ↑d) ^ 2 / 2 ^ 2) / 3
Tactic:
ring
Proof state after:
no goals
Theorem: Section20Sheet2Solutions.RepMap.comp_id
Proof state before:
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
⊢ comp φ (id ρ) = φ
Tactic:
ext
Proof state after:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp φ (id ρ)).toLinearMap x✝ = φ.toLinearMap x✝
Theorem: Section20Sheet2Solutions.RepMap.comp_id
Proof state before:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp φ (id ρ)).toLinearMap x✝ = φ.toLinearMap x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Section20Sheet2Solutions.RepMap.id_comp
Proof state before:
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
⊢ comp (id σ) φ = φ
Tactic:
ext
Proof state after:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp (id σ) φ).toLinearMap x✝ = φ.toLinearMap x✝
Theorem: Section20Sheet2Solutions.RepMap.id_comp
Proof state before:
case toLinearMap.h
k : Type
inst✝⁷ : Field k
G : Type
inst✝⁶ : Group G
V : Type
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module k V
W : Type
inst✝³ : AddCommGroup W
inst✝² : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝¹ : AddCommGroup X
inst✝ : Module k X
φ : RepMap ρ σ
x✝ : V
⊢ (comp (id σ) φ).toLinearMap x✝ = φ.toLinearMap x✝
Tactic:
rfl
Proof state after:
no goals
Theorem: Section20Sheet2Solutions.RepMap.comp_assoc
Proof state before:
k : Type
inst✝⁹ : Field k
G : Type
inst✝⁸ : Group G
V : Type
inst✝⁷ : AddCommGroup V
inst✝⁶ : Module k V
W : Type
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module k W
ρ : Representation k G V
σ : Representation k G W
X : Type
inst✝³ : AddCommGroup X
inst✝² : Module k X
τ : Representation k G X
Y : Type
inst✝¹ : AddCommGroup Y
inst✝ : Module k Y
υ : Representation k G Y
ξ : RepMap τ υ
ψ : RepMap σ τ
φ : RepMap ρ σ
⊢ comp (comp ξ ψ) φ = comp ξ (comp ψ φ)
Tactic:
rfl
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
n : ℕ
⊢ Nat.factorial n = ∏ i in Finset.Icc 1 n, i
Tactic:
induction' n with d hd
Proof state after:
case zero

⊢ Nat.factorial Nat.zero = ∏ i in Finset.Icc 1 Nat.zero, i

case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ Nat.factorial (Nat.succ d) = ∏ i in Finset.Icc 1 (Nat.succ d), i
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
case zero

⊢ Nat.factorial Nat.zero = ∏ i in Finset.Icc 1 Nat.zero, i
Tactic:
rfl
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ Nat.factorial (Nat.succ d) = ∏ i in Finset.Icc 1 (Nat.succ d), i
Tactic:
rw [Nat.factorial_succ, hd]
Proof state after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = ∏ i in Finset.Icc 1 (Nat.succ d), i
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = ∏ i in Finset.Icc 1 (Nat.succ d), i
Tactic:
rw [Finset.Icc_eq_cons_Ico (show 1 ≤ d + 1 by linarith)]
Proof state after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i =
    ∏ i in Finset.cons (d + 1) (Finset.Ico 1 (d + 1)) (_ : d + 1 ∉ Finset.Ico 1 (d + 1)), i
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i =
    ∏ i in Finset.cons (d + 1) (Finset.Ico 1 (d + 1)) (_ : d + 1 ∉ Finset.Ico 1 (d + 1)), i
Tactic:
rw [Finset.prod_cons]
Proof state after:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = (d + 1) * ∏ x in Finset.Ico 1 (d + 1), x
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
case succ
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ (d + 1) * ∏ i in Finset.Icc 1 d, i = (d + 1) * ∏ x in Finset.Ico 1 (d + 1), x
Tactic:
congr
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.factorial_eq_prod
Proof state before:
d : ℕ
hd : Nat.factorial d = ∏ i in Finset.Icc 1 d, i
⊢ 1 ≤ d + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: Section15Sheet7Solutions.wilson_theorem
Proof state before:
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Tactic:
have := (Nat.prime_iff_fac_equiv_neg_one (?_ : p ≠ 1)).1 hp
Proof state after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1

case refine_1
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
⊢ p ≠ 1
Theorem: Section15Sheet7Solutions.wilson_theorem
Proof state before:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = -1
Tactic:
rw [← this, hn]
Proof state after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n + 1 - 1))
Theorem: Section15Sheet7Solutions.wilson_theorem
Proof state before:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n + 1 - 1))
Tactic:
simp
Proof state after:
case refine_2
p n : ℕ
hp : Nat.Prime p
hn : p = 4 * n + 1
this : ↑(Nat.factorial (p - 1)) = -1
⊢ ∏ j in Finset.Icc 1 (4 * n), ↑j = ↑(Nat.factorial (4 * n))