mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case mp
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) →
    τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}

pp: case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
·

Goal state after:
case mp
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ (∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ) →
    τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'}
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ

Tactic:
·

Goal state after:
case mpr
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁸ : Semiring R
inst✝⁷ : Semiring S
σ : R →+* S
σ' : S →+* R
inst✝⁶ : RingHomInvPair σ σ'
inst✝⁵ : RingHomInvPair σ' σ
A : Type u_3
inst✝⁴ : AddCommMonoid A
inst✝³ : Module R A
τA : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommMonoid B'
inst✝ : Module S B'
τB' : TopologicalSpace B'
hσ : Continuous ⇑σ
hσ' : Continuous ⇑σ'
e : A ≃SL[σ] B'
g : A →ₛₗ[σ] B' := ⋯
g' : B' →ₛₗ[σ'] A := ⋯
h : A →+ B' := ⋯
h' : B' →+ A := ⋯
τ : TopologicalSpace B'
⊢ τ ∈ {t | ContinuousSMul S B' ∧ ContinuousAdd B'} →
    ∃ x ∈ {t | ContinuousSMul R A ∧ ContinuousAdd A}, TopologicalSpace.induced (⇑e.toHomeomorph.symm) x = τ
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case hg
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun rs ↦ rs.1 • rs.2

pp: case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)

Tactic:
·

Goal state after:
case hg
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun rs ↦ rs.1 • rs.2
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)

Tactic:
·

Goal state after:
case hf
R : Type u_1
inst✝¹ : Semiring R
τR : TopologicalSpace R
inst✝ : IsTopologicalSemiring R
⊢ Continuous fun r ↦ (r, 1)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_1
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul S B'

pp: case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B'

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousSMul S B'
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B'

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
S : Type u_2
τR : TopologicalSpace R
τS : TopologicalSpace S
inst✝⁷ : Ring R
inst✝⁶ : Ring S
A : Type u_3
inst✝⁵ : AddCommGroup A
inst✝⁴ : Module R A
inst✝³ : TopologicalSpace A
inst✝² : IsModuleTopology R A
B' : Type u_5
inst✝¹ : AddCommGroup B'
inst✝ : Module S B'
σ : R →+* S
hσ : IsOpenQuotientMap ⇑σ
φ : A →ₛₗ[σ] B'
hφ : Function.Surjective ⇑φ
this✝ : ContinuousAdd A
this : TopologicalSpace B' := TopologicalSpace.coinduced (⇑φ) inferInstance
hφo : IsOpenQuotientMap ⇑φ
⊢ ContinuousAdd B'
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case of_equiv
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
α✝ β✝ : Type u_2
a✝¹ : α✝ ≃ β✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : β✝ → Type u_3
inst✝³ : (i : β✝) → AddCommMonoid (A i)
inst✝² : (i : β✝) → Module R (A i)
inst✝¹ : (i : β✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : β✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : β✝) → A i)

pp: case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
·

Goal state after:
case of_equiv
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
α✝ β✝ : Type u_2
a✝¹ : α✝ ≃ β✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : β✝ → Type u_3
inst✝³ : (i : β✝) → AddCommMonoid (A i)
inst✝² : (i : β✝) → Module R (A i)
inst✝¹ : (i : β✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : β✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : β✝) → A i)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)

pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
·

Goal state after:
case h_empty
R : Type u_1
inst✝⁶ : TopologicalSpace R
inst✝⁵ : Semiring R
ι : Type u_2
inst✝⁴ : Finite ι
A : PEmpty.{u_2 + 1} → Type u_3
inst✝³ : (i : PEmpty.{u_2 + 1}) → AddCommMonoid (A i)
inst✝² : (i : PEmpty.{u_2 + 1}) → Module R (A i)
inst✝¹ : (i : PEmpty.{u_2 + 1}) → TopologicalSpace (A i)
inst✝ : ∀ (i : PEmpty.{u_2 + 1}), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : PEmpty.{u_2 + 1}) → A i)
Module: Mathlib.Topology.Algebra.Module.ModuleTopology

Goal state before:
pp: case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)

Tactic:
·

Goal state after:
case h_option
R : Type u_1
inst✝⁷ : TopologicalSpace R
inst✝⁶ : Semiring R
ι : Type u_2
inst✝⁵ : Finite ι
α✝ : Type u_2
inst✝⁴ : Fintype α✝
a✝ :
  ∀ {A : α✝ → Type u_3} [inst : (i : α✝) → AddCommMonoid (A i)] [inst_1 : (i : α✝) → Module R (A i)]
    [inst_2 : (i : α✝) → TopologicalSpace (A i)] [∀ (i : α✝), IsModuleTopology R (A i)],
    IsModuleTopology R ((i : α✝) → A i)
