harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem subset_tangentCone_prod_right {t : Set F} {y : F} (hs : x ∈ closure s) :
    LinearMap.inr 𝕜 E F '' tangentConeAt 𝕜 t y ⊆ tangentConeAt 𝕜 (s ×ˢ t) (x, y)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
hs : x ∈ closure s
w : F
c : ℕ → 𝕜
d : ℕ → F
hd : ∀ᶠ (n : ℕ) in atTop, y + d n ∈ t
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
⊢ ∀ (n : ℕ), ∃ d', x + d' ∈ s ∧ ‖c n • d'‖ < (1 / 2) ^ n

Tactic:
intro n

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
s : Set E
t : Set F
y : F
hs : x ∈ closure s
w : F
c : ℕ → 𝕜
d : ℕ → F
hd : ∀ᶠ (n : ℕ) in atTop, y + d n ∈ t
hc : Tendsto (fun n => ‖c n‖) atTop atTop
hy : Tendsto (fun n => c n • d n) atTop (𝓝 w)
n : ℕ
⊢ ∃ d', x + d' ∈ s ∧ ‖c n • d'‖ < (1 / 2) ^ n
-- Mathlib/Data/ZMod/Basic.lean
lemma lift_injective {f : {f : ℤ →+ A // f n = 0}} :
    Injective (lift n f) ↔ ∀ m, f.1 m = 0 → (m : ZMod n) = 0

Proof state:
n : ℕ
A : Type u_2
inst✝ : AddGroup A
f : { f // f ↑n = 0 }
⊢ Injective ⇑((lift n) f) ↔ ∀ (m : ℤ), ↑f m = 0 → ↑m = 0

Tactic:
simp only [← AddMonoidHom.ker_eq_bot_iff, eq_bot_iff, SetLike.le_def,
  ZMod.intCast_surjective.forall, ZMod.lift_coe, AddMonoidHom.mem_ker, AddSubgroup.mem_bot]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem append_concat (a : α) (l₁ l₂ : List α) : l₁ ++ concat l₂ a = concat (l₁ ++ l₂) a

Proof state:
α : Type u_1
a : α
l₁ l₂ : List α
⊢ l₁ ++ l₂.concat a = (l₁ ++ l₂).concat a

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem ucs_comap_incl (k : ℕ) :
    ((⊥ : LieSubmodule R L M).ucs k).comap N.incl = (⊥ : LieSubmodule R L N).ucs k

Proof state:
case succ
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
ih : comap N.incl (ucs k ⊥) = ucs k ⊥
⊢ comap N.incl (ucs (k + 1) ⊥) = ucs (k + 1) ⊥

Tactic:
simp [← ih]

Result:
no goals

Proof state:
case zero
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ comap N.incl (ucs 0 ⊥) = ucs 0 ⊥

Tactic:
exact N.ker_incl

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ comap N.incl (ucs k ⊥) = ucs k ⊥

Tactic:
induction k with
| zero => exact N.ker_incl
| succ k ih => simp [← ih]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem nnnorm_approxOn_le [OpensMeasurableSpace E] {f : β → E} (hf : Measurable f) {s : Set E}
    {y₀ : E} (h₀ : y₀ ∈ s) [SeparableSpace s] (x : β) (n : ℕ) :
    ‖approxOn f hf s y₀ h₀ n x - f x‖₊ ≤ ‖f x - y₀‖₊

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Tactic:
have := edist_approxOn_le hf h₀ x n

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ↑‖f x - y₀‖₊
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Tactic:
exact mod_cast this

Result:
no goals

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (f x) y₀
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Tactic:
simp only [edist_nndist, nndist_eq_nnnorm] at this

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : ↑‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ↑‖f x - y₀‖₊
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Proof state:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist y₀ (f x)
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊

Tactic:
rw [edist_comm y₀] at this

Result:
β : Type u_2
E : Type u_4
inst✝⁴ : MeasurableSpace β
inst✝³ : MeasurableSpace E
inst✝² : NormedAddCommGroup E
inst✝¹ : OpensMeasurableSpace E
f : β → E
hf : Measurable f
s : Set E
y₀ : E
h₀ : y₀ ∈ s
inst✝ : SeparableSpace ↑s
x : β
n : ℕ
this : edist ((approxOn f hf s y₀ h₀ n) x) (f x) ≤ edist (f x) y₀
⊢ ‖(approxOn f hf s y₀ h₀ n) x - f x‖₊ ≤ ‖f x - y₀‖₊
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_erase_eq_nodal_div (hi : i ∈ s) :
    nodal (s.erase i) v = nodal s v / (X - C (v i))

Proof state:
case ha
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ X - C (v i) ≠ 0

Tactic:
exact X_sub_C_ne_zero _

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ nodal (s.erase i) v = nodal s v / (X - C (v i))

Tactic:
rw [nodal_eq_mul_nodal_erase hi, mul_div_cancel_left₀]

Result:
case ha
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v : ι → F
i : ι
hi : i ∈ s
⊢ X - C (v i) ≠ 0
-- Mathlib/MeasureTheory/Covering/Differentiation.lean
theorem ae_tendsto_div : ∀ᵐ x ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Tactic:
have I : ∀ x ∈ w, x ≠ ∞ := fun x xs hx => w_top (hx ▸ xs)

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)

Proof state:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∀ (a : α),
    (∀ c ∈ w,
        ∀ d ∈ w,
          c < d → ¬((∃ᶠ (a : Set α) in v.filterAt a, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt a, d < ρ a / μ a)) →
      ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt a) (𝓝 c)

Tactic:
intro x hx

Result:
case h
α : Type u_1
inst✝⁴ : PseudoMetricSpace α
m0 : MeasurableSpace α
μ : Measure α
v : VitaliFamily μ
inst✝³ : SecondCountableTopology α
inst✝² : BorelSpace α
inst✝¹ : IsLocallyFiniteMeasure μ
ρ : Measure α
inst✝ : IsLocallyFiniteMeasure ρ
hρ : ρ ≪ μ
w : Set ℝ≥0∞
w_count : w.Countable
w_dense : Dense w
left✝ : 0 ∉ w
w_top : ⊤ ∉ w
I : ∀ x ∈ w, x ≠ ⊤
A :
  ∀ c ∈ w,
    ∀ d ∈ w,
      c < d →
        ∀ᵐ (x : α) ∂μ,
          ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
B :
  ∀ᵐ (x : α) ∂μ,
    ∀ c ∈ w,
      ∀ d ∈ w,
        c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
x : α
hx :
  ∀ c ∈ w,
    ∀ d ∈ w, c < d → ¬((∃ᶠ (a : Set α) in v.filterAt x, ρ a / μ a < c) ∧ ∃ᶠ (a : Set α) in v.filterAt x, d < ρ a / μ a)
⊢ ∃ c, Tendsto (fun a => ρ a / μ a) (v.filterAt x) (𝓝 c)
-- Mathlib/Data/Nat/Bits.lean
lemma mod_two_of_bodd (n : ℕ) : n % 2 = (bodd n).toNat

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝ : ∀ (b : Bool), (false && b) = false
⊢ ∀ (b : Bool), (b ^^ false) = b

Tactic:
intro b

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ (b ^^ false) = b

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝ : ∀ (b : Bool), (false && b) = false
b : Bool
⊢ (b ^^ false) = b

Tactic:
cases b <;> rfl

Result:
no goals

Proof state:
n : ℕ
this : (n % 2 + 2 * (n / 2)).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat

Tactic:
simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
  at this

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
b : Bool
⊢ (false && b) = false

Tactic:
cases b <;> rfl

Result:
no goals

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = n.bodd.toNat

Tactic:
have _ : ∀ b, bxor b false = b := by
  intro b
  cases b <;> rfl

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), (b ^^ false) = b
⊢ n % 2 = n.bodd.toNat

Proof state:
n : ℕ
this : (n % 2 + 2 * (n / 2)).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat

Tactic:
simp? [not] at this says
  simp only [bodd_add, bodd_mul, bodd_succ, not, bodd_zero, Bool.false_and, Bool.bne_false]
    at this

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), (b ^^ false) = b
⊢ n % 2 = (n % 2).bodd.toNat

