harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[to_additive]
lemma norm_div_eq_norm_right {x : E} (y : E) (h : ‖x‖ = 0) : ‖x / y‖ = ‖y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x / y‖ = ‖y‖

Tactic:
apply le_antisymm ?_ ?_

Result:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x / y‖ ≤ ‖y‖

E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x / y‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖x / y‖ ≤ ‖y‖

Tactic:
simpa [h] using norm_div_le x y

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
x y : E
h : ‖x‖ = 0
⊢ ‖y‖ ≤ ‖x / y‖

Tactic:
simpa [h, norm_div_rev x y] using norm_sub_norm_le' y x

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Topology.IsInducing.isLindelof_iff {f : X → Y} (hf : IsInducing f) :
    IsLindelof s ↔ IsLindelof (f '' s)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
⊢ IsLindelof s ↔ IsLindelof (f '' s)

Tactic:
refine ⟨fun hs => hs.image hf.continuous, fun hs F F_ne_bot _ F_le => ?_⟩

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F

Proof state:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
exact ⟨x, x_in, hf.mapClusterPt_iff.1 hx⟩

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
⊢ ∃ x ∈ s, ClusterPt x F

Tactic:
obtain ⟨_, ⟨x, x_in : x ∈ s, rfl⟩, hx : ClusterPt (f x) (map f F)⟩ :=
  hs ((map_mono F_le).trans_eq map_principal)

Result:
case intro.intro.intro.intro
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : IsInducing f
hs : IsLindelof (f '' s)
F : Filter X
F_ne_bot : F.NeBot
x✝ : CountableInterFilter F
F_le : F ≤ 𝓟 s
x : X
x_in : x ∈ s
hx : ClusterPt (f x) (map f F)
⊢ ∃ x ∈ s, ClusterPt x F
-- Mathlib/Geometry/Manifold/IsManifold/InteriorBoundary.lean
lemma isInteriorPoint_disjointUnion_right {p : M ⊕ M'} (hp : I.IsInteriorPoint p)
    (hright : Sum.isRight p) : I.IsInteriorPoint (Sum.getRight p hright)

Proof state:
case right
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hright : p.isRight = true
x : M' := p.getRight hright
h : ¬I.IsInteriorPoint x
⊢ I.IsBoundaryPoint (Sum.inr (p.getRight hright))

Tactic:
have := isInteriorPoint_or_isBoundaryPoint (I := I) x

Result:
case right
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hright : p.isRight = true
x : M' := p.getRight hright
h : ¬I.IsInteriorPoint x
this : I.IsInteriorPoint x ∨ I.IsBoundaryPoint x
⊢ I.IsBoundaryPoint (Sum.inr (p.getRight hright))

Proof state:
case left
𝕜 : Type u_1
inst✝⁷ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁴ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
M' : Type u_5
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H M'
p : M ⊕ M'
hp : I.IsInteriorPoint p
hright : p.isRight = true
x : M' := p.getRight hright
h : ¬I.IsInteriorPoint x
⊢ I.IsInteriorPoint p

Tactic:
exact hp

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive (attr := simp)] lemma zpow_eq_empty : s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Proof state:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ s ^ 0 ≠ ∅

Tactic:
rw [← nonempty_iff_ne_empty]

Result:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Proof state:
case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ (s ^ 0).Nonempty

Tactic:
simp

Result:
no goals

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

Tactic:
contrapose!

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ≠ ∅ ∨ n = 0 → s ^ n ≠ ∅

Proof state:
case mp.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
hs : s ≠ ∅
⊢ s ^ n ≠ ∅

Tactic:
exact nonempty_iff_ne_empty.1 (nonempty_iff_ne_empty.2 hs).zpow

Result:
no goals

Proof state:
case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Tactic:
rintro ⟨rfl, hn⟩

Result:
case mpr.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Proof state:
case mpr.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
n : ℤ
hn : n ≠ 0
⊢ ∅ ^ n = ∅

Tactic:
exact empty_zpow hn

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ ↔ s = ∅ ∧ n ≠ 0

