harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem orderTopology_of_nhds_abs {α : Type*} [TopologicalSpace α] [LinearOrderedAddCommGroup α]
    (h_nhds : ∀ a : α, 𝓝 a = ⨅ r > 0, 𝓟 { b | |a - b| < r }) : OrderTopology α

Proof state:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a

Tactic:
letI := Preorder.topology α

Result:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a

Proof state:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := { topology_eq_generate_intervals := rfl }
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a

Tactic:
exact (nhds_eq_iInf_abs_sub a).symm

Result:
no goals

Proof state:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
⊢ OrderTopology α

Tactic:
refine ⟨TopologicalSpace.ext_nhds fun a => ?_⟩

Result:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
⊢ 𝓝 a = 𝓝 a

Proof state:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
this : TopologicalSpace α := Preorder.topology α
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a

Tactic:
letI : OrderTopology α := ⟨rfl⟩

Result:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
this✝ : TopologicalSpace α := Preorder.topology α
this : OrderTopology α := { topology_eq_generate_intervals := rfl }
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a

Proof state:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
⊢ 𝓝 a = 𝓝 a

Tactic:
rw [h_nhds]

Result:
α : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : LinearOrderedAddCommGroup α
h_nhds : ∀ (a : α), 𝓝 a = ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r}
a : α
⊢ ⨅ r, ⨅ (_ : r > 0), 𝓟 {b | |a - b| < r} = 𝓝 a
-- Mathlib/RingTheory/Nilpotent/Defs.lean
theorem IsNilpotent.of_pow [MonoidWithZero R] {x : R} {m : ℕ}
    (h : IsNilpotent (x ^ m)) : IsNilpotent x

Proof state:
case intro
R : Type u_1
inst✝ : MonoidWithZero R
x : R
m n : ℕ
h : (x ^ m) ^ n = 0
⊢ IsNilpotent x

Tactic:
use m * n

Result:
case h
R : Type u_1
inst✝ : MonoidWithZero R
x : R
m n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
x : R
m : ℕ
h : IsNilpotent (x ^ m)
⊢ IsNilpotent x

Tactic:
obtain ⟨n, h⟩ := h

Result:
case intro
R : Type u_1
inst✝ : MonoidWithZero R
x : R
m n : ℕ
h : (x ^ m) ^ n = 0
⊢ IsNilpotent x

Proof state:
case h
R : Type u_1
inst✝ : MonoidWithZero R
x : R
m n : ℕ
h : (x ^ m) ^ n = 0
⊢ x ^ (m * n) = 0

Tactic:
rw [← h, pow_mul x m n]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_unused_input_left [Inhabited α] (f : α → β → σ → σ × γ)
    (h : ∀ a b s, f default b s = f a b s) :
    mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s

Proof state:
case snoc
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
n✝ : ℕ
xs : Vector α n✝
ys : Vector β n✝
x : α
y : β
ih : ∀ {s : σ}, mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s
s : σ
⊢ mapAccumr₂ f (xs.snoc x) (ys.snoc y) s = mapAccumr (fun b s => f default b s) (ys.snoc y) s

Tactic:
simp [h x y s, ih]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs : Vector α n
ys : Vector β n
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
⊢ mapAccumr₂ f xs ys s = mapAccumr (fun b s => f default b s) ys s