Tactic:
rcases mod_two_eq_zero_or_one n with h | h <;> rw [h] <;> rfl

Result:
no goals

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat

Tactic:
have _ : ∀ b, and false b = false := by
  intro b
  cases b <;> rfl

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝ : ∀ (b : Bool), (false && b) = false
⊢ n % 2 = n.bodd.toNat

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
⊢ ∀ (b : Bool), (false && b) = false

Tactic:
intro b

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
b : Bool
⊢ (false && b) = false

Proof state:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), (b ^^ false) = b
⊢ n % 2 = n.bodd.toNat

Tactic:
rw [← this]

Result:
n : ℕ
this : (n % 2).bodd = n.bodd
x✝¹ : ∀ (b : Bool), (false && b) = false
x✝ : ∀ (b : Bool), (b ^^ false) = b
⊢ n % 2 = (n % 2).bodd.toNat

Proof state:
n : ℕ
⊢ n % 2 = n.bodd.toNat

Tactic:
have := congr_arg bodd (mod_add_div n 2)

Result:
n : ℕ
this : (n % 2 + 2 * (n / 2)).bodd = n.bodd
⊢ n % 2 = n.bodd.toNat
-- Mathlib/Order/Heyting/Boundary.lean
theorem hnot_eq_top_iff_exists_boundary : ￢a = ⊤ ↔ ∃ b, ∂ b = a :=
  ⟨fun h => ⟨a, by rw [boundary, h, inf_top_eq]⟩, by
    rintro ⟨b, rfl⟩
    exact hnot_boundary _⟩

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
⊢ (∃ b, ∂ b = a) → ￢a = ⊤

