mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I : (FractionalIdeal R⁰ (FractionRing R))ˣ
⊢ mk0 ⟨integralRep ↑I, ⋯⟩ = (mk (FractionRing R)) I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
⊢ Function.Surjective ⇑mk0

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
x✝ : ∃ x, spanSingleton R⁰ ↑x = ↑I
x : Kˣ
hx : spanSingleton R⁰ ↑x = ↑I
⊢ ↑↑I = R ∙ ↑x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
hI : (↑↑I).IsPrincipal
x : K
hx : ↑↑I = R ∙ x
⊢ ↑I = spanSingleton R⁰ x

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDomain R
I : (FractionalIdeal R⁰ K)ˣ
⊢ (mk K) I = 1 ↔ (↑↑I).IsPrincipal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : Field K
inst✝⁴ : Algebra R K
inst✝³ : IsFractionRing R K
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : FractionalIdeal R⁰ K
hI : (↑(I ^ n)).IsPrincipal
⊢ (↑I).IsPrincipal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : FractionalIdeal R⁰ K
hI : IsUnit I
⊢ (↑I).IsPrincipal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : Ideal R
hI : IsUnit ↑I
hsub : (↑↑I).IsPrincipal
⊢ (coeSubmodule K I).IsPrincipal

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : Subsingleton (ClassGroup R)
I : Ideal R
hI : IsUnit ↑I
⊢ Submodule.IsPrincipal I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
n : ℕ
hn : n.Coprime (Fintype.card (ClassGroup R))
I : Ideal R
hI : Submodule.IsPrincipal (I ^ n)
⊢ Submodule.IsPrincipal I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsDedekindDomain R
I J : ↥(Ideal R)⁰
⊢ mk0 I = (mk0 J)⁻¹ ↔ ∃ x, x ≠ 0 ∧ ↑I * ↑J = Ideal.span {x}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Field K
inst✝³ : Algebra R K
inst✝² : IsFractionRing R K
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ ∀ (x : ClassGroup R), x ∈ {1}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
⊢ Fintype.card (ClassGroup R) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : IsDedekindDomain R
inst✝ : Fintype (ClassGroup R)
⊢ Fintype.card (ClassGroup R) = 1 ↔ IsPrincipalIdealRing R

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
N : Type u_2
M : Type uM
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
f : M →ₗ[R] N
inst✝ : Module.FinitePresentation R N
H : ∀ (I : Ideal R) (x : I.IsMaximal), ∃ g, (LocalizedModule.map I.primeCompl) f ∘ₗ g = id
⊢ ∃ g, f ∘ₗ g = id

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
⊢ Module.Finite R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
s : Finset M
hs : Submodule.span R ↑s = ⊤
N : Type (max u_1 uM) := ↥s →₀ R
f : N →ₗ[R] M := Finsupp.linearCombination R Subtype.val
⊢ Function.Surjective ⇑f

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Localization.AtPrime I) (LocalizedModule I.primeCompl M)
inst✝ : FinitePresentation R M
⊢ Projective R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
I : (FractionalIdeal S⁰ L)ˣ
x✝ : ∃ x, spanSingleton S⁰ ↑x = ↑I
u : Lˣ
hu : spanSingleton S⁰ ↑u = ↑I
⊢ (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)) ((Units.mapEquiv (ringEquivOfRingEquiv K L f).symm.toMulEquiv) I) = I

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.LocalProperties.Projective

Goal state before:
pp: R : Type u_1
M : Type uM
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup M
inst✝⁸ : Module R M
Rₚ : (P : Ideal R) → [P.IsMaximal] → Type u_4
inst✝⁷ : (P : Ideal R) → [inst : P.IsMaximal] → CommRing (Rₚ P)
inst✝⁶ : (P : Ideal R) → [inst : P.IsMaximal] → Algebra R (Rₚ P)
inst✝⁵ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalization.AtPrime (Rₚ P) P
Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5
inst✝⁴ : (P : Ideal R) → [inst : P.IsMaximal] → AddCommGroup (Mₚ P)
inst✝³ : (P : Ideal R) → [inst : P.IsMaximal] → Module R (Mₚ P)
inst✝² : (P : Ideal R) → [inst : P.IsMaximal] → Module (Rₚ P) (Mₚ P)
inst✝¹ : ∀ (P : Ideal R) [inst : P.IsMaximal], IsScalarTower R (Rₚ P) (Mₚ P)
f : (P : Ideal R) → [inst : P.IsMaximal] → M →ₗ[R] Mₚ P
inst : ∀ (P : Ideal R) [inst : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)
H : ∀ (I : Ideal R) (x : I.IsMaximal), Projective (Rₚ I) (Mₚ I)
inst✝ : FinitePresentation R M
⊢ Projective R M

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.ClassGroup.Basic