Tactic:
induction xs, ys using Vector.revInductionOn₂ generalizing s with
| nil => rfl
| snoc xs ys x y ih => simp [h x y s, ih]

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_5
n : ℕ
inst✝ : Inhabited α
f : α → β → σ → σ × γ
h : ∀ (a : α) (b : β) (s : σ), f default b s = f a b s
s : σ
⊢ mapAccumr₂ f nil nil s = mapAccumr (fun b s => f default b s) nil s

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem support_gen_of_gen' {S : Set R[M]} (hS : Algebra.adjoin R S = ⊤) :
    Algebra.adjoin R (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤

Tactic:
suffices (of' R M '' ⋃ f ∈ S, (f.support : Set M)) = ⋃ f ∈ S, of' R M '' (f.support : Set M) by
  rw [this]
  exact support_gen_of_gen hS

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support) = ⊤

Tactic:
exact support_gen_of_gen hS

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support
⊢ adjoin R (of' R M '' ⋃ f ∈ S, ↑f.support) = ⊤

Tactic:
rw [this]

Result:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
this : of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support
⊢ adjoin R (⋃ f ∈ S, of' R M '' ↑f.support) = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
inst✝ : AddMonoid M
S : Set R[M]
hS : adjoin R S = ⊤
⊢ of' R M '' ⋃ f ∈ S, ↑f.support = ⋃ f ∈ S, of' R M '' ↑f.support

Tactic:
simp only [Set.image_iUnion]

Result:
no goals
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem op_smul_set_smul_eq_smul_smul_set (a : α) (s : Set β) (t : Set γ)
    (h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c) : (op a • s) • t = s • a • t

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
⊢ (op a • s) • t = s • a • t

Tactic:
ext

Result:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t

Proof state:
case h
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : SMul αᵐᵒᵖ β
inst✝¹ : SMul β γ
inst✝ : SMul α γ
a : α
s : Set β
t : Set γ
h : ∀ (a : α) (b : β) (c : γ), (op a • b) • c = b • a • c
x✝ : γ
⊢ x✝ ∈ (op a • s) • t ↔ x✝ ∈ s • a • t

Tactic:
simp [mem_smul, mem_smul_set, h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma addPolynomial_slope {x₁ x₂ y₁ y₂ : F} (h₁ : W.Equation x₁ y₁) (h₂ : W.Equation x₂ y₂)
    (hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)) : W.addPolynomial x₁ y₁ (W.slope x₁ x₂ y₁ y₂) =
      -((X - C x₁) * (X - C x₂) * (X - C (W.addX x₁ x₂ <| W.slope x₁ x₂ y₁ y₂)))

Proof state:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -W.slope x₁ x₂ y₁ y₂ ^ 2 - W.a₁ * W.slope x₁ x₂ y₁ y₂ + W.a₂,
      c := 2 * x₁ * W.slope x₁ x₂ y₁ y₂ ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * W.slope x₁ x₂ y₁ y₂ + (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * W.slope x₁ x₂ y₁ y₂ ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * W.slope x₁ x₂ y₁ y₂ -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂) + x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂),
      d := -(x₁ * x₂ * W.addX x₁ x₂ (W.slope x₁ x₂ y₁ y₂)) }

Tactic:
rw [slope_of_X_ne hx]

Result:
case neg
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ = x₂
⊢ { a := 1, b := -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂,
      c :=
        2 * x₁ * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (W.a₁ * x₁ - 2 * y₁ - W.a₃) * ((y₁ - y₂) / (x₁ - x₂)) +
          (-W.a₁ * y₁ + W.a₄),
      d :=
        -x₁ ^ 2 * ((y₁ - y₂) / (x₁ - x₂)) ^ 2 + (2 * x₁ * y₁ + W.a₃ * x₁) * ((y₁ - y₂) / (x₁ - x₂)) -
          (y₁ ^ 2 + W.a₃ * y₁ - W.a₆) } =
    { a := 1, b := -(x₁ + x₂ + W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))),
      c := x₁ * x₂ + x₁ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)) + x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂)),
      d := -(x₁ * x₂ * W.addX x₁ x₂ ((y₁ - y₂) / (x₁ - x₂))) }

Proof state:
case neg.b
F : Type u
inst✝ : Field F
W : Affine F
x₁ x₂ y₁ y₂ : F
h₁ : y₁ ^ 2 + W.a₁ * x₁ * y₁ + W.a₃ * y₁ = x₁ ^ 3 + W.a₂ * x₁ ^ 2 + W.a₄ * x₁ + W.a₆
h₂ : y₂ ^ 2 + W.a₁ * x₂ * y₂ + W.a₃ * y₂ = x₂ ^ 3 + W.a₂ * x₂ ^ 2 + W.a₄ * x₂ + W.a₆
hxy : ¬(x₁ = x₂ ∧ y₁ = W.negY x₂ y₂)
hx : ¬x₁ - x₂ = 0
⊢ -((y₁ - y₂) / (x₁ - x₂)) ^ 2 - W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) + W.a₂ =
    -(x₁ + x₂ + (((y₁ - y₂) / (x₁ - x₂)) ^ 2 + W.a₁ * ((y₁ - y₂) / (x₁ - x₂)) - W.a₂ - x₁ - x₂))