Tactic:
rintro ⟨b, rfl⟩

Result:
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b : α
⊢ ￢∂ b = ⊤

Proof state:
case intro
α : Type u_1
inst✝ : CoheytingAlgebra α
b : α
⊢ ￢∂ b = ⊤

Tactic:
exact hnot_boundary _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CoheytingAlgebra α
a : α
h : ￢a = ⊤
⊢ ∂ a = a

Tactic:
rw [boundary, h, inf_top_eq]

Result:
no goals
-- Mathlib/RingTheory/OreLocalization/Ring.lean
@[simp]
lemma zsmul_eq_zsmul (n : ℤ) (x : X[S⁻¹]) :
    letI inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℤ) (R := R) (X := X) (S := S)
    HSMul.hSMul (self := @instHSMul _ _ inst.toSMul) n x = n • x

Proof state:
R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x

Tactic:
exact congr($(AddCommGroup.uniqueIntModule.2 inst).smul n x)

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
⊢ n • x = n • x

Tactic:
letI inst := OreLocalization.instModuleOfIsScalarTower (R₀ := ℤ) (R := R) (X := X) (S := S)

Result:
R : Type u_1
inst✝³ : Ring R
S : Submonoid R
inst✝² : OreSet S
X : Type u_2
inst✝¹ : AddCommGroup X
inst✝ : Module R X
n : ℤ
x : OreLocalization S X
inst : Module ℤ (OreLocalization S X) := instModuleOfIsScalarTower
⊢ n • x = n • x
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem continuousAt_eval₂ [TopologicalSpace α] {f : α →ᵤ[𝔖] β} {x : α}
    (h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x) (hc : ContinuousAt (toFun 𝔖 f) x) :
    ContinuousAt (fun fx : (α →ᵤ[𝔖] β) × α ↦ toFun 𝔖 fx.1 fx.2) (f, x)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ U ○ U