Tactic:
constructor

Result:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ^ n = ∅ → s = ∅ ∧ n ≠ 0

case mpr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s = ∅ ∧ n ≠ 0 → s ^ n = ∅

Proof state:
case mp
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
⊢ s ≠ ∅ ∨ n = 0 → s ^ n ≠ ∅

Tactic:
rintro (hs | rfl)

Result:
case mp.inl
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
n : ℤ
hs : s ≠ ∅
⊢ s ^ n ≠ ∅

case mp.inr
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : DivisionMonoid α
s : Finset α
⊢ s ^ 0 ≠ ∅
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma top_supp_eq_univ (c : ConnectedComponent (⊤ : SimpleGraph V)) :
    c.supp = (Set.univ : Set V)

Proof state:
case h.a
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ ⊤.Reachable v w

Tactic:
exact (@SimpleGraph.top_connected V (Nonempty.intro v)).preconnected v w

Result:
no goals

Proof state:
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
⊢ c.supp = Set.univ

Tactic:
ext v

Result:
case h
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ v ∈ c.supp ↔ v ∈ Set.univ

Proof state:
case h
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ v ∈ c.supp ↔ v ∈ Set.univ

Tactic:
simp only [Set.mem_univ, iff_true, mem_supp_iff, ← hw]

Result:
case h
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ ⊤.connectedComponentMk v = Quot.mk ⊤.Reachable w

Proof state:
V : Type u
c : ⊤.ConnectedComponent
⊢ c.supp = Set.univ

Tactic:
have ⟨w, hw⟩ := c.exists_rep

Result:
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
⊢ c.supp = Set.univ

Proof state:
case h
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ ⊤.connectedComponentMk v = Quot.mk ⊤.Reachable w

Tactic:
apply SimpleGraph.ConnectedComponent.sound

Result:
case h.a
V : Type u
c : ⊤.ConnectedComponent
w : V
hw : Quot.mk ⊤.Reachable w = c
v : V
⊢ ⊤.Reachable v w
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma twoTorsionPolynomial_disc : W.twoTorsionPolynomial.disc = 16 * W.Δ

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ W.twoTorsionPolynomial.disc = 16 * W.Δ

Tactic:
simp only [b₂, b₄, b₆, b₈, Δ, twoTorsionPolynomial, Cubic.disc]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 2 - 4 * 4 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
          4 * (W.a₁ ^ 2 + 4 * W.a₂) ^ 3 * (W.a₃ ^ 2 + 4 * W.a₆) -
        27 * 4 ^ 2 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
      18 * 4 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * (W.a₃ ^ 2 + 4 * W.a₆) =
    16 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
⊢ (W.a₁ ^ 2 + 4 * W.a₂) ^ 2 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 2 - 4 * 4 * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) ^ 3 -
          4 * (W.a₁ ^ 2 + 4 * W.a₂) ^ 3 * (W.a₃ ^ 2 + 4 * W.a₆) -
        27 * 4 ^ 2 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
      18 * 4 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * (2 * W.a₄ + W.a₁ * W.a₃)) * (W.a₃ ^ 2 + 4 * W.a₆) =
    16 *
      (-(W.a₁ ^ 2 + 4 * W.a₂) ^ 2 *
              (W.a₁ ^ 2 * W.a₆ + 4 * W.a₂ * W.a₆ - W.a₁ * W.a₃ * W.a₄ + W.a₂ * W.a₃ ^ 2 - W.a₄ ^ 2) -
            8 * (2 * W.a₄ + W.a₁ * W.a₃) ^ 3 -
          27 * (W.a₃ ^ 2 + 4 * W.a₆) ^ 2 +
        9 * (W.a₁ ^ 2 + 4 * W.a₂) * (2 * W.a₄ + W.a₁ * W.a₃) * (W.a₃ ^ 2 + 4 * W.a₆))

Tactic:
ring1

