harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem two_pi_pos : 0 < 2 * π

Proof state:
⊢ 0 < 2 * π

Tactic:
linarith [pi_pos]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem AEMeasurable.ennreal_tsum {ι} [Countable ι] {f : ι → α → ℝ≥0∞} {μ : Measure α}
    (h : ∀ i, AEMeasurable (f i) μ) : AEMeasurable (fun x => ∑' i, f i x) μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => ⨆ s, ∑ i ∈ s, f i x) μ

Tactic:
exact .iSup fun s ↦ Finset.aemeasurable_sum s fun i _ => h i

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => ∑' (i : ι), f i x) μ

Tactic:
simp_rw [ENNReal.tsum_eq_iSup_sum]

Result:
α : Type u_1
mα : MeasurableSpace α
ι : Type u_5
inst✝ : Countable ι
f : ι → α → ℝ≥0∞
μ : Measure α
h : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun x => ⨆ s, ∑ i ∈ s, f i x) μ
-- Mathlib/CategoryTheory/Shift/ShiftedHomOpposite.lean
lemma opEquiv_symm_apply_comp {X Y : C} {a : ℤ}
    (f : ShiftedHom (Opposite.op X) (Opposite.op Y) a) {b : ℤ} {Z : C}
    (z : ShiftedHom X Z b) {c : ℤ} (h : b + a = c) :
    ((ShiftedHom.opEquiv a).symm f).comp z h =
      (ShiftedHom.opEquiv a).symm (z.op ≫ f) ≫
        (shiftFunctorAdd' C b a c h).inv.app Z

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ ((opEquiv a).symm f).comp z h = (opEquiv a).symm (Quiver.Hom.op z ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply,
  ShiftedHom.comp]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.op z ≫ f).unop) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
