harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sigma.lean
theorem lookupAll_sublist (a : α) : ∀ l : List (Sigma β), (lookupAll a l).map (Sigma.mk a) <+ l
  | [] => by simp
  | ⟨a', b'⟩ :: l => by
    by_cases h : a = a'
    · subst h
      simp only [ne_eq, not_true, lookupAll_cons_eq, List.map]
      exact (lookupAll_sublist a l).cons₂ _
    · simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]
      exact (lookupAll_sublist a l).cons _

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
⊢ map (Sigma.mk a) (lookupAll a []) <+ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
by_cases h : a = a'

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ ⟨a, b'⟩ :: map (Sigma.mk a) (lookupAll a l) <+ ⟨a, b'⟩ :: l

Tactic:
exact (lookupAll_sublist a l).cons₂ _

Result:
no goals

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a l) <+ ⟨a', b'⟩ :: l

Tactic:
exact (lookupAll_sublist a l).cons _

Result:
no goals

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk a) (lookupAll a (⟨a, b'⟩ :: l)) <+ ⟨a, b'⟩ :: l

Tactic:
simp only [ne_eq, not_true, lookupAll_cons_eq, List.map]

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ ⟨a, b'⟩ :: map (Sigma.mk a) (lookupAll a l) <+ ⟨a, b'⟩ :: l

Proof state:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
subst h

Result:
case pos
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a : α
l : List (Sigma β)
b' : β a
⊢ map (Sigma.mk a) (lookupAll a (⟨a, b'⟩ :: l)) <+ ⟨a, b'⟩ :: l

Proof state:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a (⟨a', b'⟩ :: l)) <+ ⟨a', b'⟩ :: l

Tactic:
simp only [ne_eq, h, not_false_iff, lookupAll_cons_ne]

Result:
case neg
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a a' : α
b' : β a'
l : List (Sigma β)
h : ¬a = a'
⊢ map (Sigma.mk a) (lookupAll a l) <+ ⟨a', b'⟩ :: l
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem baseChange_add : (f + g).baseChange A = f.baseChange A + g.baseChange A

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
⊢ baseChange A (f + g) = baseChange A f + baseChange A g

Tactic:
ext

Result:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝

Proof state:
case a.h.h
R : Type u_1
A : Type u_2
M : Type u_4
N : Type u_5
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring A
inst✝⁴ : Algebra R A
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
f g : M →ₗ[R] N
x✝ : M
⊢ ((AlgebraTensorModule.curry (baseChange A (f + g))) 1) x✝ =
    ((AlgebraTensorModule.curry (baseChange A f + baseChange A g)) 1) x✝

Tactic:
simp [baseChange_eq_ltensor, -baseChange_tmul]

Result:
no goals
-- Mathlib/Algebra/FreeAlgebra.lean
theorem lift_unique (f : X → A) (g : FreeAlgebra R X →ₐ[R] A) :
    (g : FreeAlgebra R X → A) ∘ ι R = f ↔ g = lift R f

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔ g = (lift R) f

Tactic:
rw [← (lift R).symm_apply_eq, lift]

Result:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔
    { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm g = f

Proof state:
R : Type u_1
inst✝² : CommSemiring R
X : Type u_2
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : X → A
g : FreeAlgebra R X →ₐ[R] A
⊢ ⇑g ∘ ι R = f ↔
    { toFun := FreeAlgebra.liftAux R, invFun := fun F => ⇑F ∘ ι R, left_inv := ⋯, right_inv := ⋯ }.symm g = f

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Submodule.lean
theorem lTensorOne'_tmul (y : R) (n : N) :
    N.lTensorOne' (algebraMap R _ y ⊗ₜ[R] n) = y • n := Subtype.val_injective <| by
  simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
    LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]
  exact mulMap_tmul _ N _ _

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = (algebraMap R S) y * ↑n

Tactic:
exact mulMap_tmul _ N _ _

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ↑(N.lTensorOne' ((algebraMap R ↥⊥) y ⊗ₜ[R] n)) = ↑(y • n)

Tactic:
simp_rw [lTensorOne', LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.coe_ofEq_apply, LinearMap.codRestrict_apply, SetLike.val_smul, Algebra.smul_def]

Result:
R : Type u
S : Type v
inst✝² : CommSemiring R
inst✝¹ : Semiring S
inst✝ : Algebra R S
N : Submodule R S
y : R
n : ↥N
⊢ ((Subalgebra.toSubmodule ⊥).mulMap N) ((algebraMap R ↥⊥) y ⊗ₜ[R] n) = (algebraMap R S) y * ↑n
-- Mathlib/Data/Fin/Basic.lean
/-- Given a fixed pivot `p : Fin (n + 1)`, `p.succAbove` is injective. -/
lemma succAbove_right_injective : Injective p.succAbove

Proof state:
n : ℕ
p : Fin (n + 1)
⊢ Injective p.succAbove

Tactic:
rintro i j hij

Result:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : p.succAbove i = p.succAbove j
⊢ i = j

Proof state:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
cases hi <| Nat.lt_trans i.castSucc_lt_succ hj

Result:
no goals

Proof state:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
rw [hij] at hi

Result:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Proof state:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
rw [← hij] at hj

Result:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j

Proof state:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
⊢ i = j

Tactic:
split_ifs at hij with hi hj hj

Result:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j

case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j

case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Proof state:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
cases hj <| Nat.lt_trans j.castSucc_lt_succ hi

Result:
no goals

Proof state:
case neg
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
exact succ_injective _ hij

Result:
no goals

Proof state:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : p.succAbove i = p.succAbove j
⊢ i = j

Tactic:
unfold succAbove at hij

Result:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
⊢ i = j

Proof state:
case pos
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : j.castSucc < p
hij : i.castSucc = j.castSucc
⊢ i = j

Tactic:
exact castSucc_injective _ hij

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_perm {s : Set α} {σ : Equiv.Perm α} (hs : { a : α | σ a ≠ a } ⊆ s) : σ '' s = s

Proof state:
case h.inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
h : σ ((Equiv.symm σ) i) = (Equiv.symm σ) i
⊢ σ i = i

Tactic:
convert congr_arg σ h <;> exact (σ.apply_symm_apply _).symm

Result:
no goals

Proof state:
case h.inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
refine iff_of_true ⟨σ.symm i, hs fun h => hi ?_, σ.apply_symm_apply _⟩ (hs hi)

Result:
case h.inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
h : σ ((Equiv.symm σ) i) = (Equiv.symm σ) i
⊢ σ i = i

Proof state:
case h
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
obtain hi | hi := eq_or_ne (σ i) i

Result:
case h.inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

case h.inr
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i ≠ i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Proof state:
case h.inl.intro.intro
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
j : α
hj : j ∈ s
h : σ j = i
⊢ i ∈ s

Tactic:
rwa [σ.injective (hi.trans h.symm)]

Result:
no goals

Proof state:
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
⊢ ⇑σ '' s = s

Tactic:
ext i

Result:
case h
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Proof state:
case h.inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s → i ∈ s

Tactic:
rintro ⟨j, hj, h⟩

Result:
case h.inl.intro.intro
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
j : α
hj : j ∈ s
h : σ j = i
⊢ i ∈ s

Proof state:
case h.inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s ↔ i ∈ s

Tactic:
refine ⟨?_, fun h => ⟨i, h, hi⟩⟩

Result:
case h.inl
α : Type u_1
s : Set α
σ : Equiv.Perm α
hs : {a | σ a ≠ a} ⊆ s
i : α
hi : σ i = i
⊢ i ∈ ⇑σ '' s → i ∈ s
-- Mathlib/LinearAlgebra/Dual.lean
@[simp]
lemma coe_dualAnnihilator_span (s : Set M) :
    ((span R s).dualAnnihilator : Set (Module.Dual R M)) = {f | s ⊆ LinearMap.ker f}

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ f ∈ ↑(span R s).dualAnnihilator ↔ f ∈ {f | s ⊆ ↑(LinearMap.ker f)}

Tactic:
simp only [SetLike.mem_coe, mem_dualAnnihilator, Set.mem_setOf_eq, ← LinearMap.mem_ker]

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ (∀ w ∈ span R s, w ∈ LinearMap.ker f) ↔ s ⊆ ↑(LinearMap.ker f)

Proof state:
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ ↑(span R s).dualAnnihilator = {f | s ⊆ ↑(LinearMap.ker f)}

Tactic:
ext f

Result:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ f ∈ ↑(span R s).dualAnnihilator ↔ f ∈ {f | s ⊆ ↑(LinearMap.ker f)}

Proof state:
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
f : Dual R M
⊢ (∀ w ∈ span R s, w ∈ LinearMap.ker f) ↔ s ⊆ ↑(LinearMap.ker f)

Tactic:
exact span_le

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_ge_eq_sup : (⨆ j ≥ i, f j) = f i ⊔ (⨆ j > i, f j)

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ ⨆ j, ⨆ (_ : j ≥ i), f j = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
rw [iSup_split_single _ i]

Result:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Proof state:
α : Type u_1
inst✝¹ : CompleteLattice α
ι : Type u_8
inst✝ : PartialOrder ι
f : ι → α
i : ι
⊢ (⨆ (_ : i ≥ i), f i) ⊔ ⨆ i_1, ⨆ (_ : i_1 ≠ i), ⨆ (_ : i_1 ≥ i), f i_1 = f i ⊔ ⨆ j, ⨆ (_ : j > i), f j

Tactic:
simp only [ge_iff_le, le_refl, iSup_pos, ne_comm, iSup_and', gt_iff_lt, lt_iff_le_and_ne,
  and_comm]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma one_le_zpow_iff_right₀ (ha : 1 < a) : 1 ≤ a ^ n ↔ 0 ≤ n

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulStrictMono G₀
n : ℤ
ha : 1 < a
⊢ 1 ≤ a ^ n ↔ 0 ≤ n

Tactic:
simp [← zpow_le_zpow_iff_right₀ ha]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformField.lean
theorem continuous_hatInv [CompletableTopField K] {x : hat K} (h : x ≠ 0) :
    ContinuousAt hatInv x

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ (fun x => ↑x⁻¹) = fun x => (fun y => ↑y) ((fun x => x⁻¹) x)

Tactic:
simp

Result:
no goals

Proof state:
case a.hm
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this✝ : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
this : (Filter.comap coe' (𝓝 y)).NeBot
⊢ Filter.comap (fun p => (↑p.1, ↑p.2)) (uniformity (hat K)) ≤ uniformity K

Tactic:
rw [Completion.comap_coe_eq_uniformity]

Result:
no goals

Proof state:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
  by_contra h
  exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm

Result:
case a
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this : (fun x => ↑x⁻¹) = (fun y => ↑y) ∘ fun x => x⁻¹
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Proof state:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x

Tactic:
refine isDenseInducing_coe.continuousAt_extend ?_

Result:
K : Type u_1
inst✝² : Field K
inst✝¹ : UniformSpace K
inst✝ : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ c, Tendsto (fun x => ↑x⁻¹) (Filter.comap coe' (𝓝 x)) (𝓝 c)
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Iic_diff_Ioc_self_of_le (hab : a ≤ b) : Iic b \ Ioc a b = Iic a

Proof state:
α : Type u_2
a b : α
inst✝² : LinearOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : LocallyFiniteOrderBot α
hab : a ≤ b
⊢ Iic b \ Ioc a b = Iic a

Tactic:
rw [Iic_diff_Ioc, min_eq_left hab]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem lipschitzOnWith_iff_norm_div_le {f : E → F} {C : ℝ≥0} :
    LipschitzOnWith C f s ↔ ∀ ⦃x⦄, x ∈ s → ∀ ⦃y⦄, y ∈ s → ‖f x / f y‖ ≤ C * ‖x / y‖

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
s : Set E
f : E → F
C : ℝ≥0
⊢ LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖

Tactic:
simp only [lipschitzOnWith_iff_dist_le_mul, dist_eq_norm_div]

Result:
no goals
-- Mathlib/Topology/Algebra/GroupWithZero.lean
theorem Filter.tendsto_mul_iff_of_ne_zero [T1Space G₀] {f g : α → G₀} {l : Filter α} {x y : G₀}
    (hg : Tendsto g l (𝓝 y)) (hy : y ≠ 0) :
    Tendsto (fun n => f n * g n) l (𝓝 <| x * y) ↔ Tendsto f l (𝓝 x)

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 x)

Tactic:
rw [← mul_div_cancel_right₀ x hy]

Result:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 (x * y / y))

Tactic:
refine Tendsto.congr' ?_ (hfg.div hg hy)

Result:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ (fun n => f n * g n) / g =ᶠ[l] f

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ (fun n => f n * g n) / g =ᶠ[l] f

Tactic:
exact (hg.eventually_ne hy).mono fun n hn => mul_div_cancel_right₀ _ hn

Result:
no goals

Proof state:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
⊢ Tendsto (fun n => f n * g n) l (𝓝 (x * y)) ↔ Tendsto f l (𝓝 x)

Tactic:
refine ⟨fun hfg => ?_, fun hf => hf.mul hg⟩

Result:
α : Type u_1
G₀ : Type u_3
inst✝⁴ : GroupWithZero G₀
inst✝³ : TopologicalSpace G₀
inst✝² : HasContinuousInv₀ G₀
inst✝¹ : ContinuousMul G₀
inst✝ : T1Space G₀
f g : α → G₀
l : Filter α
x y : G₀
hg : Tendsto g l (𝓝 y)
hy : y ≠ 0
hfg : Tendsto (fun n => f n * g n) l (𝓝 (x * y))
⊢ Tendsto f l (𝓝 x)
-- Mathlib/Data/Matroid/Closure.lean
lemma mem_closure_of_mem' (M : Matroid α) (heX : e ∈ X) (h : e ∈ M.E

Proof state:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.closure (X ∩ M.E)

Tactic:
exact M.mem_closure_of_mem ⟨heX, h⟩

Result:
no goals

Proof state:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.closure X

Tactic:
rw [← closure_inter_ground]

Result:
α : Type u_2
X : Set α
e : α
M : Matroid α
heX : e ∈ X
h : autoParam (e ∈ M.E) _auto✝
⊢ e ∈ M.closure (X ∩ M.E)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem sub_emod (a b n : Int) : (a - b) % n = (a % n - b % n) % n

Proof state:
a b n : Int
⊢ (a - b) % n = (a % n - b % n) % n

Tactic:
apply (emod_add_cancel_right b).mp

Result:
a b n : Int
⊢ (a - b + b) % n = (a % n - b % n + b) % n

Proof state:
a b n : Int
⊢ (a - b + b) % n = (a % n - b % n + b) % n

Tactic:
rw [Int.sub_add_cancel, ← Int.add_emod_emod, Int.sub_add_cancel, emod_emod]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem toBlock_diagonal_self (d : m → α) (p : m → Prop) :
    Matrix.toBlock (diagonal d) p p = diagonal fun i : Subtype p => d ↑i

Proof state:
case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

Tactic:
simp [One.one, h, Subtype.val_injective.ne h]

Result:
no goals

Proof state:
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
⊢ (diagonal d).toBlock p p = diagonal fun i => d ↑i

Tactic:
ext i j

Result:
case a
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

Proof state:
case a
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

Tactic:
by_cases h : i = j

Result:
case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

case neg
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : ¬i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

Proof state:
case pos
m : Type u_2
α : Type u_12
inst✝¹ : DecidableEq m
inst✝ : Zero α
d : m → α
p : m → Prop
i j : { a // p a }
h : i = j
⊢ (diagonal d).toBlock p p i j = diagonal (fun i => d ↑i) i j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Data/Set/Function.lean
protected lemma bijOn (h : ∀ a, e a ∈ t ↔ a ∈ s) : BijOn e s t :=
  e.bijOn' (fun _ ↦ (h _).2) fun b hb ↦ (h _).1 <| by rwa [apply_symm_apply]

Proof state:
α : Type u_1
β : Type u_2
e : α ≃ β
s : Set α
t : Set β
h : ∀ (a : α), e a ∈ t ↔ a ∈ s
b : β
hb : b ∈ t
⊢ e (e.symm b) ∈ t

Tactic:
rwa [apply_symm_apply]

Result:
no goals