harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/UnionInter.lean
@[simp] lemma union_zero : s ∪ 0 = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Multiset α
⊢ s ∪ 0 = s

Tactic:
simp [union_def]

Result:
no goals
-- Mathlib/Data/List/Indexes.lean
theorem mapIdx_eq_ofFn (l : List α) (f : ℕ → α → β) :
    l.mapIdx f = ofFn fun i : Fin l.length ↦ f (i : ℕ) (l.get i)

Proof state:
case cons
α : Type u
β : Type v
head✝ : α
tail✝ : List α
IH : ∀ (f : ℕ → α → β), mapIdx f tail✝ = ofFn fun i => f (↑i) (tail✝.get i)
f : ℕ → α → β
⊢ mapIdx f (head✝ :: tail✝) = ofFn fun i => f (↑i) ((head✝ :: tail✝).get i)

Tactic:
simp [IH]

Result:
no goals

Proof state:
case nil
α : Type u
β : Type v
f : ℕ → α → β
⊢ mapIdx f [] = ofFn fun i => f (↑i) ([].get i)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
f : ℕ → α → β
⊢ mapIdx f l = ofFn fun i => f (↑i) (l.get i)

Tactic:
induction l generalizing f with
| nil => simp
| cons _ _ IH => simp [IH]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma leftHomologyMap'_sub :
    leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ -
      leftHomologyMap' φ' h₁ h₂

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
φ φ' : S₁ ⟶ S₂
h₁ : S₁.LeftHomologyData
h₂ : S₂.LeftHomologyData
⊢ leftHomologyMap' (φ - φ') h₁ h₂ = leftHomologyMap' φ h₁ h₂ - leftHomologyMap' φ' h₁ h₂

Tactic:
simp only [sub_eq_add_neg, leftHomologyMap'_add, leftHomologyMap'_neg]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem LiftRel.symm (R : α → α → Prop) (H : Symmetric R) : Symmetric (LiftRel R) :=
  fun s1 s2 (h : Function.swap (LiftRel R) s2 s1) => by rwa [LiftRel.swap, H.swap_eq] at h

Proof state:
α : Type u
R : α → α → Prop
H : Symmetric R
s1 s2 : WSeq α
h : Function.swap (LiftRel R) s2 s1
⊢ LiftRel R s2 s1

Tactic:
rwa [LiftRel.swap, H.swap_eq] at h

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem sub_quot {R : Type uR} [Ring R] (r : R → R → Prop) {a b} :
    (⟨Quot.mk _ a⟩ - ⟨Quot.mk _ b⟩ : RingQuot r) = ⟨Quot.mk _ (a - b)⟩

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
⊢ { toQuot := Quot.mk (Rel r) a } - { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a - b) }

Tactic:
show sub r _ _ = _

Result:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
⊢ RingQuot.sub r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a - b) }

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
⊢ RingQuot.sub r { toQuot := Quot.mk (Rel r) a } { toQuot := Quot.mk (Rel r) b } = { toQuot := Quot.mk (Rel r) (a - b) }

Tactic:
rw [sub_def]

Result:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ Sub.sub ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a - b) }

Proof state:
R : Type uR
inst✝ : Ring R
r : R → R → Prop
a b : R
⊢ (match { toQuot := Quot.mk (Rel r) a }, { toQuot := Quot.mk (Rel r) b } with
    | { toQuot := a }, { toQuot := b } => { toQuot := Quot.map₂ Sub.sub ⋯ ⋯ a b }) =
    { toQuot := Quot.mk (Rel r) (a - b) }

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Removal.lean
lemma triangleRemovalBound_pos (hε : 0 < ε) (hε₁ : ε ≤ 1) : 0 < triangleRemovalBound ε

Proof state:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
this : 0 < 1 - ε / 4
⊢ 0 < triangleRemovalBound ε

Tactic:
unfold triangleRemovalBound

