Theorem: Matrix.conj_hom_prop (Logic/Logic/LogicSymbol.lean)

State before:
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
n : ℕ
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
v : Fin n → α
⊢ f (conj v) = ∀ (i : Fin n), f (v i)
Tactic:
induction' n with n ih <;> simp[conj]
State after:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ f (v 0) ∧ f (conj (vecTail v)) ↔ ∀ (i : Fin (n + 1)), f (v i)

State before:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ f (v 0) ∧ f (conj (vecTail v)) ↔ ∀ (i : Fin (n + 1)), f (v i)
Tactic:
simp[ih]
State after:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) ↔ ∀ (i : Fin (n + 1)), f (v i)

State before:
case succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) ↔ ∀ (i : Fin (n + 1)), f (v i)
Tactic:
constructor
State after:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) → ∀ (i : Fin (n + 1)), f (v i)

case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (∀ (i : Fin (n + 1)), f (v i)) → f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)

State before:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)) → ∀ (i : Fin (n + 1)), f (v i)
Tactic:
intro ⟨hz, hs⟩ i
State after:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i : Fin (n + 1)
⊢ f (v i)

State before:
case succ.mp
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i : Fin (n + 1)
⊢ f (v i)
Tactic:
cases i using Fin.cases
State after:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)

case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)

State before:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)

case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
{ exact hz }
State after:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)

State before:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
{ exact hs _ }
State after:
no goals

State before:
case succ.mp.zero
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
⊢ f (v 0)
Tactic:
exact hz
State after:
no goals

State before:
case succ.mp.succ
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
hz : f (v 0)
hs : ∀ (i : Fin n), f (vecTail v i)
i✝ : Fin n
⊢ f (v i✝.succ)
Tactic:
exact hs _
State after:
no goals

State before:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
⊢ (∀ (i : Fin (n + 1)), f (v i)) → f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Tactic:
intro h
State after:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
h : ∀ (i : Fin (n + 1)), f (v i)
⊢ f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)

State before:
case succ.mpr
β : Type ?u.59199
α : Type u_1
inst✝³ : LogicalConnective α
inst✝² : LogicalConnective β
F : Type u_2
inst✝¹ : FunLike F α Prop
inst✝ : LogicalConnective.HomClass F α Prop
f : F
n : ℕ
ih : ∀ (v : Fin n → α), f (conj v) = ∀ (i : Fin n), f (v i)
v : Fin (n + 1) → α
h : ∀ (i : Fin (n + 1)), f (v i)
⊢ f (v 0) ∧ ∀ (i : Fin n), f (vecTail v i)
Tactic:
exact ⟨h 0, fun i => h _⟩
State after:
no goals