Theorem: PowerSeries.forall_congr_curry (DividedPowers/ExponentialModule/Basic.lean)

State before:
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) ↔ ∀ (u v : α), q u v
Tactic:
constructor
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) → ∀ (u v : α), q u v

case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (u v : α), q u v) → ∀ (e : Fin 2 → α), p e

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (e : Fin 2 → α), p e) → ∀ (u v : α), q u v
Tactic:
intro H u v
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
⊢ q u v

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
⊢ q u v
Tactic:
set e : Fin 2 → α := fun
| 0 => u
| 1 => v
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u v

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
⊢ q u v
Tactic:
specialize hpq e
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq : p e ↔ q (e 0) (e 1)
⊢ q u v

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq : p e ↔ q (e 0) (e 1)
⊢ q u v
Tactic:
simp [e] at hpq
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  (p fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ q u v

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  (p fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ q u v
Tactic:
rw [← hpq]
State after:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  (p fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ p fun x =>
    match x with
    | 0 => u
    | 1 => v

State before:
case mp
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
H : ∀ (e : Fin 2 → α), p e
u v : α
e : Fin 2 → α :=
  fun x =>
    match x with
    | 0 => u
    | 1 => v
hpq :
  (p fun x =>
      match x with
      | 0 => u
      | 1 => v) ↔
    q u v
⊢ p fun x =>
    match x with
    | 0 => u
    | 1 => v
Tactic:
apply H
State after:
no goals

State before:
case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
⊢ (∀ (u v : α), q u v) → ∀ (e : Fin 2 → α), p e
Tactic:
intro H e
State after:
case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 → α
⊢ p e

State before:
case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 → α
⊢ p e
Tactic:
rw [hpq]
State after:
case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 → α
⊢ q (e 0) (e 1)

State before:
case mpr
A : Type u_1
inst✝⁴ : CommRing A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Algebra A R
S : Type u_3
inst✝¹ : CommRing S
inst✝ : Algebra A S
α : Type u_4
p : (Fin 2 → α) → Prop
q : α → α → Prop
hpq : ∀ (e : Fin 2 → α), p e ↔ q (e 0) (e 1)
H : ∀ (u v : α), q u v
e : Fin 2 → α
⊢ q (e 0) (e 1)
Tactic:
apply H
State after:
no goals