Result:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
this : 0 < 1 - ε / 4
⊢ 0 < (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ ⊓ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3

Proof state:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ 0 < 1 - ε / 4

Tactic:
linarith

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
this : 0 < 1 - ε / 4
⊢ 0 < (2 * ↑⌈4 / ε⌉₊ ^ 3)⁻¹ ⊓ (1 - ε / 4) * (ε / (16 * ↑(bound (ε / 8) ⌈4 / ε⌉₊))) ^ 3

Tactic:
positivity

Result:
no goals

Proof state:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
⊢ 0 < triangleRemovalBound ε

Tactic:
have : 0 < 1 - ε / 4 := by linarith

Result:
ε : ℝ
hε : 0 < ε
hε₁ : ε ≤ 1
this : 0 < 1 - ε / 4
⊢ 0 < triangleRemovalBound ε
-- Mathlib/LinearAlgebra/Dual.lean
theorem exists_dual_map_eq_bot_of_lt_top (hp : p < ⊤) (hp' : Free R (M ⧸ p)) :
    ∃ f : Dual R M, f ≠ 0 ∧ p.map f = ⊥

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Free R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
x✝ : M
⊢ x✝ ∈ p ↔ x✝ ∈ ⊤

Tactic:
simp [hp]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Free R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
⊢ p = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Free R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
x✝ : M
⊢ x✝ ∈ p ↔ x✝ ∈ ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p ≠ ⊤
hp' : Free R (M ⧸ p)
⊢ ∃ x, x ∉ p

Tactic:
contrapose! hp

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp' : Free R (M ⧸ p)
hp : ∀ (x : M), x ∈ p
⊢ p = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
⊢ ∃ x, x ∉ p

Tactic:
rw [lt_top_iff_ne_top] at hp

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p ≠ ⊤
hp' : Free R (M ⧸ p)
⊢ ∃ x, x ∉ p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
⊢ ∃ f, f ≠ 0 ∧ map f p = ⊥

Tactic:
obtain ⟨x, hx⟩ : ∃ x : M, x ∉ p := by rw [lt_top_iff_ne_top] at hp; contrapose! hp; ext; simp [hp]

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
x : M
hx : x ∉ p
⊢ ∃ f, f ≠ 0 ∧ map f p = ⊥

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
x : M
hx : x ∉ p
⊢ ∃ f, f ≠ 0 ∧ map f p = ⊥

Tactic:
obtain ⟨f, hf, hf'⟩ := p.exists_dual_map_eq_bot_of_nmem hx hp'

Result:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
x : M
hx : x ∉ p
f : Dual R M
hf : f x ≠ 0
hf' : map f p = ⊥
⊢ ∃ f, f ≠ 0 ∧ map f p = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
x : M
hx : x ∉ p
f : Dual R M
hf : f x ≠ 0
hf' : map f p = ⊥
⊢ f ≠ 0

Tactic:
aesop

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p : Submodule R M
hp : p < ⊤
hp' : Free R (M ⧸ p)
x : M
hx : x ∉ p
f : Dual R M
hf : f x ≠ 0
hf' : map f p = ⊥
⊢ ∃ f, f ≠ 0 ∧ map f p = ⊥

Tactic:
exact ⟨f, by aesop, hf'⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem attach_reverse (xs : Vector α n) :
    xs.reverse.attach = xs.attach.reverse.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse

Tactic:
rw [attach_congr (reverse_mk ..)]

Result:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (fun x => ⟨x.val, ⋯⟩) { toArray := toArray✝.reverse, size_toArray := ⋯ }.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse

Proof state:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ map (fun x => ⟨x.val, ⋯⟩) { toArray := toArray✝.reverse, size_toArray := ⋯ }.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse

Tactic:
simp [Array.map_attachWith]

Result:
no goals

Proof state:
α : Type ?u.59716
n : Nat
xs : Vector α n
x✝ : { x // x ∈ xs }
x : α
h : x ∈ xs
⊢ x ∈ xs.reverse

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
n : Nat
xs : Vector α n
⊢ xs.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      xs.attach.reverse

Tactic:
cases xs

Result:
case mk
α : Type u_1
n : Nat
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ }.reverse.attach =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      { toArray := toArray✝, size_toArray := size_toArray✝ }.attach.reverse
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_concat {a : α} : ∀ (l : List α), getLast (l ++ [a]) (by simp) = a
  | [] => rfl
  | a::t => by
    simp [getLast_cons _, getLast_concat t]

Proof state:
α : Type u_1
a✝ a : α
t : List α
⊢ (a :: t ++ [a✝]).getLast ⋯ = a✝

Tactic:
simp [getLast_cons _, getLast_concat t]

Result:
no goals

Proof state:
α : Type ?u.190172
a : α
l : List α
⊢ l ++ [a] ≠ []

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sum/Basic.lean
theorem isSome_getLeft?_iff_isLeft : x.getLeft?.isSome ↔ x.isLeft

Proof state:
α : Type u
β : Type v
x : α ⊕ β
⊢ x.getLeft?.isSome = true ↔ x.isLeft = true

Tactic:
rw [isLeft_iff, Option.isSome_iff_exists]

Result:
α : Type u
β : Type v
x : α ⊕ β
⊢ (∃ a, x.getLeft? = some a) ↔ ∃ y, x = inl y

Proof state:
α : Type u
β : Type v
x : α ⊕ β
⊢ (∃ a, x.getLeft? = some a) ↔ ∃ y, x = inl y

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_eq_zero_of_not_mem [DecidableEq M]
    (φ : MvPolynomial σ R) (i : M) (hi : i ∉ Finset.image (weight w) φ.support) :
    weightedHomogeneousComponent w i φ = 0

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w) x = i
⊢ ∀ d ∈ φ.support, (weight w) d ≠ i

Tactic:
exact fun m hm ↦ hi m (mem_support_iff.mp hm)

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w)) φ.support
⊢ ∀ d ∈ φ.support, (weight w) d ≠ i