Result:
no goals
-- Mathlib/FieldTheory/KummerExtension.lean
lemma X_pow_sub_C_eq_prod {R : Type*} [CommRing R] [IsDomain R]
    {n : ℕ} {ζ : R} (hζ : IsPrimitiveRoot ζ n) {α a : R} (hn : 0 < n) (e : α ^ n = a) :
    (X ^ n - C a) = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
let K := FractionRing R

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
apply_fun Polynomial.map i using map_injective i h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ Polynomial.map i (X ^ n - C a) = Polynomial.map i (∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
let i := algebraMap R K

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Tactic:
have h := FaithfulSMul.algebraMap_injective R K

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ X ^ n - C a = ∏ i ∈ Finset.range n, (X - C (ζ ^ i * α))

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
n : ℕ
ζ : R
hζ : IsPrimitiveRoot ζ n
α a : R
hn : 0 < n
e : α ^ n = a
K : Type u_1 := FractionRing R
i : R →+* K := algebraMap R K
h : Function.Injective ⇑(algebraMap R K)
⊢ Polynomial.map i (X ^ n - C a) = Polynomial.map i (∏ i ∈ Finset.range n, (X - C (ζ ^ i * α)))

Tactic:
simpa only [Polynomial.map_sub, Polynomial.map_pow, map_X, map_C, map_mul, map_pow,
  Polynomial.map_prod, Polynomial.map_mul]
  using X_pow_sub_C_eq_prod' (hζ.map_of_injective h) hn <| map_pow i α n ▸ congrArg i e

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem neg_add_le_of_le_add {a b c : Int} (h : a ≤ b + c) : -b + a ≤ c

Proof state:
a b c : Int
h✝ : a ≤ b + c
h : -b + a ≤ -b + (b + c)
⊢ -b + a ≤ c

Tactic:
rwa [Int.neg_add_cancel_left] at h

Result:
no goals

Proof state:
a b c : Int
h : a ≤ b + c
⊢ -b + a ≤ c

Tactic:
have h := Int.add_le_add_left h (-b)

Result:
a b c : Int
h✝ : a ≤ b + c
h : -b + a ≤ -b + (b + c)
⊢ -b + a ≤ c
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_onTerm [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (t : L.Term α)
    (v : α → M) : (φ.onTerm t).realize v = t.realize v

Proof state:
case var
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
a✝ : α
⊢ Term.realize v (φ.onTerm (var a✝)) = Term.realize v (var a✝)

Tactic:
rfl

Result:
no goals

Proof state:
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
t : L.Term α
v : α → M
⊢ Term.realize v (φ.onTerm t) = Term.realize v t

Tactic:
induction' t with _ n f ts ih

Result:
case var
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
a✝ : α
⊢ Term.realize v (φ.onTerm (var a✝)) = Term.realize v (var a✝)

case func
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)

Proof state:
case func
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
α : Type u'
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
v : α → M
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih : ∀ (a : Fin n), Term.realize v (φ.onTerm (ts a)) = Term.realize v (ts a)
⊢ Term.realize v (φ.onTerm (func f ts)) = Term.realize v (func f ts)

Tactic:
simp only [Term.realize, LHom.onTerm, LHom.map_onFunction, ih]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem SameCycle.exists_pow_eq'' [Finite α] (h : SameCycle f x y) :
    ∃ i : ℕ, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

Proof state:
case intro.succ.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ ∃ i_1, 0 < i_1 ∧ i_1 ≤ orderOf f ∧ (f ^ i_1) x = (f ^ (i + 1)) x

Tactic:
exact ⟨i.succ, i.zero_lt_succ, hi.le, by rfl⟩

Result:
no goals

Proof state:
case intro.zero.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = (f ^ 0) x

Tactic:
refine ⟨orderOf f, orderOf_pos f, le_rfl, ?_⟩

Result:
case intro.zero.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ (f ^ orderOf f) x = (f ^ 0) x

Proof state:
α : Type u_2
f : Perm α
x y : α
inst✝ : Finite α
h : f.SameCycle x y
⊢ ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = y

Tactic:
obtain ⟨_ | i, hi, rfl⟩ := h.exists_pow_eq'

Result:
case intro.zero.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ ∃ i, 0 < i ∧ i ≤ orderOf f ∧ (f ^ i) x = (f ^ 0) x

case intro.succ.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ ∃ i_1, 0 < i_1 ∧ i_1 ≤ orderOf f ∧ (f ^ i_1) x = (f ^ (i + 1)) x

Proof state:
case intro.zero.intro
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
hi : 0 < orderOf f
h : f.SameCycle x ((f ^ 0) x)
⊢ (f ^ orderOf f) x = (f ^ 0) x

Tactic:
rw [pow_orderOf_eq_one, pow_zero]

Result:
no goals

Proof state:
α : Type u_2
f : Perm α
x : α
inst✝ : Finite α
i : ℕ
hi : i + 1 < orderOf f
h : f.SameCycle x ((f ^ (i + 1)) x)
⊢ (f ^ i.succ) x = (f ^ (i + 1)) x

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_neg_right (x y : V) : angle x (-y) = π - angle x y

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner x (-y) / (‖x‖ * ‖-y‖)) = π - arccos (inner x y / (‖x‖ * ‖y‖))

