mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

pp: case refine_2.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ⊤
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
·

Goal state after:
case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|

pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' : Ideal.span {↑I.den} * I₀ = Ideal.span {↑a} * I.num
⊢ ↑(Ideal.absNorm I.num) * ↑|(Algebra.norm ℤ) ↑a| = ↑(Ideal.absNorm I₀) * ↑|(Algebra.norm ℤ) ↑I.den|
Module: Mathlib.RingTheory.FractionalIdeal.Norm

Goal state before:
pp: R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥

Tactic:
·

Goal state after:
R : Type u_1
inst✝⁶ : CommRing R
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Free ℤ R
inst✝³ : Module.Finite ℤ R
K : Type u_2
inst✝² : CommRing K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
a : ↥R⁰
I₀ : Ideal R
h : a • I.den • ↑I = I.den • Submodule.map (Algebra.linearMap R K) I₀
h' :
  Submodule.map (Algebra.linearMap R K) (Ideal.span {↑I.den} • I₀) =
    Submodule.map (Algebra.linearMap R K) (Ideal.span {↑a} • I.num)
⊢ (Algebra.linearMap R K).ker = ⊥
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
⊢ (↑↑ψ).toFun x = K.subtype x

pp: K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ := ⋯
this : IsTopologicalRing ↥K.topologicalClosure := ⋯
ι : ↥K → ↥K.topologicalClosure := ⋯
ui : IsUniformInducing ι
di : IsDenseInducing ι := ⋯
extψ : ↥K.topologicalClosure →+* ℂ := ⋯
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := ⋯
ψ₁ : ℝ →+* ℂ := ⋯
hψ₁ : Continuous ⇑ψ₁
x : ↥K
⊢ ∃ r, ofRealHom.rangeRestrictField r = j (ι x)

Tactic:
·

Goal state after:
case refine_2.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
⊢ (↑↑ψ).toFun x = K.subtype x
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < (m ^ 2 + n ^ 2) / 2

Tactic:
·

Goal state after:
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hyo : y % 2 = 1
hzpos : 0 < z
h0 : ¬x = 0
v : ℚ := ⋯
w : ℚ := ⋯
hq : v ^ 2 + w ^ 2 = 1
hvz : v ≠ 0
hw1 : w ≠ -1
hQ : ∀ (x : ℚ), 1 + x ^ 2 ≠ 0
hp : (v, w) ∈ {p | p.1 ^ 2 + p.2 ^ 2 = 1 ∧ p.2 ≠ -1}
q : ℚ := ⋯
ht4 : v = 2 * q / (1 + q ^ 2) ∧ w = (1 - q ^ 2) / (1 + q ^ 2)
m : ℤ := ⋯
n : ℤ := ⋯
hm0 : m ≠ 0
hq2 : q = ↑n / ↑m
hm2n2 : 0 < m ^ 2 + n ^ 2
hm2n20 : ↑m ^ 2 + ↑n ^ 2 ≠ 0
hw2 : w = (↑m ^ 2 - ↑n ^ 2) / (↑m ^ 2 + ↑n ^ 2)
hv2 : v = 2 * ↑m * ↑n / (↑m ^ 2 + ↑n ^ 2)
hnmcp : n.gcd m = 1
hmncp : m.gcd n = 1
hm2 : m % 2 = 1
hn2 : n % 2 = 1
h1 :
  2 ∣ m ^ 2 + n ^ 2 ∧
    2 ∣ m ^ 2 - n ^ 2 ∧ (m ^ 2 - n ^ 2) / 2 % 2 = 0 ∧ ((m ^ 2 - n ^ 2) / 2).gcd ((m ^ 2 + n ^ 2) / 2) = 1
⊢ 0 < (m ^ 2 + n ^ 2) / 2
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case e'_3
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝¹ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this✝ : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
this : extψ (↑j.symm (j (ι x))) = ofRealHom r
⊢ K.subtype x = ofRealHom r

Tactic:
·

Goal state after:
case e'_3
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝¹ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this✝ : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ofRealHom.fieldRange
j : ↥K.topologicalClosure ≃+* ↥ofRealHom.fieldRange := RingEquiv.subfieldCongr h
ψ₁ : ℝ →+* ℂ := extψ.comp (j.symm.toRingHom.comp ofRealHom.rangeRestrictField)
hψ₁ : Continuous ⇑ψ₁
x : ↥K
r : ℝ
hr : ofRealHom.rangeRestrictField r = j (ι x)
this : extψ (↑j.symm (j (ι x))) = ofRealHom r
⊢ K.subtype x = ofRealHom r
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified

pp: case inr
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h2 : x % 2 = 1 ∧ y % 2 = 0
⊢ h.IsPrimitiveClassified

Tactic:
·

Goal state after:
case inl
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hzpos : 0 < z
h1 : x % 2 = 0 ∧ y % 2 = 1
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified

pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : z ≤ 0
⊢ h.IsPrimitiveClassified

Tactic:
·

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
hc : x.gcd y = 1
hz : 0 < z
⊢ h.IsPrimitiveClassified
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified

pp: case neg
x y z : ℤ
h : PythagoreanTriple x y z
h0 : ¬x.gcd y = 0
⊢ h.IsClassified

Tactic:
·

Goal state after:
case pos
x y z : ℤ
h : PythagoreanTriple x y z
h0 : x.gcd y = 0
⊢ h.IsClassified
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ⊤
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
·

Goal state after:
case refine_2.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h : K.topologicalClosure = ⊤
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case mp
x y z : ℤ
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 →
    ∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