Tactic:
simp only [Finset.mem_image, mem_support_iff, ne_eq, exists_prop, not_exists, not_and] at hi

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : ∀ (x : σ →₀ ℕ), ¬coeff x φ = 0 → ¬(weight w) x = i
⊢ ∀ d ∈ φ.support, (weight w) d ≠ i

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w)) φ.support
⊢ (weightedHomogeneousComponent w i) φ = 0

Tactic:
apply weightedHomogeneousComponent_eq_zero'

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
σ : Type u_3
w : σ → M
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq M
φ : MvPolynomial σ R
i : M
hi : i ∉ Finset.image (⇑(weight w)) φ.support
⊢ ∀ d ∈ φ.support, (weight w) d ≠ i
-- Mathlib/Topology/Order/ExtendFrom.lean
theorem continuousOn_Ioc_extendFrom_Ioo [TopologicalSpace α] [LinearOrder α] [DenselyOrdered α]
    [OrderTopology α] [TopologicalSpace β] [RegularSpace β] {f : α → β} {a b : α} {lb : β}
    (hab : a < b) (hf : ContinuousOn f (Ioo a b)) (hb : Tendsto f (𝓝[<] b) (𝓝 lb)) :
    ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[>] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
erw [dual_Ico, dual_Ioi, dual_Ioo] at this

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn f (⇑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto f (𝓝[⇑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) →
      ContinuousOn (extendFrom (⇑OrderDual.ofDual ⁻¹' Ioo a b) f) (⇑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
have := @continuousOn_Ico_extendFrom_Ioo αᵒᵈ _ _ _ _ _ _ _ f _ _ lb hab

Result:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this : ContinuousOn f (Ioo b a) → Tendsto f (𝓝[>] b) (𝓝 lb) → ContinuousOn (extendFrom (Ioo b a) f) (Ico b a)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Proof state:
α : Type u_1
β : Type u_2
inst✝⁵ : TopologicalSpace α
inst✝⁴ : LinearOrder α
inst✝³ : DenselyOrdered α
inst✝² : OrderTopology α
inst✝¹ : TopologicalSpace β
inst✝ : RegularSpace β
f : α → β
a b : α
lb : β
hab : a < b
hf : ContinuousOn f (Ioo a b)
hb : Tendsto f (𝓝[<] b) (𝓝 lb)
this :
  ContinuousOn f (⇑OrderDual.ofDual ⁻¹' Ioo a b) →
    Tendsto f (𝓝[⇑OrderDual.ofDual ⁻¹' Iio b] b) (𝓝 lb) →
      ContinuousOn (extendFrom (⇑OrderDual.ofDual ⁻¹' Ioo a b) f) (⇑OrderDual.ofDual ⁻¹' Ioc a b)
⊢ ContinuousOn (extendFrom (Ioo a b) f) (Ioc a b)

Tactic:
exact this hf hb

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_X_compare :
    (ratfuncAdicComplRingEquiv K) ((RatFunc.X : RatFunc K) : RatFuncAdicCompl K) =
      ((PowerSeries.X : K⟦X⟧) : K⸨X⸩)

Proof state:
K : Type u_2
inst✝ : Field K
⊢ (ratfuncAdicComplRingEquiv K) ↑RatFunc.X = (ofPowerSeries ℤ K) PowerSeries.X

Tactic:
rw [PowerSeries.coe_X, ← RatFunc.coe_X, ← LaurentSeries_coe, ← compare_coe]

Result:
K : Type u_2
inst✝ : Field K
⊢ (ratfuncAdicComplRingEquiv K) ↑RatFunc.X = AbstractCompletion.compare ?pkg (LaurentSeriesPkg K) (coe ?pkg RatFunc.X)

case pkg
K : Type u_2
inst✝ : Field K
⊢ AbstractCompletion (RatFunc K)

Proof state:
K : Type u_2
inst✝ : Field K
⊢ (ratfuncAdicComplRingEquiv K) ↑RatFunc.X = AbstractCompletion.compare ?pkg (LaurentSeriesPkg K) (coe ?pkg RatFunc.X)

case pkg
K : Type u_2
inst✝ : Field K
⊢ AbstractCompletion (RatFunc K)

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem ext_of_toZModPow {x y : ℤ_[p]} : (∀ n, toZModPow n x = toZModPow n y) ↔ x = y

Proof state:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) → x = y

Tactic:
intro h

Result:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ x = y

Proof state:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y

Tactic:
rintro rfl _

Result:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝) x = (toZModPow n✝) x

Proof state:
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) ↔ x = y

Tactic:
constructor

Result:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ (∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y) → x = y

case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
⊢ x = y → ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y

Proof state:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ x = y

Tactic:
rw [← lift_self x, ← lift_self y]

Result:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ (lift ⋯) x = (lift ⋯) y

Proof state:
case mp
p : ℕ
hp_prime : Fact (Nat.Prime p)
x y : ℤ_[p]
h : ∀ (n : ℕ), (toZModPow n) x = (toZModPow n) y
⊢ (lift ⋯) x = (lift ⋯) y

Tactic:
simp (config := { unfoldPartialApp := true }) [lift, limNthHom, nthHom, h]

Result:
no goals

Proof state:
case mpr
p : ℕ
hp_prime : Fact (Nat.Prime p)
x : ℤ_[p]
n✝ : ℕ
⊢ (toZModPow n✝) x = (toZModPow n✝) x

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem Δ_of_isShortNF_of_char_three : W.Δ = -W.a₄ ^ 3

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ W.Δ = -W.a₄ ^ 3

Tactic:
rw [Δ_of_isShortNF]

Result:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3

Proof state:
R : Type u_1
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsShortNF
inst✝ : CharP R 3
⊢ -16 * (4 * W.a₄ ^ 3 + 27 * W.a₆ ^ 2) = -W.a₄ ^ 3

Tactic:
linear_combination (-21 * W.a₄ ^ 3 - 144 * W.a₆ ^ 2) * CharP.cast_eq_zero R 3

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem realize_castLE_of_eq {m n : ℕ} (h : m = n) {h' : m ≤ n} {φ : L.BoundedFormula α m}
    {v : α → M} {xs : Fin n → M} : (φ.castLE h').Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)

Tactic:
simp only [castLE_rfl, cast_refl, OrderIso.coe_refl, Function.comp_id]

Result:
no goals

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m n : ℕ
h : m = n
h' : m ≤ n
φ : L.BoundedFormula α m
v : α → M
xs : Fin n → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast h)

Tactic:
subst h

Result:
L : Language
M : Type w
inst✝ : L.Structure M
α : Type u'
m : ℕ
φ : L.BoundedFormula α m
v : α → M
h' : m ≤ m
xs : Fin m → M
⊢ (castLE h' φ).Realize v xs ↔ φ.Realize v (xs ∘ Fin.cast ⋯)
-- Mathlib/Order/Defs/LinearOrder.lean
lemma min_le_left (a b : α) : min a b ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
⊢ min a b ≤ a

Tactic:
if h : a ≤ b
then simp [min_def, if_pos h, le_refl]
else simpa [min_def, if_neg h] using le_of_not_le h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ min a b ≤ a

Tactic:
simp [min_def, if_pos h, le_refl]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : ¬a ≤ b
⊢ min a b ≤ a

Tactic:
simpa [min_def, if_neg h] using le_of_not_le h

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_eq_mul_conj (n : ℤ√d) : (norm n : ℤ√d) = n * star n

Proof state:
d : ℤ
n : ℤ√d
⊢ ↑n.norm = n * star n

Tactic:
ext <;> simp [norm, star, mul_comm, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_inv : ∀ L : List G, L.prod⁻¹ = (L.map fun x => x⁻¹).prod
  | [] => by simp
  | x :: xs => by simp [mul_comm, prod_inv xs]

Proof state:
G : Type u_7
inst✝ : CommGroup G
x : G
xs : List G
⊢ (x :: xs).prod⁻¹ = (map (fun x => x⁻¹) (x :: xs)).prod

Tactic:
simp [mul_comm, prod_inv xs]

Result:
no goals

Proof state:
G : Type u_7
inst✝ : CommGroup G
⊢ [].prod⁻¹ = (map (fun x => x⁻¹) []).prod

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem contDiffOn_extend_coord_change [ChartedSpace H M] (hf : f ∈ maximalAtlas I n M)
    (hf' : f' ∈ maximalAtlas I n M) :
    ContDiffOn 𝕜 n (f.extend I ∘ (f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) ((f'.extend I).symm ≫ f.extend I).source

Tactic:
rw [extend_coord_change_source, I.image_eq]

Result:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (↑I.symm ⁻¹' (f'.symm ≫ₕ f).source ∩ range ↑I)

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : TopologicalSpace H
inst✝¹ : TopologicalSpace M
n : WithTop ℕ∞
f f' : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
inst✝ : ChartedSpace H M
hf : f ∈ maximalAtlas I n M
hf' : f' ∈ maximalAtlas I n M
⊢ ContDiffOn 𝕜 n (↑(f.extend I) ∘ ↑(f'.extend I).symm) (↑I.symm ⁻¹' (f'.symm ≫ₕ f).source ∩ range ↑I)

Tactic:
exact (StructureGroupoid.compatible_of_mem_maximalAtlas hf' hf).1

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem primeFactorsList_zero : primeFactorsList 0 = []

Proof state:
⊢ primeFactorsList 0 = []

Tactic:
rw [primeFactorsList]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem zipIdx_cons' (n : Nat) (x : α) (xs : List α) :
    zipIdx (x :: xs) n = (x, n) :: (zipIdx xs n).map (Prod.map id (· + 1))

Proof state:
α : Type u_1
n : Nat
x : α
xs : List α
⊢ (x :: xs).zipIdx n = (x, n) :: map (Prod.map id fun x => x + 1) (xs.zipIdx n)

Tactic:
rw [zipIdx_cons, Nat.add_comm, ← map_snd_add_zipIdx_eq_zipIdx]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Trim.lean
theorem measure_trim_toMeasurable_eq_zero {hm : m ≤ m0} (hs : μ.trim hm s = 0) :
    μ (@toMeasurable α m (μ.trim hm) s) = 0 :=
  measure_eq_zero_of_trim_eq_zero hm (by rwa [@measure_toMeasurable _ m])

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : (μ.trim hm) s = 0
⊢ (μ.trim hm) (toMeasurable (μ.trim hm) s) = 0

Tactic:
rwa [@measure_toMeasurable _ m]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma exists_norm_mul_eq_self (x : K) : ∃ c, ‖c‖ = 1 ∧ c * ‖x‖ = x

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0

case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Proof state:
K : Type u_1
inst✝ : RCLike K
⊢ ‖1‖ = 1 ∧ 1 * ↑‖0‖ = 0

Tactic:
simp

Result:
no goals

Proof state:
case inr
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖x‖ = x

Tactic:
exact ⟨x / ‖x‖, by simp [norm_ne_zero_iff.2, hx]⟩

Result:
no goals

Proof state:
case inl
K : Type u_1
inst✝ : RCLike K
⊢ ∃ c, ‖c‖ = 1 ∧ c * ↑‖0‖ = 0

Tactic:
exact ⟨1, by simp⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝ : RCLike K
x : K
hx : x ≠ 0
⊢ ‖x / ↑‖x‖‖ = 1 ∧ x / ↑‖x‖ * ↑‖x‖ = x

Tactic:
simp [norm_ne_zero_iff.2, hx]

Result:
no goals