Tactic:
rcases h𝔖 with ⟨V, hV, hVx⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ U ○ U

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ ∀ s ∈ 𝓤 β,
    ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
      (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ s ○ s

Tactic:
intro U hU

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ U ○ U

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ ContinuousAt (fun fx => (toFun 𝔖) fx.1 fx.2) (f, x)

Tactic:
rw [ContinuousAt, nhds_eq_comap_uniformity, tendsto_comap_iff, ← lift'_comp_uniformity,
  tendsto_lift']

Result:
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
h𝔖 : ∃ V ∈ 𝔖, V ∈ 𝓝 x
hc : ContinuousAt ((toFun 𝔖) f) x
⊢ ∀ s ∈ 𝓤 β,
    ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
      (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ s ○ s

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : UniformSpace β
𝔖 : Set (Set α)
inst✝ : TopologicalSpace α
f : α →ᵤ[𝔖] β
x : α
hc : ContinuousAt ((toFun 𝔖) f) x
U : Set (β × β)
hU : U ∈ 𝓤 β
V : Set α
hV : V ∈ 𝔖
hVx : V ∈ 𝓝 x
⊢ ∀ᶠ (a : (α →ᵤ[𝔖] β) × α) in 𝓝 (f, x),
    (Prod.mk ((toFun 𝔖) (f, x).1 (f, x).2) ∘ fun fx => (toFun 𝔖) fx.1 fx.2) a ∈ U ○ U

Tactic:
filter_upwards [prod_mem_nhds (UniformOnFun.gen_mem_nhds _ _ _ hV hU)
  (inter_mem hVx <| hc <| UniformSpace.ball_mem_nhds _ hU)]
  with ⟨g, y⟩ ⟨hg, hyV, hy⟩ using ⟨toFun 𝔖 f y, hy, hg y hyV⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem foldr_map (f : α₁ → α₂) (g : α₂ → β → β) (l : Array α₁) (init : β) :
    (l.map f).foldr g init = l.foldr (fun x y => g (f x) y) init

Proof state:
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
l : Array α₁
init : β
⊢ foldr g init (map f l) = foldr (fun x y => g (f x) y) init l

Tactic:
cases l

Result:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
init : β
toList✝ : List α₁
⊢ foldr g init (map f { toList := toList✝ }) = foldr (fun x y => g (f x) y) init { toList := toList✝ }

Proof state:
case mk
α₁ : Type u_1
α₂ : Type u_2
β : Type u_3
f : α₁ → α₂
g : α₂ → β → β
init : β
toList✝ : List α₁
⊢ foldr g init (map f { toList := toList✝ }) = foldr (fun x y => g (f x) y) init { toList := toList✝ }

Tactic:
simp [List.foldr_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem finrank_dualCoannihilator_eq {Φ : Subspace K (Module.Dual K V)} :
    finrank K Φ.dualCoannihilator = finrank K Φ.dualAnnihilator

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(comap (↑(evalEquiv K V)) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)

Tactic:
exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(dualCoannihilator Φ) = finrank K ↥(dualAnnihilator Φ)

Tactic:
rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]

Result:
K : Type u
V : Type v
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
Φ : Subspace K (Dual K V)
⊢ finrank K ↥(comap (↑(evalEquiv K V)) (dualAnnihilator Φ)) = finrank K ↥(dualAnnihilator Φ)
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
theorem preimage_basicOpen {X Y : LocallyRingedSpace.{u}} (f : X ⟶ Y) {U : Opens Y}
    (s : Y.presheaf.obj (op U)) :
    (Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
      @RingedSpace.basicOpen X.toRingedSpace ((Opens.map f.base).obj U) (f.c.app _ s)

Proof state:
case h.h.mp
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ↑((Opens.map f.base).obj (Y.toRingedSpace.basicOpen s)) →
    x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Tactic:
rintro ⟨hxU, hx⟩

Result:
case h.h.mp.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : (ConcreteCategory.hom f.base) x ∈ U
hx : IsUnit ((ConcreteCategory.hom (Y.toRingedSpace.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
⊢ x ∈ ↑(X.toRingedSpace.basicOpen ((ConcreteCategory.hom (f.c.app (op U))) s))

Proof state:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (X.presheaf.germ ((Opens.map f.base).obj U) x hxU))
      ((ConcreteCategory.hom (f.c.app (op U))) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)

Tactic:
rw [← stalkMap_germ_apply] at hx

Result:
case h.h.mpr.intro
X Y : LocallyRingedSpace
f : X ⟶ Y
U : Opens ↑Y.toTopCat
s : ↑(Y.presheaf.obj (op U))
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (Opens.map f.base).obj U
hx :
  IsUnit
    ((ConcreteCategory.hom (Hom.stalkMap f x))
      ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s))
⊢ IsUnit ((ConcreteCategory.hom (Y.presheaf.germ U ((ConcreteCategory.hom f.base) x) hxU)) s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem pow_dvd_pow {m n : Nat} (a : Nat) (h : m ≤ n) : a ^ m ∣ a ^ n

Proof state:
case intro
m n a : Nat
h : m ≤ n
w✝ : Nat
h✝ : n = m + w✝
⊢ a ^ m ∣ a ^ n

Tactic:
case intro k p =>
  subst p
  rw [Nat.pow_add]
  apply Nat.dvd_mul_right

Result:
no goals

Proof state:
m a k : Nat
h : m ≤ m + k
⊢ a ^ m ∣ a ^ m * a ^ k

Tactic:
apply Nat.dvd_mul_right

Result:
no goals

Proof state:
m n a : Nat
h : m ≤ n
k : Nat
p : n = m + k
⊢ a ^ m ∣ a ^ n

Tactic:
subst p

Result:
m a k : Nat
h : m ≤ m + k
⊢ a ^ m ∣ a ^ (m + k)

Proof state:
m n a : Nat
h : m ≤ n
⊢ a ^ m ∣ a ^ n

Tactic:
cases Nat.exists_eq_add_of_le h

Result:
case intro
m n a : Nat
h : m ≤ n
w✝ : Nat
h✝ : n = m + w✝
⊢ a ^ m ∣ a ^ n

Proof state:
m a k : Nat
h : m ≤ m + k
⊢ a ^ m ∣ a ^ (m + k)

Tactic:
rw [Nat.pow_add]

Result:
m a k : Nat
h : m ≤ m + k
⊢ a ^ m ∣ a ^ m * a ^ k
-- Mathlib/AlgebraicGeometry/Restrict.lean
@[reassoc (attr := simp)]
lemma Scheme.Opens.isoOfLE_inv_ι {X : Scheme.{u}} {U V : X.Opens}
    (hUV : U ≤ V) :
    (Scheme.Opens.isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι

Proof state:
X : Scheme
U V : X.Opens
hUV : U ≤ V
⊢ (isoOfLE hUV).inv ≫ (V.ι ⁻¹ᵁ U).ι ≫ V.ι = U.ι

Tactic:
simp [isoOfLE]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem rename (hφ : φ.IsSymmetric) (e : σ ≃ τ) : (rename e φ).IsSymmetric := fun _ => by
  apply rename_injective _ e.symm.injective
  simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id_apply]
  rw [hφ]

Proof state:
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x✝ : Perm τ
⊢ (rename ⇑e.symm) ((rename ⇑x✝) ((rename ⇑e) φ)) = (rename ⇑e.symm) ((rename ⇑e) φ)

Tactic:
simp_rw [rename_rename, ← Equiv.coe_trans, Equiv.self_trans_symm, Equiv.coe_refl, rename_id_apply]

Result:
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x✝ : Perm τ
⊢ (rename ⇑((e.trans x✝).trans e.symm)) φ = φ

Proof state:
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x✝ : Perm τ
⊢ (rename ⇑((e.trans x✝).trans e.symm)) φ = φ

Tactic:
rw [hφ]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x✝ : Perm τ
⊢ (rename ⇑x✝) ((rename ⇑e) φ) = (rename ⇑e) φ

Tactic:
apply rename_injective _ e.symm.injective

Result:
case a
σ : Type u_1
τ : Type u_2
R : Type u_3
inst✝ : CommSemiring R
φ : MvPolynomial σ R
hφ : φ.IsSymmetric
e : σ ≃ τ
x✝ : Perm τ
⊢ (rename ⇑e.symm) ((rename ⇑x✝) ((rename ⇑e) φ)) = (rename ⇑e.symm) ((rename ⇑e) φ)
-- Mathlib/Topology/UnitInterval.lean
theorem mem_iff_one_sub_mem {t : ℝ} : t ∈ I ↔ 1 - t ∈ I

Proof state:
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 ↔ 0 ≤ 1 - t ∧ 1 - t ≤ 1

Tactic:
constructor <;> intro <;> constructor <;> linarith

Result:
no goals

Proof state:
t : ℝ
⊢ t ∈ I ↔ 1 - t ∈ I

Tactic:
rw [mem_Icc, mem_Icc]

Result:
t : ℝ
⊢ 0 ≤ t ∧ t ≤ 1 ↔ 0 ≤ 1 - t ∧ 1 - t ≤ 1