Tactic:
ring1

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem cylinder_eq_cylinder_union [DecidableEq ι] (I : Finset ι) (S : Set (∀ i : I, α i))
    (J : Finset ι) :
    cylinder I S =
      cylinder (I ∪ J) (Finset.restrict₂ Finset.subset_union_left ⁻¹' S)

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
J : Finset ι
⊢ cylinder I S = cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

Tactic:
ext1 f

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
J : Finset ι
f : (i : ι) → α i
⊢ f ∈ cylinder I S ↔ f ∈ cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝ : DecidableEq ι
I : Finset ι
S : Set ((i : { x // x ∈ I }) → α ↑i)
J : Finset ι
f : (i : ι) → α i
⊢ f ∈ cylinder I S ↔ f ∈ cylinder (I ∪ J) (Finset.restrict₂ ⋯ ⁻¹' S)

Tactic:
simp only [mem_cylinder, Finset.restrict_def, Finset.restrict₂_def, mem_preimage]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem of_natCast {α} [AddMonoidWithOne α] (n : ℕ) : ((n : Num) : α) = n

Proof state:
α : Type u_1
inst✝ : AddMonoidWithOne α
n : ℕ
⊢ ↑↑n = ↑n

Tactic:
rw [← cast_to_nat, to_of_nat]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem le_sup_iff : a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
h : a ≤ b ⊔ c
bc : b ≤ c
⊢ a ≤ c

Tactic:
rwa [sup_eq_right.2 bc] at h

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
h : a ≤ b ⊔ c
bc : c ≤ b
⊢ a ≤ b

Tactic:
rwa [sup_eq_left.2 bc] at h

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a b c : α
⊢ a ≤ b ⊔ c ↔ a ≤ b ∨ a ≤ c

Tactic:
exact ⟨fun h =>
  (le_total c b).imp
    (fun bc => by rwa [sup_eq_left.2 bc] at h)
    (fun bc => by rwa [sup_eq_right.2 bc] at h),
  fun h => h.elim le_sup_of_le_left le_sup_of_le_right⟩

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
/-- `eqToHom h` is heterogeneously equal to the identity of its codomain. -/
lemma eqToHom_heq_id_cod (X Y : C) (h : X = Y) : HEq (eqToHom h) (𝟙 Y)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
h : X = Y
⊢ HEq (eqToHom h) (𝟙 Y)

Tactic:
subst h

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ HEq (eqToHom ⋯) (𝟙 X)

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ HEq (eqToHom ⋯) (𝟙 X)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem zipIdx_map (l : List α) (k : Nat) (f : α → β) :
    zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id)

Proof state:
case cons
α : Type u_1
β : Type u_2
k : Nat
f : α → β
hd : α
tl : List α
IH : (map f tl).zipIdx k = map (Prod.map f id) (tl.zipIdx k)
⊢ (f hd, k) :: map ((Prod.map id fun x => x + 1) ∘ Prod.map f id) (tl.zipIdx k) =
    Prod.map f id (hd, k) :: map (Prod.map f id ∘ Prod.map id fun x => x + 1) (tl.zipIdx k)

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
k : Nat
f : α → β
hd : α
tl : List α
IH : (map f tl).zipIdx k = map (Prod.map f id) (tl.zipIdx k)
⊢ (map f (hd :: tl)).zipIdx k = map (Prod.map f id) ((hd :: tl).zipIdx k)

Tactic:
rw [map_cons, zipIdx_cons', zipIdx_cons', map_cons, map_map, IH, map_map]

Result:
case cons
α : Type u_1
β : Type u_2
k : Nat
f : α → β
hd : α
tl : List α
IH : (map f tl).zipIdx k = map (Prod.map f id) (tl.zipIdx k)
⊢ (f hd, k) :: map ((Prod.map id fun x => x + 1) ∘ Prod.map f id) (tl.zipIdx k) =
    Prod.map f id (hd, k) :: map (Prod.map f id ∘ Prod.map id fun x => x + 1) (tl.zipIdx k)

Proof state:
case nil
α : Type u_1
β : Type u_2
k : Nat
f : α → β
⊢ (map f []).zipIdx k = map (Prod.map f id) ([].zipIdx k)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : List α
k : Nat
f : α → β
⊢ (map f l).zipIdx k = map (Prod.map f id) (l.zipIdx k)

Tactic:
induction l with
| nil => rfl
| cons hd tl IH =>
  rw [map_cons, zipIdx_cons', zipIdx_cons', map_cons, map_map, IH, map_map]
  rfl

Result:
no goals
-- Mathlib/Logic/Function/ULift.lean
theorem ULift.down_injective {α : Sort _} : Function.Injective (@ULift.down α)
  | ⟨a⟩, ⟨b⟩, _ => by congr

Proof state:
α : Type u_1
a b : α
x✝ : { down := a }.down = { down := b }.down
⊢ { down := a } = { down := b }

Tactic:
congr

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem coordChange_same_apply (e : Trivialization F proj) {b : B} (h : b ∈ e.baseSet) (x : F) :
    e.coordChange e b x = x

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
b : B
h : b ∈ e.baseSet
x : F
⊢ e.coordChange e b x = x

Tactic:
rw [coordChange, e.apply_symm_apply' h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem ContinuousMapZero.integral_apply {R : Type*} [NormedCommRing R] [Zero Y]
    [NormedAlgebra ℝ R] [CompleteSpace R] {f : X → C(Y, R)₀}
    (hf : MeasureTheory.Integrable f μ) (y : Y) :
    (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁶ : MeasurableSpace X
μ : Measure X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CompactSpace Y
R : Type u_6
inst✝³ : NormedCommRing R
inst✝² : Zero Y
inst✝¹ : NormedAlgebra ℝ R
inst✝ : CompleteSpace R
f : X → C(Y, R)₀
hf : Integrable f μ
y : Y
⊢ (∫ (x : X), f x ∂μ) y = ∫ (x : X), (f x) y ∂μ

Tactic:
calc (∫ x, f x ∂μ) y = ContinuousMapZero.evalCLM ℝ y (∫ x, f x ∂μ) := rfl
  _ = ∫ x, ContinuousMapZero.evalCLM ℝ y (f x) ∂μ :=
        (ContinuousLinearMap.integral_comp_comm _ hf).symm
  _ = _ := rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem sub_apply [IsFiniteMeasure ν] (h₁ : MeasurableSet s) (h₂ : ν ≤ μ) :
    (μ - ν) s = μ s - ν s

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ ν t + measure_sub t = μ t

Tactic:
rw [MeasureTheory.Measure.ofMeasurable_apply _ h_t_measurable_set, add_comm,
  tsub_add_cancel_of_le (h₂ t)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
⊢ ν + measure_sub = μ

Tactic:
ext1 t h_t_measurable_set

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
t : Set α
h_t_measurable_set : MeasurableSet t
⊢ (ν + measure_sub) t = μ t

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ measure_sub s = μ s - ν s

Tactic:
apply Measure.ofMeasurable_apply _ h₁

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ (μ - ν) s = μ s - ν s

Tactic:
rw [h_measure_sub_eq]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
inst✝ : IsFiniteMeasure ν
h₁ : MeasurableSet s
h₂ : ν ≤ μ
measure_sub : Measure α := ofMeasurable (fun t x => μ t - ν t) ⋯ ⋯
h_measure_sub_add : ν + measure_sub = μ
h_measure_sub_eq : μ - ν = measure_sub
⊢ measure_sub s = μ s - ν s
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} :
    Equicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, Equicontinuous (uα := u k) F

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Equicontinuous F ↔ ∀ (k : κ), Equicontinuous F

Tactic:
simp_rw [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace]

Result:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous (⇑ofFun ∘ swap F)

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
⊢ Continuous (⇑ofFun ∘ swap F) ↔ ∀ (k : κ), Continuous (⇑ofFun ∘ swap F)

Tactic:
rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get_insertIfNew [EquivBEq α] [LawfulHashable α] {k a : α} {v : β} {h₁} :
    get (m.insertIfNew k v) a h₁ =
      if h₂ : k == a ∧ ¬k ∈ m then v else get m a (mem_of_mem_insertIfNew' h₁ h₂)

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h₂ : (k == a) = true ∧ ¬k ∈ m then v else get m a ⋯

Tactic:
simp only [mem_iff_contains, Bool.not_eq_true]

Result:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h : (k == a) = true ∧ m.contains k = false then v else get m a ⋯

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k a : α
v : β
h₁ : a ∈ m.insertIfNew k v
⊢ get (m.insertIfNew k v) a h₁ = if h : (k == a) = true ∧ m.contains k = false then v else get m a ⋯

Tactic:
exact Raw₀.Const.get_insertIfNew ⟨m.1, _⟩ m.2

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.natDegree_map [Semiring S] [Nontrivial S] {P : R[X]} (hmo : P.Monic) (f : R →+* S) :
    (P.map f).natDegree = P.natDegree

Proof state:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0

Tactic:
rw [coeff_map, Monic.coeff_natDegree hmo, RingHom.map_one]

Result:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ 1 ≠ 0

Proof state:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).natDegree = P.natDegree

Tactic:
refine le_antisymm natDegree_map_le (le_natDegree_of_ne_zero ?_)

Result:
R : Type u
S : Type v
inst✝² : Semiring R
inst✝¹ : Semiring S
inst✝ : Nontrivial S
P : R[X]
hmo : P.Monic
f : R →+* S
⊢ (Polynomial.map f P).coeff P.natDegree ≠ 0
-- Mathlib/FieldTheory/LinearDisjoint.lean
theorem linearDisjoint_iff' :
    A.LinearDisjoint B ↔ A.toSubalgebra.LinearDisjoint B.toSubalgebra

Proof state:
case a.h.e'_7.h
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
x✝ : E
⊢ x✝ ∈ (IsScalarTower.toAlgHom F (↥B) E).range ↔ x✝ ∈ B.toSubalgebra

Tactic:
simp

Result:
no goals

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ A.LinearDisjoint ↥B ↔ A.LinearDisjoint B.toSubalgebra

Tactic:
rw [linearDisjoint_iff]

Result:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ A.LinearDisjoint (IsScalarTower.toAlgHom F (↥B) E).range ↔ A.LinearDisjoint B.toSubalgebra

Proof state:
case a.h.e'_7
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ (IsScalarTower.toAlgHom F (↥B) E).range = B.toSubalgebra

Tactic:
ext

Result:
case a.h.e'_7.h
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
x✝ : E
⊢ x✝ ∈ (IsScalarTower.toAlgHom F (↥B) E).range ↔ x✝ ∈ B.toSubalgebra

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ A.LinearDisjoint (IsScalarTower.toAlgHom F (↥B) E).range ↔ A.LinearDisjoint B.toSubalgebra

Tactic:
congr!

Result:
case a.h.e'_7
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
⊢ (IsScalarTower.toAlgHom F (↥B) E).range = B.toSubalgebra
-- Mathlib/LinearAlgebra/Dual.lean
theorem map_eval_injective : (Submodule.map (eval K V)).Injective

Proof state:
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Injective (Submodule.map (eval K V))

Tactic:
apply Submodule.map_injective_of_injective

Result:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Injective ⇑(eval K V)

Proof state:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ Function.Injective ⇑(eval K V)

Tactic:
rw [← LinearMap.ker_eq_bot]

Result:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ ker (eval K V) = ⊥

Proof state:
case hf
K : Type uK
V : Type uV
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Projective K V
⊢ ker (eval K V) = ⊥

Tactic:
exact eval_ker K V

Result:
no goals