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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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 (Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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 (Finsupp.equivFunOnFinite.symm e) ↔ q ((Finsupp.equivFunOnFinite.symm e) 0) ((Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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 (Finsupp.equivFunOnFinite.symm e) ↔ q ((Finsupp.equivFunOnFinite.symm e) 0) ((Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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
      (Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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
      (Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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
      (Finsupp.equivFunOnFinite.symm fun x =>
        match x with
        | 0 => u
        | 1 => v) ↔
    q u v
⊢ p
    (Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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
      (Finsupp.equivFunOnFinite.symm fun x =>
        match x with
        | 0 => u
        | 1 => v) ↔
    q u v
⊢ p
    (Finsupp.equivFunOnFinite.symm 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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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
inst✝ : Zero α
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