awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)
have rw : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
  (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
        (a : R) → Q)
      c :
    Q)
Tactic: rw [← ContinuousAffineMap.coe_toAffineMap, AffineMap.apply_lineMap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
rw :
  Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
          (a : R) → Q)
        c :
      Q)
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((AffineMap.lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)
have rw₁ : Eq.{u_5 + 1} (α := Q)
  (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
        (a : R) → Q)
      c :
    Q)
  (((AffineMap.lineMap (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₀) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p₁) : R →ᵃ[R] Q) :
        (a : R) → Q)
      c :
    Q)
Tactic: rw [← ContinuousAffineMap.coe_toAffineMap, AffineMap.apply_lineMap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace R
inst_10 : TopologicalSpace V
inst_11 : TopologicalSpace W
inst_12 : ContinuousSMul R V
inst_13 : ContinuousSMul R W
inst_14 : ContinuousVAdd V P
inst_15 : ContinuousVAdd W Q
f : P →ᴬ[R] Q
p₀ p₁ : P
c : R
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
    (((lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᴬ[R] Q) : (a : R) → Q) c : Q)
have simp_rw : Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) ((AffineMap.lineMap p₀ p₁ : (a : R) → P) c : P) : Q)
  (((AffineMap.lineMap ((f : (a : P) → Q) p₀) ((f : (a : P) → Q) p₁) : R →ᵃ[R] Q) : (a : R) → Q) c : Q)