dsimp

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f ≫ z)) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasShift C ℤ
X Y : C
a : ℤ
f : ShiftedHom (Opposite.op X) (Opposite.op Y) a
b : ℤ
Z : C
z : ShiftedHom X Z b
c : ℤ
h : b + a = c
⊢ (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f)) ≫
      (shiftFunctor C a).map z ≫ (shiftFunctorAdd' C b a c h).inv.app Z =
    (((opShiftFunctorEquivalence C a).unitIso.inv.app (Opposite.op Y)).unop ≫
        (shiftFunctor C a).map (Quiver.Hom.unop f ≫ z)) ≫
      (shiftFunctorAdd' C b a c h).inv.app Z

Tactic:
simp only [assoc, Functor.map_comp]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem list_prod_left {l : List ℤ} {n : ℕ} : J(l.prod | n) = (l.map fun a => J(a | n)).prod

Proof state:
l : List ℤ
n : ℕ
⊢ J(l.prod | n) = (List.map (fun a => J(a | n)) l).prod

Tactic:
induction l with
| nil => simp only [List.prod_nil, List.map_nil, one_left]
| cons n l' ih => rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

Result:
no goals

Proof state:
case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a => J(a | n✝)) l').prod
⊢ J((n :: l').prod | n✝) = (List.map (fun a => J(a | n✝)) (n :: l')).prod

Tactic:
rw [List.map, List.prod_cons, List.prod_cons, mul_left, ih]

Result:
no goals

Proof state:
case nil
n : ℕ
⊢ J([].prod | n) = (List.map (fun a => J(a | n)) []).prod

Tactic:
simp only [List.prod_nil, List.map_nil, one_left]

Result:
no goals
-- Mathlib/Data/TypeVec.lean
theorem eq_nilFun {α β : TypeVec 0} (f : α ⟹ β) : f = nilFun

Proof state:
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
⊢ f = nilFun

Tactic:
ext x

Result:
case a.h
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝

Proof state:
case a.h
α : TypeVec.{u_1} 0
β : TypeVec.{u_2} 0
f : α ⟹ β
x : Fin2 0
x✝ : α x
⊢ f x x✝ = nilFun x x✝

Tactic:
cases x

Result:
no goals
-- Mathlib/Logic/Function/Iterate.lean
theorem iterate_comm (f : α → α) (m n : ℕ) : f^[n]^[m] = f^[m]^[n] :=
  (iterate_mul _ _ _).symm.trans (Eq.trans (by rw [Nat.mul_comm]) (iterate_mul _ _ _))

Proof state:
α : Type u
f : α → α
m n : ℕ
⊢ f^[n * m] = f^[m * n]

Tactic:
rw [Nat.mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
theorem FiberFunctor.isPretransitive_of_isGalois (X : C) [IsGalois X] :
    MulAction.IsPretransitive (Aut F) (F.obj X)

Proof state:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨a, ha⟩ := AutGalois.π_surjective F ⟨X, x, inferInstance⟩ φ

Result:
case intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ ∃ g, g • x = y

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
⊢ MulAction.IsPretransitive (Aut F) (F.obj X).carrier

Tactic:
refine ⟨fun x y ↦ ?_⟩

Result:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
⊢ ∃ g, g • x = y

Proof state:
case intro.intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ ∃ g, g • x = y

Tactic:
use (autMulEquivAutGalois F).symm ⟨a⟩

Result:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ (autMulEquivAutGalois F).symm { unop' := a } • x = y

Proof state:
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
⊢ ∃ g, g • x = y

Tactic:
obtain ⟨(φ : Aut X), h⟩ := MulAction.IsPretransitive.exists_smul_eq (M := Aut X) x y

Result:
case intro
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
⊢ ∃ g, g • x = y

Proof state:
case h
C : Type u₁
inst✝³ : Category.{u₂, u₁} C
inst✝² : GaloisCategory C
F : C ⥤ FintypeCat
inst✝¹ : FiberFunctor F
X : C
inst✝ : IsGalois X
x y : (F.obj X).carrier
φ : Aut X
h : φ • x = y
a : AutGalois F
ha : (AutGalois.π F { obj := X, pt := x, isGalois := ⋯ }) a = φ
⊢ (autMulEquivAutGalois F).symm { unop' := a } • x = y

Tactic:
simpa [mulAction_def, ha]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_top : expGrowthInf ⊤ = ⊤

Proof state:
⊢ expGrowthInf ⊤ = ⊤

Tactic:
nth_rw 2 [← liminf_const (f := atTop (α := ℕ)) ⊤]

Result:
⊢ expGrowthInf ⊤ = liminf (fun x => ⊤) atTop

Proof state:
⊢ expGrowthInf ⊤ = liminf (fun x => ⊤) atTop

Tactic:
apply liminf_congr

Result:
case h

⊢ ∀ᶠ (a : ℕ) in atTop, (⊤ a).log / ↑a = ⊤

Proof state:
case h

⊢ ∀ᶠ (a : ℕ) in atTop, (⊤ a).log / ↑a = ⊤

Tactic:
simp only [log_top, eventually_atTop]

Result:
case h

⊢ ∃ a, ∀ b ≥ a, (⊤ b).log / ↑b = ⊤

Proof state:
case h

⊢ ∃ a, ∀ b ≥ a, (⊤ b).log / ↑b = ⊤

Tactic:
exact ⟨1, fun n n_pos ↦ top_div_of_pos_ne_top (Nat.cast_pos'.2 n_pos) (natCast_ne_top n)⟩

Result:
no goals
-- Mathlib/Data/Nat/Bits.lean
@[simp]
lemma shiftLeft'_false : ∀ n, shiftLeft' false m n = m <<< n
  | 0 => rfl
  | n + 1 => by
    have : 2 * (m * 2^n) = 2^(n+1)*m

Proof state:
m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
have : 2 * (m * 2^n) = 2^(n+1)*m := by
  rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]; simp

Result:
m n : ℕ
this : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Proof state:
m n : ℕ
this : 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m
⊢ shiftLeft' false m (n + 1) = m <<< (n + 1)

Tactic:
simp [shiftLeft_eq, shiftLeft', bit_val, shiftLeft'_false, this]

Result:
no goals

Proof state:
m n : ℕ
⊢ 2 * (m * 2 ^ n) = 2 ^ (n + 1) * m

Tactic:
rw [Nat.mul_comm, Nat.mul_assoc, ← Nat.pow_succ]

Result:
m n : ℕ
⊢ m * 2 ^ n.succ = 2 ^ (n + 1) * m
-- Mathlib/Algebra/Homology/ExactSequence.lean
lemma Exact.exact' (hS : S.Exact) (i j k : ℕ) (hij : i + 1 = j

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
i j k : ℕ
hij : autoParam (i + 1 = j) _auto✝
hjk : autoParam (j + 1 = k) _auto✝
hk : autoParam (k ≤ n) _auto✝
⊢ (S.sc' ⋯ i j k ⋯ ⋯ ⋯).Exact

Tactic:
subst hij hjk

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
i : ℕ
hk : autoParam (i + 1 + 1 ≤ n) _auto✝
⊢ (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ ⋯).Exact

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
n : ℕ
S : ComposableArrows C n
hS : S.Exact
i : ℕ
hk : autoParam (i + 1 + 1 ≤ n) _auto✝
⊢ (S.sc' ⋯ i (i + 1) (i + 1 + 1) ⋯ ⋯ ⋯).Exact

Tactic:
exact hS.exact i hk

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_submatrix_equiv (A : Matrix m m α) (e : n ≃ m) (b : n → α) :
    cramer (A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e

Proof state:
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ (A.submatrix ⇑e ⇑e).cramer b i = (A.cramer (b ∘ ⇑e.symm) ∘ ⇑e) i

Tactic:
simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,
  det_submatrix_equiv_self e, Function.comp_def]

Result:
no goals

Proof state:
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
⊢ (A.submatrix ⇑e ⇑e).cramer b = A.cramer (b ∘ ⇑e.symm) ∘ ⇑e

Tactic:
ext i

Result:
case h
m : Type u
n : Type v
α : Type w
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : CommRing α
A : Matrix m m α
e : n ≃ m
b : n → α
i : n
⊢ (A.submatrix ⇑e ⇑e).cramer b i = (A.cramer (b ∘ ⇑e.symm) ∘ ⇑e) i
-- Mathlib/Algebra/Polynomial/Div.lean
lemma le_rootMultiplicity_mul {p q : R[X]} (x : R) (hpq : p * q ≠ 0) :
    rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ rootMultiplicity x p + rootMultiplicity x q ≤ rootMultiplicity x (p * q)

Tactic:
rw [le_rootMultiplicity_iff hpq, pow_add]

Result:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q

Proof state:
R : Type u
inst✝ : CommRing R
p q : R[X]
x : R
hpq : p * q ≠ 0
⊢ (X - C x) ^ rootMultiplicity x p * (X - C x) ^ rootMultiplicity x q ∣ p * q

Tactic:
exact mul_dvd_mul (pow_rootMultiplicity_dvd p x) (pow_rootMultiplicity_dvd q x)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem toFinsupp_apply (f : R[X]) (i) : f.toFinsupp i = f.coeff i

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
i : ℕ
⊢ f.toFinsupp i = f.coeff i

Tactic:
cases f

Result:
case ofFinsupp
R : Type u
inst✝ : Semiring R
i : ℕ
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.toFinsupp i = { toFinsupp := toFinsupp✝ }.coeff i

Proof state:
case ofFinsupp
R : Type u
inst✝ : Semiring R
i : ℕ
toFinsupp✝ : R[ℕ]
⊢ { toFinsupp := toFinsupp✝ }.toFinsupp i = { toFinsupp := toFinsupp✝ }.coeff i

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Category/LightProfinite/Basic.lean
theorem epi_iff_surjective {X Y : LightProfinite.{u}} (f : X ⟶ Y) :
    Epi f ↔ Function.Surjective f

Proof state:
case h.h.h.h
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X => ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x => { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ ↑((ConcreteCategory.hom (f ≫ h)) x).down = ↑((ConcreteCategory.hom (f ≫ g)) x).down

Tactic:
dsimp [g, LocallyConstant.ofIsClopen]

Result:
case h.h.h.h
X Y : LightProfinite
f : X ⟶ Y
y : ↑Y.toTop
hy : ∀ (a : ↑X.toTop), (ConcreteCategory.hom f) a ≠ y
hf : Epi f
C : Set ((fun X => ↑X.toTop) Y) := Set.range ⇑(ConcreteCategory.hom f)
hC : IsClosed C
U : Set ((fun X => ↑X.toTop) Y) := Cᶜ
hyU : y ∈ U
hUy : U ∈ 𝓝 y
V : Set ↑Y.toTop
hV : V ∈ {s | IsClopen s}
hyV : y ∈ V
hVU : V ⊆ U
Z : LightProfinite := of (ULift.{u, 0} (Fin 2))
g : Y ⟶ Z :=
  ofHom (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := ⇑(LocallyConstant.map ULift.up (LocallyConstant.ofIsClopen hV)), continuous_toFun := ⋯ }
h : Y ⟶ Z :=
  ofHom (fun X => TotallyDisconnectedSpace ↑X ∧ SecondCountableTopology ↑X)
    { toFun := fun x => { down := 1 }, continuous_toFun := ⋯ }
x : ↑X.toTop
⊢ ↑((ConcreteCategory.hom h) ((ConcreteCategory.hom f) x)).down =
    ↑({ toFun := ULift.up ∘ fun x => if x ∈ V then 0 else 1, continuous_toFun := ⋯ } ((ConcreteCategory.hom f) x)).down
-- Mathlib/Algebra/Module/CharacterModule.lean
lemma dual_injective_of_surjective (f : A →ₗ[R] B) (hf : Function.Surjective f) :
    Function.Injective (dual f)

Proof state:
case h
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
x : B
⊢ φ x = ψ x

Tactic:
obtain ⟨y, rfl⟩ := hf x

Result:
case h.intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ φ (f y) = ψ (f y)

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
⊢ φ = ψ

Tactic:
ext x

Result:
case h
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
x : B
⊢ φ x = ψ x

Proof state:
case h.intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ φ (f y) = ψ (f y)

Tactic:
change (dual f) φ _ = (dual f) ψ _

Result:
case h.intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) φ) y = ((dual f) ψ) y

Proof state:
case h.intro
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
y : A
⊢ ((dual f) φ) y = ((dual f) ψ) y

Tactic:
rw [eq]

Result:
no goals

Proof state:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
⊢ Function.Injective ⇑(dual f)

Tactic:
intro φ ψ eq

Result:
R : Type uR
inst✝⁴ : CommRing R
A : Type uA
inst✝³ : AddCommGroup A
B : Type uB
inst✝² : AddCommGroup B
inst✝¹ : Module R A
inst✝ : Module R B
f : A →ₗ[R] B
hf : Function.Surjective ⇑f
φ ψ : CharacterModule B
eq : (dual f) φ = (dual f) ψ
⊢ φ = ψ
-- Mathlib/Topology/LocalAtTarget.lean
theorem denseRange_iff_restrictPreimage :
    DenseRange f ↔ ∀ i, DenseRange ((U i).1.restrictPreimage f)

Proof state:
case e_a
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ univ = ⋃ i, {x | x ∈ U i}

Tactic:
exact hU.iSup_set_eq_univ.symm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure (range f) = univ ↔ ∀ (i : ι), Subtype.val ⁻¹' closure (range f) = univ

Tactic:
simp only [Opens.carrier_eq_coe, SetLike.coe_sort_coe, preimage_eq_univ_iff,
  Subtype.range_coe_subtype, SetLike.mem_coe]

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure (range f) = univ ↔ ∀ (i : ι), {x | x ∈ U i} ⊆ closure (range f)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure (range f) = univ ↔ ∀ (i : ι), {x | x ∈ U i} ⊆ closure (range f)

Tactic:
rw [← iUnion_subset_iff, ← Set.univ_subset_iff, iff_iff_eq]

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ (univ ⊆ closure (range f)) = (⋃ i, {x | x ∈ U i} ⊆ closure (range f))

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ (univ ⊆ closure (range f)) = (⋃ i, {x | x ∈ U i} ⊆ closure (range f))

Tactic:
congr 1

Result:
case e_a
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ univ = ⋃ i, {x | x ∈ U i}

Proof state:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ DenseRange f ↔ ∀ (i : ι), DenseRange ((U i).carrier.restrictPreimage f)

Tactic:
simp_rw [denseRange_iff_closure_range, Set.range_restrictPreimage,
  ← (U _).2.isOpenEmbedding_subtypeVal.isOpenMap.preimage_closure_eq_closure_preimage
    continuous_subtype_val]

Result:
α : Type u_1
β : Type u_2
inst✝ : TopologicalSpace β
f : α → β
ι : Type u_3
U : ι → Opens β
hU : IsOpenCover U
⊢ closure (range f) = univ ↔ ∀ (i : ι), Subtype.val ⁻¹' closure (range f) = univ
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem sum_map_tmul_counit_eq {B : Type*} [AddCommMonoid B] [Module R B]
    {F : Type*} [FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Repr R a} :
    ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ counit (R := R) (repr.right i) = f a ⊗ₜ[R] 1

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

Tactic:
have := sum_tmul_counit_eq repr

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a
this : ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a
this :
  (LinearMap.rTensor R ↑f) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i)) =
    (LinearMap.rTensor R ↑f) (a ⊗ₜ[R] 1)
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

Tactic:
simp_all only [map_sum, LinearMap.rTensor_tmul, LinearMap.coe_coe]

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a
this : ∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i) = a ⊗ₜ[R] 1
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1

Tactic:
apply_fun LinearMap.rTensor R (f : A →ₗ[R] B) at this

Result:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : AddCommMonoid A
inst✝⁵ : Module R A
inst✝⁴ : Coalgebra R A
B : Type u_1
inst✝³ : AddCommMonoid B
inst✝² : Module R B
F : Type u_2
inst✝¹ : FunLike F A B
inst✝ : LinearMapClass F R A B
f : F
a : A
repr : Repr R a
this :
  (LinearMap.rTensor R ↑f) (∑ i ∈ repr.index, repr.left i ⊗ₜ[R] counit (repr.right i)) =
    (LinearMap.rTensor R ↑f) (a ⊗ₜ[R] 1)
⊢ ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] counit (repr.right i) = f a ⊗ₜ[R] 1