pp: case mpr
x y z : ℤ
⊢ (∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)) →
    PythagoreanTriple x y z ∧ x.gcd y = 1

Tactic:
·

Goal state after:
case mp
x y z : ℤ
⊢ PythagoreanTriple x y z ∧ x.gcd y = 1 →
    ∃ m n,
      (x = m ^ 2 - n ^ 2 ∧ y = 2 * m * n ∨ x = 2 * m * n ∧ y = m ^ 2 - n ^ 2) ∧
        (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

pp: case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
·

Goal state after:
case refine_2.inr.inl
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = RingHom.id ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inl
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2 ∧ 2 * m * n = 2 * m * n ∨ m ^ 2 - n ^ 2 = 2 * m * n ∧ 2 * m * n = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

pp: case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n = m ^ 2 - n ^ 2 ∧ m ^ 2 - n ^ 2 = 2 * m * n ∨ 2 * m * n = 2 * m * n ∧ m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
·

Goal state after:
case h.inl
z m n : ℤ
h : PythagoreanTriple (m ^ 2 - n ^ 2) (2 * m * n) z ∧ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2 ∧ 2 * m * n = 2 * m * n ∨ m ^ 2 - n ^ 2 = 2 * m * n ∧ 2 * m * n = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)
Module: Mathlib.NumberTheory.FLT.Polynomial

Goal state before:
pp: case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
dr0 : derivative (C u * a ^ p) = 0 ∧ derivative (C v * b ^ q) = 0 ∧ derivative (C w * c ^ r) = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0

Tactic:
·

Goal state after:
case inr
k : Type u_1
inst✝ : Field k
p q r : ℕ
hp : p ≠ 0
hq : q ≠ 0
hr : r ≠ 0
hineq : q * r + r * p + p * q ≤ p * q * r
chp : ↑p ≠ 0
chq : ↑q ≠ 0
chr : ↑r ≠ 0
a b c : k[X]
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
hab : IsCoprime a b
u v w : k
hu : u ≠ 0
hv : v ≠ 0
hw : w ≠ 0
heq : C u * a ^ p + C v * b ^ q + C w * c ^ r = 0
hbc : IsCoprime b c
hca : IsCoprime c a
hCu : C u ≠ 0
hCv : C v ≠ 0
hCw : C w ≠ 0
hap : a ^ p ≠ 0
hbq : b ^ q ≠ 0
hcr : c ^ r ≠ 0
habp : IsCoprime (C u * a ^ p) (C v * b ^ q)
hbcp : IsCoprime (C v * b ^ q) (C w * c ^ r)
hcap : IsCoprime (C w * c ^ r) (C u * a ^ p)
habcp : IsCoprime (C u * a ^ p * (C v * b ^ q)) (C w * c ^ r)
dr0 : derivative (C u * a ^ p) = 0 ∧ derivative (C v * b ^ q) = 0 ∧ derivative (C w * c ^ r) = 0
⊢ derivative a = 0 ∧ derivative b = 0 ∧ derivative c = 0
Module: Mathlib.Topology.Instances.Complex

Goal state before:
pp: case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype

Tactic:
·

Goal state after:
case refine_2.inr.inr
K : Subfield ℂ
ψ : ↥K →+* ℂ
hc : UniformContinuous ⇑ψ
this✝ : IsTopologicalDivisionRing ℂ :=
  { toIsTopologicalRing := NormedDivisionRing.to_isTopologicalDivisionRing.toIsTopologicalRing,
    toContinuousInv₀ := NormedDivisionRing.to_isTopologicalDivisionRing.toContinuousInv₀ }
this : IsTopologicalRing ↥K.topologicalClosure := Subring.instIsTopologicalRing K.topologicalClosure.toSubring
ι : ↥K → ↥K.topologicalClosure := ⇑(Subfield.inclusion ⋯)
ui : IsUniformInducing ι
di : IsDenseInducing ι := IsUniformInducing.isDenseInducing ui ?refine_1
extψ : ↥K.topologicalClosure →+* ℂ := IsDenseInducing.extendRingHom ui ⋯ hc
hψ : Continuous (⋯.extend ⇑ψ)
h✝ : K.topologicalClosure = ⊤
ψ₁ : ℂ →+* ℂ := extψ.comp ((RingEquiv.subfieldCongr h✝).symm.toRingHom.comp Subfield.topEquiv.symm.toRingHom)
hψ₁ : Continuous ⇑ψ₁
h : ψ₁ = starRingEnd ℂ
⊢ (↑↑ψ).toFun = ⇑K.subtype ∨ (↑↑ψ).toFun = ⇑(starRingEnd ℂ) ∘ ⇑K.subtype
Module: Mathlib.NumberTheory.PythagoreanTriples

Goal state before:
pp: case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n = m ^ 2 - n ^ 2 ∧ m ^ 2 - n ^ 2 = 2 * m * n ∨ 2 * m * n = 2 * m * n ∧ m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)

Tactic:
·

Goal state after:
case h.inr
z m n : ℤ
h : PythagoreanTriple (2 * m * n) (m ^ 2 - n ^ 2) z ∧ (2 * m * n).gcd (m ^ 2 - n ^ 2) = 1
co : m.gcd n = 1
pp : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (2 * m * n = m ^ 2 - n ^ 2 ∧ m ^ 2 - n ^ 2 = 2 * m * n ∨ 2 * m * n = 2 * m * n ∧ m ^ 2 - n ^ 2 = m ^ 2 - n ^ 2) ∧
    (z = m ^ 2 + n ^ 2 ∨ z = -(m ^ 2 + n ^ 2)) ∧ m.gcd n = 1 ∧ (m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0)