awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
have refine_2 : (↑e : M →L[R] M₂) = 0
Tactic: refine ⟨e, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
hM : Subsingleton M
hM₂ : Subsingleton M₂
e : M ≃L[R] M₂ :=
  { toFun := 0, map_add' := ⋯, map_smul' := ⋯, invFun := 0, left_inv := ⋯, right_inv := ⋯, continuous_toFun := ⋯,
    continuous_invFun := ⋯ }
⊢ (↑e : M →L[R] M₂) = 0
have refine_2 : ∀ (x : M), Eq.{u_3 + 1} (α := M₂) (((↑e : M →L[R] M₂) : (a : M) → M₂) x : M₂) ((0 : (a : M) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0
have pos : ∀ (h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0), Eq (α := M₂ →L[R] M) (inverse 0) 0
Tactic: by_cases h : IsInvertible (0 : M →L[R] M₂)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
pos : ∀ (h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0), Eq (α := M₂ →L[R] M) (inverse 0) 0
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0
have neg : ∀ (h : ¬IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0), Eq (α := M₂ →L[R] M) (inverse 0) 0
Tactic: by_cases h : IsInvertible (0 : M →L[R] M₂)
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0
have hM : Subsingleton M
Tactic: rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0
have hM₂ : Subsingleton M₂
Tactic: rcases isInvertible_zero_iff.1 h with ⟨hM, hM₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
h : IsInvertible.{u_1, u_2, u_3} (R := R) (M := M) (M₂ := M₂) 0
hM : Subsingleton M
hM₂ : Subsingleton M₂
⊢ Eq (α := M₂ →L[R] M) (inverse 0) 0
have pos : ∀ (x : M₂), Eq.{u_2 + 1} (α := M) ((inverse 0 : (a : M₂) → M) x : M) ((0 : (a : M₂) → M) x : M)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
hf : f.IsInvertible
⊢ (g ∘SL f).IsInvertible
have rcases : ∀ (N : M₂ ≃L[R] M₃), ((↑N : M₂ →L[R] M₃) ∘SL f).IsInvertible
Tactic: rcases hg with ⟨N, rfl⟩
Cleared hypotheses: g, hg
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
f : M →L[R] M₂
hf : f.IsInvertible
N : M₂ ≃L[R] M₃
⊢ ((↑N : M₂ →L[R] M₃) ∘SL f).IsInvertible
have rcases : ∀ (M_1 : M ≃L[R] M₂), ((↑N : M₂ →L[R] M₃) ∘SL (↑M_1 : M →L[R] M₂)).IsInvertible
Tactic: rcases hf with ⟨M, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
⊢ f.inverse = g
have this : f = (↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg) : M →L[R] M₂)
Tactic: have : f = ContinuousLinearEquiv.equivOfInverse' f g hf hg := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M →L[R] M₂
g : M₂ →L[R] M
hf : f ∘SL g = ContinuousLinearMap.id R M₂
hg : g ∘SL f = ContinuousLinearMap.id R M
this : f = (↑(ContinuousLinearEquiv.equivOfInverse' f g hf hg) : M →L[R] M₂)
⊢ f.inverse = g
have rw : (↑(ContinuousLinearEquiv.symm (ContinuousLinearEquiv.equivOfInverse' f g hf hg)) : M₂ →L[R] M) = g
Tactic: rw [this, inverse_equiv]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
f : M →L[R] M₂
x : M
y : M₂
hf : f.IsInvertible
⊢ (f.inverse : (a : M₂) → M) y = x ↔ y = (f : (a : M) → M₂) x
have rcases : ∀ (M_1 : M ≃L[R] M₂), ((↑M_1 : M →L[R] M₂).inverse : (a : M₂) → M) y = x ↔ y = ((↑M_1 : M →L[R] M₂) : (a : M) → M₂) x
Tactic: rcases hf with ⟨M, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M_1 : Type u_2
M₂ : Type u_3
inst : TopologicalSpace M_1
inst_1 : TopologicalSpace M₂
inst_2 : Semiring R
inst_3 : AddCommMonoid M_1
inst_4 : Module R M_1
inst_5 : AddCommMonoid M₂
inst_6 : Module R M₂
x : M_1
y : M₂
M : M_1 ≃L[R] M₂
⊢ ((↑M : M_1 →L[R] M₂).inverse : (a : M₂) → M_1) y = x ↔ y = ((↑M : M_1 →L[R] M₂) : (a : M_1) → M₂) x
have simp : (M.symm : (a : M₂) → M_1) y = x ↔ y = (M : (a : M_1) → M₂) x
Tactic: simp only [inverse_equiv, ContinuousLinearEquiv.coe_coe]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible ↔ f.IsInvertible
have mp : ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible → f.IsInvertible
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
mp : ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible → f.IsInvertible
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible ↔ f.IsInvertible
have mpr : f.IsInvertible → ((↑e : M₂ →L[R] M₃) ∘SL f).IsInvertible
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
⊢ f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
    (((↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
⊢ f.IsInvertible
have this : f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f
Tactic: have : f = e.symm ∘L ((e : M₂ →L[R] M₃) ∘L f) := by ext; simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
A : M ≃L[R] M₃
hA : (↑A : M →L[R] M₃) = (↑e : M₂ →L[R] M₃) ∘SL f
this : f = (↑e.symm : M₃ →L[R] M₂) ∘SL (↑e : M₂ →L[R] M₃) ∘SL f
⊢ f.IsInvertible
have mp : ((↑e.symm : M₃ →L[R] M₂) ∘SL (↑A : M →L[R] M₃)).IsInvertible
Tactic: rw [this, ← hA]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible ↔ f.IsInvertible
have mp : (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible → f.IsInvertible
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
mp : (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible → f.IsInvertible
⊢ (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible ↔ f.IsInvertible
have mpr : f.IsInvertible → (f ∘SL (↑e : M₃ →L[R] M)).IsInvertible
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
⊢ f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)
have h : ∀ (x : M),
  Eq.{u_3 + 1} (α := M₂) ((f : (a : M) → M₂) x : M₂)
    (((f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃) : (a : M) → M₂) x : M₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
⊢ f.IsInvertible
have this : f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)
Tactic: have : f = (f ∘L (e : M₃ →L[R] M)) ∘L e.symm := by ext; simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
A : M₃ ≃L[R] M₂
hA : (↑A : M₃ →L[R] M₂) = f ∘SL (↑e : M₃ →L[R] M)
this : f = (f ∘SL (↑e : M₃ →L[R] M)) ∘SL (↑e.symm : M →L[R] M₃)
⊢ f.IsInvertible
have mp : ((↑A : M₃ →L[R] M₂) ∘SL (↑e.symm : M →L[R] M₃)).IsInvertible
Tactic: rw [this, ← hA]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have pos : ∀ (hf : f.IsInvertible), ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
Tactic: by_cases hf : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
pos : ∀ (hf : f.IsInvertible), ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have neg : ∀ (hf : ¬f.IsInvertible), ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
Tactic: by_cases hf : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : f.IsInvertible
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have pos : ∀ (A : M ≃L[R] M₂),
  ((↑e : M₂ →L[R] M₃) ∘SL (↑A : M →L[R] M₂)).inverse = (↑A : M →L[R] M₂).inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
Tactic: rcases hf with ⟨A, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
A : M ≃L[R] M₂
⊢ ((↑e : M₂ →L[R] M₃) ∘SL (↑A : M →L[R] M₂)).inverse = (↑A : M →L[R] M₂).inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have pos : Eq (α := M₃ ≃L[R] M) (ContinuousLinearEquiv.symm (A.trans e)) (e.symm.trans A.symm)
Tactic: simp only [ContinuousLinearEquiv.comp_coe, inverse_equiv, ContinuousLinearEquiv.coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have neg : 0 = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, zero_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have neg₁ : Eq (α := M₃ →L[R] M) 0 (comp (σ₂₃ := RingHom.id R) 0 (↑e.symm : M₃ →L[R] M₂))
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, zero_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₂ ≃L[R] M₃
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
neg₁ : Eq (α := M₃ →L[R] M) 0 (comp (σ₂₃ := RingHom.id R) 0 (↑e.symm : M₃ →L[R] M₂))
⊢ ((↑e : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑e.symm : M₃ →L[R] M₂)
have neg₂ : Eq (α := M₃ →L[R] M) 0 0
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, zero_comp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have pos : ∀ (hf : f.IsInvertible), (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
Tactic: by_cases hf : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
pos : ∀ (hf : f.IsInvertible), (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have neg : ∀ (hf : ¬f.IsInvertible), (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
Tactic: by_cases hf : f.IsInvertible
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : f.IsInvertible
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have pos : ∀ (A : M ≃L[R] M₂),
  ((↑A : M →L[R] M₂) ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL (↑A : M →L[R] M₂).inverse
Tactic: rcases hf with ⟨A, rfl⟩
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
A : M ≃L[R] M₂
⊢ ((↑A : M →L[R] M₂) ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL (↑A : M →L[R] M₂).inverse
have pos : Eq (α := M₂ ≃L[R] M₃) (ContinuousLinearEquiv.symm (e.trans A)) (A.symm.trans e.symm)
Tactic: simp only [ContinuousLinearEquiv.comp_coe, inverse_equiv, ContinuousLinearEquiv.coe_inj]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have neg : 0 = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, comp_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have neg₁ : Eq (α := M₂ →L[R] M₃) 0 ((↑e.symm : M →L[R] M₃).comp (σ₁₂ := RingHom.id R) 0)
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, comp_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
e : M₃ ≃L[R] M
f : M →L[R] M₂
hf : ¬f.IsInvertible
neg : 0 = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
neg₁ : Eq (α := M₂ →L[R] M₃) 0 ((↑e.symm : M →L[R] M₃).comp (σ₁₂ := RingHom.id R) 0)
⊢ (f ∘SL (↑e : M₃ →L[R] M)).inverse = (↑e.symm : M →L[R] M₃) ∘SL f.inverse
have neg₂ : Eq (α := M₂ →L[R] M₃) 0 0
Tactic: rw [inverse_of_not_isInvertible (by simp [hf]), inverse_of_not_isInvertible hf, comp_zero]
-- Lean 4 proof step from Mathlib.Topology.Algebra.Module.Equiv (goal)
Goal:
R : Type u_1
M : Type u_2
M₂ : Type u_3
M₃ : Type u_4
inst : TopologicalSpace M
inst_1 : TopologicalSpace M₂
inst_2 : TopologicalSpace M₃
inst_3 : Semiring R
inst_4 : AddCommMonoid M
inst_5 : Module R M
inst_6 : AddCommMonoid M₂
inst_7 : Module R M₂
inst_8 : AddCommMonoid M₃
inst_9 : Module R M₃
g : M₂ →L[R] M₃
f : M →L[R] M₂
hg : g.IsInvertible
⊢ (g ∘SL f).inverse = f.inverse ∘SL g.inverse
have rcases : ∀ (N : M₂ ≃L[R] M₃), ((↑N : M₂ →L[R] M₃) ∘SL f).inverse = f.inverse ∘SL (↑N : M₂ →L[R] M₃).inverse
Tactic: rcases hg with ⟨N, rfl⟩
Cleared hypotheses: g, hg