A : Option α✝ → Type u_3
inst✝³ : (i : Option α✝) → AddCommMonoid (A i)
inst✝² : (i : Option α✝) → Module R (A i)
inst✝¹ : (i : Option α✝) → TopologicalSpace (A i)
inst✝ : ∀ (i : Option α✝), IsModuleTopology R (A i)
⊢ IsModuleTopology R ((i : Option α✝) → A i)
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mp
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe

pp: case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe

Tactic:
·

Goal state after:
case mp
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ Set.range DFunLike.coe → f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe
Module: Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic

Goal state before:
pp: case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe

Tactic:
·

Goal state after:
case mpr
R₁ : Type u_1
R₂ : Type u_2
inst✝⁷ : Semiring R₁
inst✝⁶ : Semiring R₂
σ₁₂ : R₁ →+* R₂
M₁ : Type u_4
inst✝⁵ : TopologicalSpace M₁
inst✝⁴ : AddCommMonoid M₁
M₂ : Type u_6
inst✝³ : TopologicalSpace M₂
inst✝² : AddCommMonoid M₂
inst✝¹ : Module R₁ M₁
inst✝ : Module R₂ M₂
f : M₁ → M₂
⊢ f ∈ {f | Continuous[inst✝⁵, inst✝³] f} ∩ Set.range DFunLike.coe → f ∈ Set.range DFunLike.coe
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom (F ≫ D₂.ι)) ∘ ⇑(ConcreteCategory.hom D₁.π) =
    ⇑(ConcreteCategory.hom D₂.p) ∘ ⇑(ConcreteCategory.hom D₁.i)

pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
·

Goal state after:
case refine_1
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom (F ≫ D₂.ι)) ∘ ⇑(ConcreteCategory.hom D₁.π) =
    ⇑(ConcreteCategory.hom D₂.p) ∘ ⇑(ConcreteCategory.hom D₁.i)
Module: Mathlib.Algebra.Category.ModuleCat.Topology.Homology

Goal state before:
pp: case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)

Tactic:
·

Goal state after:
case refine_2
R : Type u
inst✝¹ : Ring R
inst✝ : TopologicalSpace R
M N : TopModuleCat R
φ : M ⟶ N
S : ShortComplex (TopModuleCat R)
D₁ : S.LeftHomologyData :=
  { K := ker S.g, H := coker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), i := kerι S.g,
    π := cokerπ ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)), wi := ⋯, hi := isLimitKer S.g, wπ := ⋯,
    hπ := isColimitCoker ((isLimitKer S.g).lift (KernelFork.ofι S.f ⋯)) }
D₂ : S.RightHomologyData :=
  { Q := coker S.f, H := ker ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), p := cokerπ S.f,
    ι := kerι ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)), wp := ⋯, hp := isColimitCoker S.f, wι := ⋯,
    hι := isLimitKer ((isColimitCoker S.f).desc (CokernelCofork.ofπ S.g ⋯)) }
F : D₁.H ⟶ D₂.H := ShortComplex.leftRightHomologyComparison' D₁ D₂
hF : Function.Bijective ⇑(ConcreteCategory.hom F)
⊢ ⇑(ConcreteCategory.hom D₂.p) ⁻¹' ⇑(ConcreteCategory.hom D₂.p) '' Set.range ⇑(ConcreteCategory.hom D₁.i) ⊆
    Set.range ⇑(ConcreteCategory.hom D₁.i)
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case f
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ Prequotient F → ↑s.pt

pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → ?f a = ?f b

Tactic:
·

Goal state after:
case f
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ Prequotient F → ↑s.pt
Module: Mathlib.Algebra.Category.MonCat.Colimits

Goal state before:
pp: case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b

Tactic:
·

Goal state after:
case a
J : Type v
inst✝ : Category.{u, v} J
F : J ⥤ MonCat
s : Cocone F
⊢ ∀ (a b : Prequotient F), (colimitSetoid F) a b → descFunLift F s a = descFunLift F s b
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a

pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))

Tactic:
·

Goal state after:
case mp
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ Epi (ofHom (algebraMap R S)) → ∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a
Module: Mathlib.Algebra.Category.Ring.Epi

Goal state before:
pp: case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))

Tactic:
·

Goal state after:
case mpr
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
⊢ (∀ (a : S), a ⊗ₜ[R] 1 = 1 ⊗ₜ[R] a) → Epi (ofHom (algebraMap R S))
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_1
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂

pp: case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
·

Goal state after:
case refine_1
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝ : IsInvertible 0
e : M ≃L[R] M₂
he : ↑e = 0
⊢ Subsingleton M ∧ Subsingleton M₂
Module: Mathlib.Topology.Algebra.Module.Equiv

Goal state before:
pp: case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0

Tactic:
·

Goal state after:
case refine_2
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁶ : TopologicalSpace M
inst✝⁵ : TopologicalSpace M₂
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ Subsingleton M ∧ Subsingleton M₂ → IsInvertible 0