Goal state before:
pp: R : Type u_1
K : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : Field K
inst✝⁷ : Algebra R K
inst✝⁶ : IsFractionRing R K
inst✝⁵ : IsDomain R
S : Type u_3
L : Type u_4
inst✝⁴ : CommRing S
inst✝³ : IsDomain S
inst✝² : Field L
inst✝¹ : Algebra S L
inst✝ : IsFractionRing S L
f : R ≃+* S
⊢ Subgroup.map (Units.mapEquiv ↑(ringEquivOfRingEquiv K L f)).toMonoidHom (toPrincipalIdeal R K).range =
    (toPrincipalIdeal S L).range

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
h : ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
tfae_1_to_4 : IsLocallyConstant f → ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})
tfae_4_to_3 : (∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y})) → ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}
tfae_3_to_2 : (∀ (x : X), IsOpen[inst✝] {x' | f x' = f x}) → ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x
tfae_2_to_5 :
  (∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x) → ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
h : ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x
s : Set Y
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
⊢ [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in 𝓝 x, f x' = f x, ∀ (x : X), IsOpen[inst✝] {x' | f x' = f x},
      ∀ (y : Y), IsOpen[inst✝] (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
g : Y → Z
s : Set Z
⊢ IsOpen[inst✝] (g ∘ f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
g : Y → Z
f : X → Y
hg : IsLocallyConstant g
hf : Continuous[inst✝¹, inst✝] f
s : Set Z
⊢ IsOpen[inst✝¹] (g ∘ f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
hf : IsLocallyConstant f
s : Set X
hs : IsPreconnected s
x y : X
hx : x ∈ s
hy : y ∈ s
⊢ f x = f y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : X → Y
hf : IsLocallyConstant f
⊢ ∃ y, f = Function.const X y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : CompactSpace X
f : X → Y
hf : IsLocallyConstant f
⊢ (range f).Finite

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
α : Type u_5
β : Type u_6
f : X → α
g : α → β
h : IsLocallyConstant (g ∘ f)
inj : Function.Injective g
s : Set α
⊢ IsOpen[inst✝] (f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
⊢ Function.Injective LocallyConstant.toFun

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ IsLocallyConstant fun x ↦ if x ∈ U then 0 else 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {0} = U

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝¹ : TopologicalSpace X
U : Set X
inst✝ : (x : X) → Decidable (x ∈ U)
hU : IsClopen U
⊢ ⇑(ofIsClopen hU) ⁻¹' {1} = Uᶜ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_5
inst✝ : TopologicalSpace X
f g : LocallyConstant X (Fin 2)
h : ⇑f ⁻¹' {0} = ⇑g ⁻¹' {0}
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : PreconnectedSpace X
inst✝ : Nonempty Y
f : LocallyConstant X Y
⊢ ∃ y, f = const X y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ (fun x a ↦ (f a) x) ⁻¹' {g} = ⋂ a, ⇑(f a) ⁻¹' {g a}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹² : CommRing R
inst✝¹¹ : AddCommGroup M
inst✝¹⁰ : Module R M
S : Submonoid R
M' : Type u_1
inst✝⁹ : AddCommGroup M'
inst✝⁸ : Module R M'
f : M →ₗ[R] M'
inst✝⁷ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁶ : CommRing Rₛ
inst✝⁵ : Algebra R Rₛ
inst✝⁴ : Module Rₛ M'
inst✝³ : IsScalarTower R Rₛ M'
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
I : Type u_6
inst✝ : Finite I
b : Basis I Rₛ M'
⊢ ∃ r, ∃ (hr : r ∈ S), ∃ b', ∀ (i : I), (LocalizedModule.lift (Submonoid.powers r) f ⋯) (b' i) = b i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X✝ : Type u_1
Y : Type u_2
Z : Type u_3
α✝ : Type u_4
inst✝² : TopologicalSpace X✝
X : Type u_5
α : Type u_6
β : Type u_7
inst✝¹ : Finite α
inst✝ : TopologicalSpace X
f : α → LocallyConstant X β
g : α → β
⊢ IsOpen[inst✝] ((fun x a ↦ (f a) x) ⁻¹' {g})

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
y : Y
h : ∀ (x : X), f x = y
⊢ comap f = fun g ↦ const X (g y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
hfs : Function.Surjective f.toFun
⊢ Function.Injective (comap f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
R : Type u_5
inst✝ : One R
U : Set X
f : LocallyConstant X R
hU : IsClopen U
s : Set R
⊢ IsOpen[inst✝¹] (U.mulIndicator ⇑f ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
⊢ Function.LeftInverse (comap ↑e) (comap ↑e.symm)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
e : X ≃ₜ Y
⊢ Function.RightInverse (comap ↑e) (comap ↑e.symm)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
⊢ Function.LeftInverse (map ⇑e.symm) (map ⇑e)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝ : TopologicalSpace X
e : Y ≃ Z
⊢ Function.RightInverse (map ⇑e.symm) (map ⇑e)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : (s : Set X) → (x : X) → Decidable (x ∈ s)
x✝ : LocallyConstant X (Fin 2)
⊢ ⇑((fun s ↦ ofIsClopen ⋯) ((fun f ↦ { carrier := ⇑f ⁻¹' {0}, isClopen' := ⋯ }) x✝)) ⁻¹' {0} = ⇑x✝ ⁻¹' {0}

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.Localization.Free

Goal state before:
pp: R : Type u_4
M : Type u_5
inst✝¹³ : CommRing R
inst✝¹² : AddCommGroup M
inst✝¹¹ : Module R M
S : Submonoid R
M' : Type u_1
inst✝¹⁰ : AddCommGroup M'
inst✝⁹ : Module R M'
f : M →ₗ[R] M'
inst✝⁸ : IsLocalizedModule S f
Rₛ : Type u_3
inst✝⁷ : CommRing Rₛ
inst✝⁶ : Algebra R Rₛ
inst✝⁵ : Module Rₛ M'
inst✝⁴ : IsScalarTower R Rₛ M'
inst✝³ : Nontrivial Rₛ
inst✝² : IsLocalization S Rₛ
inst✝¹ : FinitePresentation R M
inst✝ : Free Rₛ M'
⊢ ∃ r ∈ S,
    Free (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) ∧
      finrank (Localization (Submonoid.powers r)) (LocalizedModule.Away r M) = finrank Rₛ M'

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : (s : Set X) → (x : X) → Decidable (x ∈ s)
x✝ : TopologicalSpace.Clopens X
⊢ (fun f ↦ { carrier := ⇑f ⁻¹' {0}, isClopen' := ⋯ }) ((fun s ↦ ofIsClopen ⋯) x✝) = x✝

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹⁴ : CommSemiring R
inst✝¹³ : CommSemiring S
inst✝¹² : Algebra R S
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝¹¹ : AddCommMonoid M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R M
inst✝⁸ : Module R N
inst✝⁷ : AddCommMonoid M'
inst✝⁶ : AddCommMonoid N'
inst✝⁵ : Module R M'
inst✝⁴ : Module R N'
inst✝³ : Module S M'
inst✝² : Module S N'
inst✝¹ : IsScalarTower R S M'
inst✝ : IsScalarTower R S N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
hf : IsBaseChange S f
hg : IsBaseChange S g
⊢ IsBaseChange S (f.prodMap g)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁹ : CommSemiring R
inst✝⁸ : CommSemiring S
inst✝⁷ : Algebra R S
ι : Type u_3
inst✝⁶ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → AddCommMonoid (M' i)
inst✝³ : (i : ι) → Module R (M i)
inst✝² : (i : ι) → Module R (M' i)
inst✝¹ : (i : ι) → Module S (M' i)
inst✝ : ∀ (i : ι), IsScalarTower R S (M' i)
f : (i : ι) → M i →ₗ[R] M' i
hf : ∀ (i : ι), IsBaseChange S (f i)
⊢ IsBaseChange S (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝¹² : CommSemiring R
inst✝¹¹ : CommSemiring S✝
inst✝¹⁰ : Algebra R S✝
S : Submonoid R
M : Type u_3
N : Type u_4
M' : Type u_5
N' : Type u_6
inst✝⁹ : AddCommMonoid M
inst✝⁸ : AddCommMonoid N
inst✝⁷ : Module R M
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid N'
inst✝³ : Module R M'
inst✝² : Module R N'
f : M →ₗ[R] M'
g : N →ₗ[R] N'
inst✝¹ : IsLocalizedModule S f
inst✝ : IsLocalizedModule S g
⊢ IsLocalizedModule S (f.prodMap g)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩

Tactic:
let dZ : TopologicalSpace Z := ⊥
    have : DiscreteTopology Z := discreteTopology_bot Z
    obtain ⟨f, hf⟩ := f
    obtain ⟨g, hg⟩ := g
    rw [IsLocallyConstant.iff_continuous] at hf hg ⊢
    dsimp only [coe_mk]
    rw [Set.union_eq_iUnion] at h
    refine (locallyFinite_of_finite _).continuous h (fun i ↦ ?_) (fun i ↦ ?_)
    · cases i <;> [exact h₂; exact h₁]
    · cases i <;> rw [continuousOn_iff_continuous_domRestrict]
      · convert! hg
        ext x
        simp only [cond_false, domRestrict_apply, Subtype.coe_eta, dite_eq_right_iff]
        exact fun hx ↦ hfg x ⟨hx, x.prop⟩
      · simp only [cond_true, domRestrict_dite, Subtype.coe_eta]
        exact hf

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
⊢ IsLocallyConstant fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S✝ : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S✝
inst✝⁶ : Algebra R S✝
S : Submonoid R
ι : Type u_3
inst✝⁵ : Finite ι
M : ι → Type u_4
M' : ι → Type u_5
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → AddCommMonoid (M' i)
inst✝² : (i : ι) → Module R (M i)
inst✝¹ : (i : ι) → Module R (M' i)
f : (i : ι) → M i →ₗ[R] M' i
inst✝ : ∀ (i : ι), IsLocalizedModule S (f i)
⊢ IsLocalizedModule S (LinearMap.pi fun i ↦ f i ∘ₗ LinearMap.proj i)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₁
⊢ (piecewise h₁ h₂ h f g hfg) x = f ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Z : Type u_3
inst✝¹ : TopologicalSpace X
C₁ C₂ : Set X
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
h : C₁ ∪ C₂ = univ
f : LocallyConstant (↑C₁) Z
g : LocallyConstant (↑C₂) Z
hfg : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f ⟨x, ⋯⟩ = g ⟨x, ⋯⟩
inst✝ : DecidablePred fun x ↦ x ∈ C₁
x : X
hx : x ∈ C₂
⊢ (piecewise h₁ h₂ h f g hfg) x = g ⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangePi

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Algebra R S
ι : Type u_3
N : ι → Type u_4
inst✝⁵ : (i : ι) → AddCommMonoid (N i)
inst✝⁴ : (i : ι) → Module R (N i)
P : ι → Type u_5
inst✝³ : (i : ι) → AddCommMonoid (P i)
inst✝² : (i : ι) → Module R (P i)
inst✝¹ : (i : ι) → Module S (P i)
inst✝ : ∀ (i : ι), IsScalarTower R S (P i)
ε : (i : ι) → N i →ₗ[R] P i
ibc : ∀ (i : ι), IsBaseChange S (ε i)
⊢ IsBaseChange S (lmap ε)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ Subtype.val ⁻¹' C₁ ∪ Subtype.val ⁻¹' C₂ = univ

Tactic:
by

Goal state after:
Module: Mathlib.Topology.LocallyConstant.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
Z : Type u_3
α : Type u_4
inst✝¹ : TopologicalSpace X
C₀ C₁ C₂ : Set X
h₀ : C₀ ⊆ C₁ ∪ C₂
h₁ : IsClosed[inst✝¹] C₁
h₂ : IsClosed[inst✝¹] C₂
f₁ : LocallyConstant (↑C₁) Z
f₂ : LocallyConstant (↑C₂) Z
inst✝ : DecidablePred fun x ↦ x ∈ C₁
hf : ∀ (x : X) (hx : x ∈ C₁ ∩ C₂), f₁ ⟨x, ⋯⟩ = f₂ ⟨x, ⋯⟩
this : (j : ↑C₀) → Decidable (j ∈ Subtype.val ⁻¹' C₁) := fun j ↦ decidable_of_iff (↑j ∈ C₁) ⋯
⊢ ∀ (x : ↑C₀) (hx : x ∈ Subtype.val ⁻¹' C₁ ∩ Subtype.val ⁻¹' C₂),
    (comap { toFun := C₁.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₁) ⟨x, ⋯⟩ =
      (comap { toFun := C₂.restrictPreimage Subtype.val, continuous_toFun := ⋯ } f₂) ⟨x, ⋯⟩

Tactic:
by

Goal state after: