mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case hg
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Surjective ⇑((↑f).submoduleMap M)

pp: case hg'
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Surjective ⇑((↑f).submoduleMap N)

Tactic:
<;>

Goal state after:
case hg
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Surjective ⇑((↑f).submoduleMap M)

case hg'
R : Type u
S : Type v
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
M N : Submodule R S
H : Function.Injective ⇑(M.mulMap N)
T : Type w
inst✝¹ : Semiring T
inst✝ : Algebra R T
f : S →ₐ[R] T
hf : Function.Injective ⇑f
this :
  Function.Injective
    (⇑((Submodule.map (↑f) M).mulMap (Submodule.map (↑f) N)) ∘
      ⇑(TensorProduct.map ((↑f).submoduleMap M) ((↑f).submoduleMap N)))
⊢ Function.Surjective ⇑((↑f).submoduleMap N)
Module: Mathlib.LinearAlgebra.TensorPower.Basic

Goal state before:
pp: case e_6.left
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin na), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.castAdd nb i)) = Fin.addCases a b (Fin.castAdd nb i)

pp: case e_6.right
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin nb), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.natAdd na i)) = Fin.addCases a b (Fin.natAdd na i)

Tactic:
<;>

Goal state after:
case e_6.left
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin na), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.castAdd nb i)) = Fin.addCases a b (Fin.castAdd nb i)

case e_6.right
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
na nb : ℕ
a : Fin na → M
b : Fin nb → M
⊢ ∀ (i : Fin nb), Sum.elim a b (Fin.addCases Sum.inl Sum.inr (Fin.natAdd na i)) = Fin.addCases a b (Fin.natAdd na i)
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: ι : Type u_1
R : Type u_4
inst✝⁵ : CommSemiring R
s : ι → Type u_7
inst✝⁴ : (i : ι) → AddCommMonoid (s i)
inst✝³ : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝² : (i : ι) → AddCommMonoid (t i)
inst✝¹ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
inst✝ : DecidableEq ι
i : ι
x : (i : ι) → s i
u : s i →ₗ[R] t i
⊢ (fun j ↦ (update f i u j) (x j)) = update (fun j ↦ (f j) (x j)) i (u (x i))

Tactic:
by
  ext j
  exact apply_update (fun i F => F (x i)) f i u j

Goal state after:
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = j

pp: case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = j

Tactic:
<;>

Goal state after:
case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨0, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨0, ⋯⟩ = j

case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
j : Fin (Nat.succ 0).succ
hij : ![a, b] ((fun i ↦ i) ⟨1, ⋯⟩) = ![a, b] j
⊢ (fun i ↦ i) ⟨1, ⋯⟩ = j
Module: Mathlib.LinearAlgebra.LinearDisjoint

Goal state before:
pp: case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨0, ⋯⟩))

pp: case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
<;>

Goal state after:
case «0»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨0, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨0, ⋯⟩))

case «1»
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
inst✝ : Algebra R S
M N : Submodule R S
H : M.LinearDisjoint N
hf : Flat R ↥M ∨ Flat R ↥N
hc : ∀ (m n : ↥(M ⊓ N)), Commute ↑m ↑n
a✝ : Nontrivial R
s : Finset ↥(M ⊓ N)
h : LinearIndependent R fun i ↦ ↑i
hs : Nontrivial ↥s
a b : ↥s
hab : a ≠ b
this : LinearIndependent R ((fun i ↦ ↑i) ∘ ![a, b])
⊢ ↑(![↑a, ↑b] ((fun i ↦ i) ⟨1, ⋯⟩)) = ↑(((fun i ↦ ↑i) ∘ ![a, b]) ((fun i ↦ i) ⟨1, ⋯⟩))
Module: Mathlib.LinearAlgebra.PiTensorProduct.Basic

Goal state before:
pp: case e_6.inl
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
x✝ : (i : ι ⊕ ι₂) → N i
val✝ : ι
⊢ Sum.rec (fun i₁ ↦ x✝ (Sum.inl i₁)) (fun i₂ ↦ x✝ (Sum.inr i₂)) (Sum.inl val✝) = x✝ (Sum.inl val✝)

pp: case e_6.inr
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
x✝ : (i : ι ⊕ ι₂) → N i
val✝ : ι₂
⊢ Sum.rec (fun i₁ ↦ x✝ (Sum.inl i₁)) (fun i₂ ↦ x✝ (Sum.inr i₂)) (Sum.inr val✝) = x✝ (Sum.inr val✝)

Tactic:
<;>

Goal state after:
case e_6.inl
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
x✝ : (i : ι ⊕ ι₂) → N i
val✝ : ι
⊢ Sum.rec (fun i₁ ↦ x✝ (Sum.inl i₁)) (fun i₂ ↦ x✝ (Sum.inr i₂)) (Sum.inl val✝) = x✝ (Sum.inl val✝)

case e_6.inr
ι : Type u_1
ι₂ : Type u_2
ι₃ : Type u_3
R : Type u_4
inst✝¹¹ : CommSemiring R
R₁ : Type u_5
R₂ : Type u_6
s : ι → Type u_7
inst✝¹⁰ : (i : ι) → AddCommMonoid (s i)
inst✝⁹ : (i : ι) → Module R (s i)
M : Type u_8
inst✝⁸ : AddCommMonoid M
inst✝⁷ : Module R M
E : Type u_9
inst✝⁶ : AddCommMonoid E
inst✝⁵ : Module R E
F : Type u_10
inst✝⁴ : AddCommMonoid F
t : ι → Type u_11
inst✝³ : (i : ι) → AddCommMonoid (t i)
inst✝² : (i : ι) → Module R (t i)
N : ι ⊕ ι₂ → Type u_12
inst✝¹ : (i : ι ⊕ ι₂) → AddCommMonoid (N i)
inst✝ : (i : ι ⊕ ι₂) → Module R (N i)
x✝ : (i : ι ⊕ ι₂) → N i
val✝ : ι₂
⊢ Sum.rec (fun i₁ ↦ x✝ (Sum.inl i₁)) (fun i₂ ↦ x✝ (Sum.inr i₂)) (Sum.inr val✝) = x✝ (Sum.inr val✝)
Module: Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ x ∣ normalize b * g

Tactic:
← (Finset.gcd_mul_left' ..).dvd_iff_dvd_right,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsGCDMonoid R
J : Ideal R
this : NormalizedGCDMonoid R := Classical.arbitrary (NormalizedGCDMonoid R)
K : Ideal R
hJK0 : J * K ≠ 0
hK : Submodule.IsPrincipal (J * K)
x : R
hJK : J * K = R ∙ x
hxmemJK : x ∈ J * K
T : Finset R
hTK : ↑T ⊆ ↑K
K' : Ideal R := span ↑T
hxT : x ∈ J * K'
g : R := T.gcd id
hK' : K' ≤ span {g}
hxJg : x ∈ J * span {g}
hx0 : x ≠ 0
b : R
hb : b ∈ J
z : R
hz : g * z ∈ span {g}
⊢ x ∣ T.gcd fun x ↦ normalize b * id x
Module: Mathlib.RingTheory.ClassGroup.Basic

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

pp: case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) → ∃ x, spanSingleton R⁰ ↑x = ↑I

Tactic:
<;>

Goal state after:
case mp
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ ↑x = ↑I) → ∃ x, spanSingleton R⁰ x = ↑I

case mpr
R : Type u_1
K : Type u_2
inst✝³ : CommRing R
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : (FractionalIdeal R⁰ K)ˣ
⊢ (∃ x, spanSingleton R⁰ x = ↑I) → ∃ x, spanSingleton R⁰ ↑x = ↑I
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
⊢ Subgroup.map (Units.mapEquiv (canonicalEquiv R⁰ (FractionRing R) K).toMulEquiv).toMonoidHom
      (toPrincipalIdeal R (FractionRing R)).range =
    (toPrincipalIdeal R K).range

Tactic:
ext I
    simp only [Subgroup.mem_map, mem_principal_ideals_iff]
    constructor
    · rintro ⟨I, ⟨x, hx⟩, rfl⟩
      refine ⟨FractionRing.algEquiv R K x, ?_⟩
      simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv, ← hx,
        RingEquiv.coe_toMulEquiv, canonicalEquiv_spanSingleton]
      rfl
    · rintro ⟨x, hx⟩
      refine ⟨Units.mapEquiv (canonicalEquiv R⁰ K (FractionRing R)).toMulEquiv I,
        ⟨(FractionRing.algEquiv R K).symm x, ?_⟩, Units.ext ?_⟩
      · simp only [RingEquiv.toMulEquiv_eq_coe, coe_mapEquiv, ← hx, RingEquiv.coe_toMulEquiv,
          canonicalEquiv_spanSingleton]
        rfl
      · simp only [RingEquiv.toMulEquiv_eq_coe, MulEquiv.coe_toMonoidHom, coe_mapEquiv,
          RingEquiv.coe_toMulEquiv, canonicalEquiv_canonicalEquiv, canonicalEquiv_self,
          RingEquiv.refl_apply]

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_cases hI0 : I = 0

Goal state after:
case pos
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)
hI0 : I = 0
⊢ Submodule.IsPrincipal I

case neg
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)
hI0 : ¬I = 0
⊢ Submodule.IsPrincipal I
Module: Mathlib.Topology.LocallyConstant.Basic

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

Tactic:
exact ⟨f x, f.eq_const x⟩

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

Goal state before:
pp: case refine_2.false
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
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif false then C₁ else C₂)

pp: case refine_2.true
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
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif true then C₁ else C₂)

