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

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ Completion.extension ⇑f ↑(a + b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b

Tactic:
extension_coe hf

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = Completion.extension ⇑f ↑a + Completion.extension ⇑f ↑b

Tactic:
extension_coe hf

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = f a + Completion.extension ⇑f ↑b
Module: Mathlib.Topology.Algebra.GroupCompletion

Goal state before:
pp: M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = f a + Completion.extension ⇑f ↑b

Tactic:
extension_coe hf

Goal state after:
M : Type u_1
R : Type u_2
α : Type u_3
β : Type u_4
inst✝⁷ : UniformSpace α
inst✝⁶ : AddGroup α
inst✝⁵ : IsUniformAddGroup α
inst✝⁴ : UniformSpace β
inst✝³ : AddGroup β
inst✝² : IsUniformAddGroup β
inst✝¹ : CompleteSpace β
inst✝ : T0Space β
f : α →+ β
hf✝ : Continuous ⇑f
hf : UniformContinuous ⇑f
a✝ b✝ : Completion α
a b : α
⊢ f (a + b) = f a + f b
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ -(u ^ 3 * P y) * (v ^ 2 * Q x) ^ 3 * (u * P z) ^ 3 + 2 * (u ^ 3 * P y) * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 3 -
                                        3 * (u ^ 2 * P x) ^ 2 * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 2 *
                                          (v * Q z) +
                                      3 * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 2 * Q x) ^ 2 * (u * P z) *
                                        (v * Q z) ^ 2 +
                                    (u ^ 2 * P x) ^ 3 * (v ^ 3 * Q y) * (v * Q z) ^ 3 -
                                  2 * (u ^ 3 * P y) ^ 2 * (v ^ 3 * Q y) * (v * Q z) ^ 3 +
                                W'.a₁ * (u ^ 2 * P x) * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 4 +
                              W'.a₁ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 3 * (v * Q z) -
                            W'.a₁ * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 3 * Q y) * (u * P z) * (v * Q z) ^ 3 -
                          W'.a₁ * (u ^ 3 * P y) ^ 2 * (v ^ 2 * Q x) * (v * Q z) ^ 4 -
                        2 * W'.a₂ * (u ^ 2 * P x) * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) +
                      2 * W'.a₂ * (u ^ 2 * P x) * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) * (v * Q z) ^ 4 +
                    W'.a₃ * (v ^ 3 * Q y) ^ 2 * (u * P z) ^ 6 -
                  W'.a₃ * (u ^ 3 * P y) ^ 2 * (v * Q z) ^ 6 -
                W'.a₄ * (v ^ 2 * Q x) * (v ^ 3 * Q y) * (u * P z) ^ 6 * (v * Q z) -
              W'.a₄ * (u ^ 2 * P x) * (v ^ 3 * Q y) * (u * P z) ^ 4 * (v * Q z) ^ 3 +
            W'.a₄ * (u ^ 3 * P y) * (v ^ 2 * Q x) * (u * P z) ^ 3 * (v * Q z) ^ 4 +
          W'.a₄ * (u ^ 2 * P x) * (u ^ 3 * P y) * (u * P z) * (v * Q z) ^ 6 -
        2 * W'.a₆ * (v ^ 3 * Q y) * (u * P z) ^ 6 * (v * Q z) ^ 3 +
      2 * W'.a₆ * (u ^ 3 * P y) * (u * P z) ^ 3 * (v * Q z) ^ 6 =
    ((u * v) ^ 2) ^ 3 *
      (-P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * Q z +
                                        3 * P x * P y * Q x ^ 2 * P z * Q z ^ 2 +
                                      P x ^ 3 * Q y * Q z ^ 3 -
                                    2 * P y ^ 2 * Q y * Q z ^ 3 +
                                  W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                W'.a₁ * P y * Q x * Q y * P z ^ 3 * Q z -
                              W'.a₁ * P x * P y * Q y * P z * Q z ^ 3 -
                            W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                          2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * Q z +
                        2 * W'.a₂ * P x * P y * Q x * P z * Q z ^ 4 +
                      W'.a₃ * Q y ^ 2 * P z ^ 6 -
                    W'.a₃ * P y ^ 2 * Q z ^ 6 -
                  W'.a₄ * Q x * Q y * P z ^ 6 * Q z -
                W'.a₄ * P x * Q y * P z ^ 4 * Q z ^ 3 +
              W'.a₄ * P y * Q x * P z ^ 3 * Q z ^ 4 +
            W'.a₄ * P x * P y * P z * Q z ^ 6 -
          2 * W'.a₆ * Q y * P z ^ 6 * Q z ^ 3 +
        2 * W'.a₆ * P y * P z ^ 3 * Q z ^ 6)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
⊢ -P y * P x ^ 3 * P z ^ 3 + 2 * P y * P y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * P x * P y * P z ^ 2 * P z +
                                      3 * P x * P y * P x ^ 2 * P z * P z ^ 2 +
                                    P x ^ 3 * P y * P z ^ 3 -
                                  2 * P y ^ 2 * P y * P z ^ 3 +
                                W'.a₁ * P x * P y ^ 2 * P z ^ 4 +
                              W'.a₁ * P y * P x * P y * P z ^ 3 * P z -
                            W'.a₁ * P x * P y * P y * P z * P z ^ 3 -
                          W'.a₁ * P y ^ 2 * P x * P z ^ 4 -
                        2 * W'.a₂ * P x * P x * P y * P z ^ 4 * P z +
                      2 * W'.a₂ * P x * P y * P x * P z * P z ^ 4 +
                    W'.a₃ * P y ^ 2 * P z ^ 6 -
                  W'.a₃ * P y ^ 2 * P z ^ 6 -
                W'.a₄ * P x * P y * P z ^ 6 * P z -
              W'.a₄ * P x * P y * P z ^ 4 * P z ^ 3 +
            W'.a₄ * P y * P x * P z ^ 3 * P z ^ 4 +
          W'.a₄ * P x * P y * P z * P z ^ 6 -
        2 * W'.a₆ * P y * P z ^ 6 * P z ^ 3 +
      2 * W'.a₆ * P y * P z ^ 3 * P z ^ 6 =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -P y * Q x ^ 3 * 0 ^ 3 + 2 * P y * Q y ^ 2 * 0 ^ 3 - 3 * P x ^ 2 * Q x * Q y * 0 ^ 2 * Q z +
                                          3 * P x * P y * Q x ^ 2 * 0 * Q z ^ 2 +
                                        P x ^ 3 * Q y * Q z ^ 3 -
                                      2 * P y ^ 2 * Q y * Q z ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * 0 ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * 0 ^ 3 * Q z -
                                W'.a₁ * P x * P y * Q y * 0 * Q z ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * Q z ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * 0 ^ 4 * Q z +
                          2 * W'.a₂ * P x * P y * Q x * 0 * Q z ^ 4 +
                        W'.a₃ * Q y ^ 2 * 0 ^ 6 -
                      W'.a₃ * P y ^ 2 * Q z ^ 6 -
                    W'.a₄ * Q x * Q y * 0 ^ 6 * Q z -
                  W'.a₄ * P x * Q y * 0 ^ 4 * Q z ^ 3 +
                W'.a₄ * P y * Q x * 0 ^ 3 * Q z ^ 4 +
              W'.a₄ * P x * P y * 0 * Q z ^ 6 -
            2 * W'.a₆ * Q y * 0 ^ 6 * Q z ^ 3 +
          2 * W'.a₆ * P y * 0 ^ 3 * Q z ^ 6 +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P x ^ 3 -
      ((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3) +
        (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3 - Q y) * Q z ^ 3 * P y ^ 2) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -P y * Q x ^ 3 * P z ^ 3 + 2 * P y * Q y ^ 2 * P z ^ 3 - 3 * P x ^ 2 * Q x * Q y * P z ^ 2 * 0 +
                                          3 * P x * P y * Q x ^ 2 * P z * 0 ^ 2 +
                                        P x ^ 3 * Q y * 0 ^ 3 -
                                      2 * P y ^ 2 * Q y * 0 ^ 3 +
                                    W'.a₁ * P x * Q y ^ 2 * P z ^ 4 +
                                  W'.a₁ * P y * Q x * Q y * P z ^ 3 * 0 -
                                W'.a₁ * P x * P y * Q y * P z * 0 ^ 3 -
                              W'.a₁ * P y ^ 2 * Q x * 0 ^ 4 -
                            2 * W'.a₂ * P x * Q x * Q y * P z ^ 4 * 0 +
                          2 * W'.a₂ * P x * P y * Q x * P z * 0 ^ 4 +
                        W'.a₃ * Q y ^ 2 * P z ^ 6 -
                      W'.a₃ * P y ^ 2 * 0 ^ 6 -
                    W'.a₄ * Q x * Q y * P z ^ 6 * 0 -
                  W'.a₄ * P x * Q y * P z ^ 4 * 0 ^ 3 +
                W'.a₄ * P y * Q x * P z ^ 3 * 0 ^ 4 +
              W'.a₄ * P x * P y * P z * 0 ^ 6 -
            2 * W'.a₆ * Q y * P z ^ 6 * 0 ^ 3 +
          2 * W'.a₆ * P y * P z ^ 3 * 0 ^ 6 +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q x ^ 3 -
      ((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3) +
        (P y - (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) * P z ^ 3 * Q y ^ 2) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.RingTheory.PrincipalIdealDomainOfPrime

Goal state before:
pp: case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ span {x} * span {y} ≤ I

Tactic:
← hx,

Goal state after:
case refine_2
R : Type u_1
inst✝ : CommSemiring R
I : Ideal R
a x : R
hx : I ⊔ span {a} = span {x}
y : R
hy : Submodule.colon I ↑(span {a}) = span {y}
⊢ (I ⊔ span {a}) * span {y} ≤ I
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (P y * Q z ^ 3 - Q y * P z ^ 3) *
        ((P y * Q z ^ 3 - Q y * P z ^ 3) ^ 2 + W'.a₁ * (P y * Q z ^ 3 - Q y * P z ^ 3) * P z * Q z * 0 -
                W'.a₂ * P z ^ 2 * Q z ^ 2 * 0 ^ 2 -
              P x * Q z ^ 2 * 0 ^ 2 -
            Q x * P z ^ 2 * 0 ^ 2 -
          P x * Q z ^ 2 * 0 ^ 2) +
      P y * Q z ^ 3 * 0 ^ 3 =
    (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ W.toAffine.negAddY (P x / P z ^ 2) (Q x / Q z ^ 2) (P y / P z ^ 3) (n / (P z * Q z * d)) =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3

Tactic:
Affine.negAddY,

Goal state after:
F : Type u
inst✝ : Field F
W : Jacobian F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
n d : F
hd : d ≠ 0
⊢ n / (P z * Q z * d) * (W.toAffine.addX (P x / P z ^ 2) (Q x / Q z ^ 2) (n / (P z * Q z * d)) - P x / P z ^ 2) +
      P y / P z ^ 3 =
    (n *
            (n ^ 2 + W.a₁ * n * P z * Q z * d - W.a₂ * P z ^ 2 * Q z ^ 2 * d ^ 2 - P x * Q z ^ 2 * d ^ 2 -
                Q x * P z ^ 2 * d ^ 2 -
              P x * Q z ^ 2 * d ^ 2) +
          P y * Q z ^ 3 * d ^ 3) /
        (P z * Q z) ^ 3 /
      d ^ 3
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ -(((u * v) ^ 2) ^ 3 * W'.negAddY P Q) - W'.a₁ * (((u * v) ^ 2) ^ 2 * W'.addX P Q) * ((u * v) ^ 2 * addZ P Q) -
      W'.a₃ * ((u * v) ^ 2 * addZ P Q) ^ 3 =
    ((u * v) ^ 2) ^ 3 * (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * addZ P Q - W'.a₃ * addZ P Q ^ 3)

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
hP : W'.Equation P
⊢ -0 - W'.a₁ * 0 * 0 - W'.a₃ * 0 ^ 3 = 0

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hPz : P z = 0
⊢ -((P x * Q z) ^ 3 * (-Q y - W'.a₁ * Q x * Q z - W'.a₃ * Q z ^ 3)) -
        W'.a₁ * ((P x * Q z) ^ 2 * Q x) * (P x * Q z * Q z) -
      W'.a₃ * (P x * Q z * Q z) ^ 3 =
    (P x * Q z) ^ 3 * Q y

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hQ : W'.Equation Q
hQz : Q z = 0
⊢ -((-(Q x * P z)) ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)) -
        W'.a₁ * ((-(Q x * P z)) ^ 2 * P x) * (-(Q x * P z) * P z) -
      W'.a₃ * (-(Q x * P z) * P z) ^ 3 =
    (-(Q x * P z)) ^ 3 * P y

Tactic:
ring1

Goal state after:
Module: Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula

Goal state before:
pp: case a
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hx : P x * Q z ^ 2 = Q x * P z ^ 2
⊢ (-W'.negAddY P Q - W'.a₁ * W'.addX P Q * 0 - W'.a₃ * 0 ^ 3) * (P z * Q z) ^ 3 + W'.negAddY P Q * (P z * Q z) ^ 3 -
      ((-(P y * Q z ^ 3 - Q y * P z ^ 3)) ^ 3 + (P y * Q z ^ 3 - Q y * P z ^ 3) ^ 3) =
    0

Tactic:
ring1

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case inr
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
hsurj : Function.Surjective ⇑v
x : K
h : x ≠ 0
⊢ ContinuousAt (⇑v) x

Tactic:
· have h0 : hv.v x ≠ 0 := (Valuation.ne_zero_iff _).mpr h
    rw [ContinuousAt, WithZeroTopology.tendsto_of_ne_zero h0]
    exact Valued.locally_const (by simpa using h0)

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case mpr
G : Type u_1
inst✝² : CommGroup G
inst✝¹ : LinearOrder G
inst✝ : IsOrderedMonoid G
a b : G
ha : a ≠ 1
⊢ (∃! k, a ^ k = b) → ∃ n, a ^ n = b

Tactic:
· exact fun h ↦ h.exists

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: e : ℤ ≃+ ℤ
⊢ e = AddEquiv.refl ℤ ∨ e = AddEquiv.neg ℤ

Tactic:
suffices e 1 = 1 ∨ -e 1 = 1 by simpa [AddEquiv.ext_int_iff, neg_eq_iff_eq_neg]
  have he : ¬IsOfFinAddOrder (e 1) :=
    not_isOfFinAddOrder_of_isAddTorsionFree ((AddEquiv.map_ne_zero_iff e).mpr Int.one_ne_zero)
  rw [← AddSubgroup.zmultiples_eq_zmultiples_iff he]
  simpa [e.surjective, eq_comm] using (e : ℤ →+ ℤ).map_zmultiples 1

Goal state after:
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.LeftInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

Tactic:
intro ⟨a, ha⟩

Goal state after:
case refine_1
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ (fun x_1 ↦ ⟨1, ⋯⟩) ((fun x_1 ↦ ⟨1, ⋯⟩) ⟨a, ha⟩) = ⟨a, ha⟩
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ Function.RightInverse (fun x_1 ↦ ⟨1, ⋯⟩) fun x_1 ↦ ⟨1, ⋯⟩

Tactic:
intro ⟨a, ha⟩

Goal state after:
case refine_2
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G'
ha : a ∈ closure {y}
⊢ (fun x_1 ↦ ⟨1, ⋯⟩) ((fun x_1 ↦ ⟨1, ⋯⟩) ⟨a, ha⟩) = ⟨a, ha⟩
Module: Mathlib.GroupTheory.ArchimedeanDensely

Goal state before:
pp: case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
⊢ ∀ {a b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun a ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
          b ↔
      a ≤ b

Tactic:
intro ⟨a, ha⟩

Goal state after:
case refine_4
G : Type u_1
G' : Type u_2
inst✝⁵ : CommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedMonoid G
inst✝² : CommGroup G'
inst✝¹ : LinearOrder G'
inst✝ : IsOrderedMonoid G'
x : G
y : G'
hxy : x = 1 ↔ y = 1
hx : x = 1
a : G
ha : a ∈ closure {x}
⊢ ∀ {b : ↥(closure {x})},
    { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
          ⟨a, ha⟩ ≤
        { toFun := fun x_1 ↦ ⟨1, ⋯⟩, invFun := fun x_1 ↦ ⟨1, ⋯⟩, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }.toFun
          b ↔
      ⟨a, ha⟩ ≤ b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case e'_2
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : v s / v r ≠ 0
⊢ {x | v x * v r < v s} = {x | v x < ↑(Units.mk0 (v s / v r) hrs)}

pp: case e'_3
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
r s : K
hr : r ≠ 0
hs : s ≠ 0
hrs : v s / v r ≠ 0
x✝ : hat K
⊢ extensionValuation x✝ * v r < v s ↔ extensionValuation x✝ < ↑(Units.mk0 (v s / v r) hrs)

Tactic:
all_goals simp [← lt_div_iff₀, zero_lt_iff, hr]

Goal state after:
Module: Mathlib.Order.Northcott

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
h : α → β
h' : β → γ
inst✝² : LE γ
inst✝¹ : Northcott h'
inst✝ : Filter.TendstoCofinite h
c : γ
⊢ {a | (h' ∘ h) a ≤ c}.Finite

Tactic:
by
    refine Set.Finite.of_finite_fibers h ?_ fun x _ ↦
      (Filter.TendstoCofinite.finite_preimage_singleton h x).inter_of_right _
    exact (finite_le (h := h') c).subset <| by grind

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

Goal state before:
pp: case pos.inl
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : s = t ∧ 1 = 1
⊢ s = t

pp: case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t

Tactic:
· exact H.1

Goal state after:
case pos.inr
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : Nontrivial R
s t : σ
h : 1 = 1
H : 1 = 0 ∧ 1 = 0
⊢ s = t
Module: Mathlib.RingTheory.PowerSeries.Basic

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∑ l ∈ Finset.map (Finsupp.mapRange.addEquiv (Finsupp.uniqueAddEquiv ()).symm).toEmbedding (s.finsuppAntidiag d),
      ∏ i ∈ s, (MvPowerSeries.coeff (l i)) (f i) =
    ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff (single () (l i))) (f i)

Tactic:
sum_map

Goal state after:
R : Type u_2
inst✝¹ : CommSemiring R
ι : Type u_3
inst✝ : DecidableEq ι
f : ι → R⟦X⟧
d : ℕ
s : Finset ι
⊢ ∑ x ∈ s.finsuppAntidiag d,
      ∏ i ∈ s,
        (MvPowerSeries.coeff (((Finsupp.mapRange.addEquiv (Finsupp.uniqueAddEquiv ()).symm).toEmbedding x) i)) (f i) =
    ∑ l ∈ s.finsuppAntidiag d, ∏ i ∈ s, (MvPowerSeries.coeff (single () (l i))) (f i)
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : v x = v y
⊢ embedding a = embedding b

Tactic:
← hx,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
a b : (ofClass v).ValueGroup₀
hab : extensionValuation.restrict ↑⋯.choose = extensionValuation.restrict ↑⋯.choose
x : K := ⋯.choose
hx_def : x = ⋯.choose
y : K := ⋯.choose
hy_def : y = ⋯.choose
hx : v x = embedding a
hy : v y = embedding b
ha0 : embedding a ≠ embedding 0
h0 : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h0' : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : v x = v y
⊢ v x = embedding b
Module: Mathlib.Topology.Algebra.Valued.ValuedField

Goal state before:
pp: case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ ¬(ofClass extensionValuation) ↑y = 0

Tactic:
simp only [coe_ofClass, extensionValuation_apply_coe, map_eq_zero, ← ne_eq]

Goal state after:
case neg.hnc
K : Type u_1
inst✝¹ : Field K
Γ₀ : Type u_2
inst✝ : LinearOrderedCommGroupWithZero Γ₀
hv : Valued K Γ₀
s : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
this : (𝓝 0).HasBasis (fun x ↦ True) fun γ ↦ {x | extensionValuation x < ↑((Units.map ↑embedding) γ)}
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
γ : (ofClass v).ValueGroup₀ˣ
hx0 : ¬x = 0
y : K := ⋯.choose
hy_def : y = ⋯.choose
hy : v y = embedding ↑γ
⊢ y ≠ 0
Module: Mathlib.RingTheory.MvPowerSeries.Trunc

Goal state before:
pp: σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
i j : σ →₀ ℕ
hij : (i, j) ∈ antidiagonal x
⊢ MvPolynomial.coeff (i, j).1 ((truncFinset R s) f) * MvPolynomial.coeff (i, j).2 ((truncFinset R t) g) =
    (coeff (i, j).1) f * (coeff (i, j).2) g

Tactic:
simp only [mem_antidiagonal] at hij

Goal state after:
σ : Type u_1
R : Type u_2
inst✝ : CommSemiring R
s t : Finset (σ →₀ ℕ)
hs : IsLowerSet ↑s
ht : IsLowerSet ↑t
x : σ →₀ ℕ
f g : MvPowerSeries σ R
hxs : x ∈ s
hxt : x ∈ t
i j : σ →₀ ℕ
hij : i + j = x
⊢ MvPolynomial.coeff (i, j).1 ((truncFinset R s) f) * MvPolynomial.coeff (i, j).2 ((truncFinset R t) g) =
    (coeff (i, j).1) f * (coeff (i, j).2) g