Tactic: simp_rw [coe_lineMap_eq, apply_lineMap]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
inst_13 : TopologicalSpace V
inst_14 : IsTopologicalAddTorsor P
inst_15 : TopologicalSpace W
inst_16 : IsTopologicalAddTorsor Q
inst_17 : TopologicalSpace W₂
inst_18 : IsTopologicalAddTorsor Q₂
f : P →ᴬ[R] Q
⊢ Continuous.{u_2, u_3} (X := V) (Y := W) (⇑(↑f : P →ᵃ[R] Q).linear : (a : V) → W)
have rw : Continuous.{u_4, u_5} (X := P) (Y := Q) (⇑(↑f : P →ᵃ[R] Q) : (a : P) → Q)
Tactic: rw [AffineMap.continuous_linear_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
have refine_1 : ∀ (h : Eq (α := V →L[R] W) f.contLinear 0), (↑f : P →ᵃ[R] Q).linear = 0
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
refine_1 : ∀ (h : Eq (α := V →L[R] W) f.contLinear 0), (↑f : P →ᵃ[R] Q).linear = 0
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
have refine_2 : ∀ (h : (↑f : P →ᵃ[R] Q).linear = 0), Eq (α := V →L[R] W) f.contLinear 0
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : Eq (α := V →L[R] W) f.contLinear 0
⊢ (↑f : P →ᵃ[R] Q).linear = 0
have refine_1 : ∀ (x : V), Eq.{u_3 + 1} (α := W) (((↑f : P →ᵃ[R] Q).linear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f : P →ᵃ[R] Q).linear = 0
⊢ Eq (α := V →L[R] W) f.contLinear 0
have refine_2 : ∀ (x : V), Eq.{u_3 + 1} (α := W) ((f.contLinear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : Eq (α := V →L[R] W) f.contLinear 0
x : V
⊢ Eq.{u_3 + 1} (α := W) (((↑f : P →ᵃ[R] Q).linear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
have refine_1 : Eq.{u_3 + 1} (α := W) (((↑0 : V →ₗ[R] W) : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
Tactic: rw [← coe_contLinear_eq_linear, h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h : (↑f : P →ᵃ[R] Q).linear = 0
x : V
⊢ Eq.{u_3 + 1} (α := W) ((f.contLinear : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
have refine_2 : Eq.{u_3 + 1} (α := W) ((0 : (a : V) → W) x : W) ((0 : (a : V) → W) x : W)
Tactic: rw [← coe_linear_eq_coe_contLinear, h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (hypothesis)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ ∃ (q : Q), f = const R P q
have h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
Tactic: have h₁ : f.contLinear = 0 ↔ (f : P →ᵃ[R] Q).linear = 0 := by
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [← coe_contLinear_eq_linear, h]; rfl
    · rw [← coe_linear_eq_coe_contLinear, h]; rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
⊢ f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
have refine_1 : ∀ (h : f = const R P q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
refine_1 : ∀ (h : f = const R P q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
have refine_2 : ∀ (h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q), f = const R P q
Tactic: refine ⟨fun h => ?_, fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : f = const R P q
⊢ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
have refine_1 : ∀ (p : P), Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p : Q) ((AffineMap.const R P q : (a : P) → Q) p : Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ f = const R P q
have refine_2 : ∀ (x : P), Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : f = const R P q
p : P
⊢ Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) p : Q) ((AffineMap.const R P q : (a : P) → Q) p : Q)
have refine_1 : Eq.{u_5 + 1} (α := Q) (((↑(const R P q) : P →ᵃ[R] Q) : (a : P) → Q) p : Q) ((AffineMap.const R P q : (a : P) → Q) p : Q)
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
have refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
Tactic: rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
have refine_2₁ : Eq.{u_5 + 1} (α := Q) ((AffineMap.const R P q : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
Tactic: rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₁ : Eq.{u_5 + 1} (α := Q) ((AffineMap.const R P q : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
have refine_2₂ : q = (const R P q : (a : P) → Q) x
Tactic: rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₁ : Eq.{u_5 + 1} (α := Q) ((AffineMap.const R P q : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₂ : q = (const R P q : (a : P) → Q) x
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
have refine_2₃ : q = Function.const P q x
Tactic: rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
q : Q
h : (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
x : P
refine_2 : Eq.{u_5 + 1} (α := Q) (((↑f : P →ᵃ[R] Q) : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₁ : Eq.{u_5 + 1} (α := Q) ((AffineMap.const R P q : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
refine_2₂ : q = (const R P q : (a : P) → Q) x
refine_2₃ : q = Function.const P q x
⊢ Eq.{u_5 + 1} (α := Q) ((f : (a : P) → Q) x : Q) ((const R P q : (a : P) → Q) x : Q)
have refine_2₄ : q = q
Tactic: rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (hypothesis)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ ∃ (q : Q), f = const R P q
have h₂ : ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
Tactic: have h₂ : ∀ q : Q, f = const R P q ↔ (f : P →ᵃ[R] Q) = AffineMap.const R P q := by
    intro q
    refine ⟨fun h => ?_, fun h => ?_⟩ <;> ext
    · rw [h]; rfl
    · rw [← coe_toAffineMap, h, AffineMap.const_apply, coe_const, Function.const_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
inst_9 : TopologicalSpace V
inst_10 : IsTopologicalAddTorsor P
inst_11 : TopologicalSpace W
inst_12 : IsTopologicalAddTorsor Q
f : P →ᴬ[R] Q
h₁ : Eq (α := V →L[R] W) f.contLinear 0 ↔ (↑f : P →ᵃ[R] Q).linear = 0
h₂ : ∀ (q : Q), f = const R P q ↔ (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
⊢ Eq (α := V →L[R] W) f.contLinear 0 ↔ ∃ (q : Q), f = const R P q
have simp_rw : (↑f : P →ᵃ[R] Q).linear = 0 ↔ ∃ (q : Q), (↑f : P →ᵃ[R] Q) = AffineMap.const R P q
Tactic: simp_rw [h₁, h₂]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst_13 : Ring k
inst_14 : AddCommGroup V₁
inst_15 : Module k V₁
inst_16 : AddTorsor V₁ P₁
inst_17 : TopologicalSpace P₁
inst_18 : AddCommGroup V₂
inst_19 : Module k V₂
inst_20 : AddTorsor V₂ P₂
inst_21 : TopologicalSpace P₂
inst_22 : AddCommGroup V₃
inst_23 : Module k V₃
inst_24 : AddTorsor V₃ P₃
inst_25 : TopologicalSpace P₃
inst_26 : AddCommGroup V₄
inst_27 : Module k V₄
inst_28 : AddTorsor V₄ P₄
inst_29 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₁ →ᴬ[k] P₃
⊢ Continuous (Y := P₂ × P₃) fun (a : P₁) ↦ ((↑f : P₁ →ᵃ[k] P₂).prod (↑g : P₁ →ᵃ[k] P₃)).toFun a
have dsimp : Continuous (Y := P₂ × P₃) fun (a : P₁) ↦ ((f : (a : P₁) → P₂) a, (g : (a : P₁) → P₃) a)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
P : Type u_4
Q : Type u_5
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace P
inst_4 : AddTorsor V P
inst_5 : AddCommGroup W
inst_6 : Module R W
inst_7 : TopologicalSpace Q
inst_8 : AddTorsor W Q
W₂ : Type u_6
Q₂ : Type u_7
W₃ : Type u_8
Q₃ : Type u_9
inst_9 : AddCommGroup W₂
inst_10 : Module R W₂
inst_11 : TopologicalSpace Q₂
inst_12 : AddTorsor W₂ Q₂
k : Type u_10
P₁ : Type u_11
P₂ : Type u_12
P₃ : Type u_13
P₄ : Type u_14
V₁ : Type u_15
V₂ : Type u_16
V₃ : Type u_17
V₄ : Type u_18
inst_13 : Ring k
inst_14 : AddCommGroup V₁
inst_15 : Module k V₁
inst_16 : AddTorsor V₁ P₁
inst_17 : TopologicalSpace P₁
inst_18 : AddCommGroup V₂
inst_19 : Module k V₂
inst_20 : AddTorsor V₂ P₂
inst_21 : TopologicalSpace P₂
inst_22 : AddCommGroup V₃
inst_23 : Module k V₃
inst_24 : AddTorsor V₃ P₃
inst_25 : TopologicalSpace P₃
inst_26 : AddCommGroup V₄
inst_27 : Module k V₄
inst_28 : AddTorsor V₄ P₄
inst_29 : TopologicalSpace P₄
f : P₁ →ᴬ[k] P₂
g : P₃ →ᴬ[k] P₄
⊢ Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((↑f : P₁ →ᵃ[k] P₂).prodMap (↑g : P₃ →ᵃ[k] P₄)).toFun a
have dsimp : Continuous (Y := P₂ × P₄) fun (a : P₁ × P₃) ↦ ((f : (a : P₁) → P₂) a.1, (g : (a : P₃) → P₄) a.2)
Tactic: dsimp
-- Lean 4 proof step from Mathlib.Topology.Algebra.ContinuousAffineMap (goal)
Goal:
R : Type u_1
V : Type u_2
W : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : TopologicalSpace V
inst_4 : AddCommGroup W
inst_5 : Module R W
inst_6 : TopologicalSpace W
inst_7 : IsTopologicalAddGroup V
inst_8 : IsTopologicalAddGroup W
f : V →ᴬ[R] W
⊢ (⇑f : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W) ((⇑f.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V ((f : (a : V) → W) 0) : V → W)
have rcases : ∀ (f : V →ᵃ[R] W) (h : Continuous f.toFun),
  (⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) =
    HAdd.hAdd (α := (a : V) → W) (β := V → W)
      ((⇑{ toAffineMap := f, cont := h : V →ᴬ[R] W }.contLinear : (a : V) → W) : (a : V) → W)
      (Function.const V (({ toAffineMap := f, cont := h : V →ᴬ[R] W } : (a : V) → W) 0) : V → W)
Tactic: rcases f with ⟨f, h⟩
Cleared hypotheses: f