Tactic:
<;>

Goal state after:
case refine_2.false
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
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif false then C₁ else C₂)

case refine_2.true
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
h : (⋃ b, bif b then C₁ else C₂) = univ
inst✝ : DecidablePred fun x ↦ x ∈ C₁
dZ : TopologicalSpace Z := ⊥
this : DiscreteTopology Z
f : ↑C₁ → Z
hf✝ : IsLocallyConstant f
hf : Continuous[instTopologicalSpaceSubtype, dZ] f
g : ↑C₂ → Z
hg✝ : IsLocallyConstant g
hg : Continuous[instTopologicalSpaceSubtype, dZ] g
hfg :
  ∀ (x : X) (hx : x ∈ C₁ ∩ C₂),
    { toFun := f, isLocallyConstant := hf✝ } ⟨x, ⋯⟩ = { toFun := g, isLocallyConstant := hg✝ } ⟨x, ⋯⟩
⊢ ContinuousOn (fun i ↦ if hi : i ∈ C₁ then f ⟨i, hi⟩ else g ⟨i, ⋯⟩) (bif true then C₁ else C₂)
Module: Mathlib.GroupTheory.Solvable

Goal state before:
pp: case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

pp: case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥

Tactic:
<;>

Goal state after:
case zero.refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ a * b ∈ ⊥

case zero.refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : IsSimpleGroup G
x✝ : Group.IsSolvable G
hn : derivedSeries G 0 = ⊥
a b : G
⊢ b * a ∈ ⊥
Module: Mathlib.FieldTheory.Normal.Closure

Goal state before:
pp: case refine_1
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
x✝ : IsNormalClosure F K L
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
⊢ normalClosure F K L = ⊤

pp: case refine_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
x✝ : (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ normalClosure F K L = ⊤
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : normalClosure F K L = ⊤
⊢ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤

Tactic:
<;>

Goal state after:
case refine_1
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
x✝ : IsNormalClosure F K L
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
⊢ normalClosure F K L = ⊤

case refine_2
F : Type u_1
K : Type u_2
L : Type u_3
inst✝⁵ : Field F
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra F K
inst✝¹ : Algebra F L
inst✝ : Algebra.IsAlgebraic F K
x✝ : (∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits) ∧ normalClosure F K L = ⊤
splits : ∀ (x : K), (Polynomial.map (algebraMap F L) (minpoly F x)).Splits
h : normalClosure F K L = ⊤
⊢ ⨆ x, IntermediateField.adjoin F ((minpoly F x).rootSet L) = ⊤
Module: Mathlib.FieldTheory.PrimitiveElement

Goal state before:
pp: case h.a.inl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hβ : IsIntegral F β
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
x : E
hα : IsIntegral F x
f : F[X] := minpoly F x
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' x) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := x + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : x ∈ F⟮γ⟯
⊢ x ∈ ↑F⟮γ⟯

pp: case h.a.inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
f : F[X] := minpoly F α
ιFE : F →+* E := algebraMap F E
c : F
x : E
hβ : IsIntegral F x
g : F[X] := minpoly F x
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' x) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • x
β_in_Fγ : x ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
⊢ x ∈ ↑F⟮γ⟯

Tactic:
<;>

Goal state after:
case h.a.inl
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
β : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hβ : IsIntegral F β
g : F[X] := minpoly F β
ιFE : F →+* E := algebraMap F E
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
c : F
x : E
hα : IsIntegral F x
f : F[X] := minpoly F x
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' x) / (β' - ιEE' β) ≠ (ιEE'.comp ιFE) c
γ : E := x + c • β
β_in_Fγ : β ∈ F⟮γ⟯
α_in_Fγ : x ∈ F⟮γ⟯
⊢ x ∈ ↑F⟮γ⟯

case h.a.inr
F : Type u_1
inst✝⁴ : Field F
inst✝³ : Infinite F
E : Type u_2
inst✝² : Field E
α : E
inst✝¹ : Algebra F E
inst✝ : Algebra.IsSeparable F E
hα : IsIntegral F α
f : F[X] := minpoly F α
ιFE : F →+* E := algebraMap F E
c : F
x : E
hβ : IsIntegral F x
g : F[X] := minpoly F x
ιEE' : E →+* (Polynomial.map ιFE g).SplittingField := algebraMap E (Polynomial.map ιFE g).SplittingField
hc :
  ∀ α' ∈ (Polynomial.map (ιEE'.comp ιFE) f).roots,
    ∀ β' ∈ (Polynomial.map (ιEE'.comp ιFE) g).roots, -(α' - ιEE' α) / (β' - ιEE' x) ≠ (ιEE'.comp ιFE) c
γ : E := α + c • x
β_in_Fγ : x ∈ F⟮γ⟯
α_in_Fγ : α ∈ F⟮γ⟯
⊢ x ∈ ↑F⟮γ⟯