Tactic:
rw [← Real.arccos_neg, norm_neg, inner_neg_right, neg_div]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x (-y) = π - angle x y

Tactic:
unfold angle

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ arccos (inner x (-y) / (‖x‖ * ‖-y‖)) = π - arccos (inner x y / (‖x‖ * ‖y‖))
-- Mathlib/Analysis/Normed/Group/Completeness.lean
lemma Metric.exists_subseq_summable_dist_of_cauchySeq (u : ℕ → α) (hu : CauchySeq u) :
    ∃ f : ℕ → ℕ, StrictMono f ∧ Summable fun i => dist (u (f (i+1))) (u (f i))

Proof state:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b

Tactic:
exact fun n => le_of_lt <| hf₂ n (f (n+1)) <| hf₁.monotone (Nat.le_add_right n 1)

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ Summable fun i => dist (u (f (i + 1))) (u (f i))

Tactic:
refine Summable.of_nonneg_of_le (fun n => by positivity) ?_ summable_geometric_two

Result:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∀ (b : ℕ), dist (u (f (b + 1))) (u (f b)) ≤ (1 / 2) ^ b

Proof state:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))

Tactic:
refine ⟨f, hf₁, ?_⟩

Result:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ Summable fun i => dist (u (f (i + 1))) (u (f i))

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
⊢ ∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))

Tactic:
obtain ⟨f, hf₁, hf₂⟩ := Metric.exists_subseq_bounded_of_cauchySeq u hu
  (fun n => (1 / (2 : ℝ))^n) (fun n => by positivity)

Result:
case intro.intro
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
⊢ ∃ f, StrictMono f ∧ Summable fun i => dist (u (f (i + 1))) (u (f i))

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
n : ℕ
⊢ 0 < (fun n => (1 / 2) ^ n) n

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
u : ℕ → α
hu : CauchySeq u
f : ℕ → ℕ
hf₁ : StrictMono f
hf₂ : ∀ (n m : ℕ), m ≥ f n → dist (u m) (u (f n)) < (1 / 2) ^ n
n : ℕ
⊢ 0 ≤ dist (u (f (n + 1))) (u (f n))

Tactic:
positivity

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma AnalyticWithinAt.pi (hf : ∀ i, AnalyticWithinAt 𝕜 (f i) s e) :
    AnalyticWithinAt 𝕜 (fun x ↦ (f · x)) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
hf : ∀ (i : ι), AnalyticWithinAt 𝕜 (f i) s e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e

Tactic:
choose p hp using hf

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hp : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
s : Set E
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
hp : ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) s e
⊢ AnalyticWithinAt 𝕜 (fun x x_1 => f x_1 x) s e

Tactic:
exact ⟨FormalMultilinearSeries.pi p, HasFPowerSeriesWithinAt.pi hp⟩

Result:
no goals