harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem Multipliable.vanishing (hf : Multipliable f) ⦃e : Set G⦄ (he : e ∈ 𝓝 (1 : G)) :
    ∃ s : Finset α, ∀ t, Disjoint t s → (∏ k ∈ t, f k) ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
classical
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G
have : UniformGroup G := uniformGroup_of_commGroup
exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

Result:
no goals

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
have : UniformGroup G := uniformGroup_of_commGroup

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this✝ : UniformSpace G := IsTopologicalGroup.toUniformSpace G
this : UniformGroup G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
letI : UniformSpace G := IsTopologicalGroup.toUniformSpace G

Result:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this : UniformSpace G := IsTopologicalGroup.toUniformSpace G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Proof state:
α : Type u_1
G : Type u_4
inst✝² : TopologicalSpace G
inst✝¹ : CommGroup G
inst✝ : IsTopologicalGroup G
f : α → G
hf : Multipliable f
e : Set G
he : e ∈ 𝓝 1
this✝ : UniformSpace G := IsTopologicalGroup.toUniformSpace G
this : UniformGroup G
⊢ ∃ s, ∀ (t : Finset α), Disjoint t s → ∏ k ∈ t, f k ∈ e

Tactic:
exact cauchySeq_finset_iff_prod_vanishing.1 hf.hasProd.cauchySeq e he

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma le_iff_norm_sqrt_mul_sqrt_inv {a : A} {b : Aˣ} (ha : 0 ≤ a) (hb : 0 ≤ (b : A)) :
    a ≤ b ↔ ‖sqrt a * sqrt (↑b⁻¹ : A)‖ ≤ 1

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ 0 ∉ spectrum ℝ≥0 ↑b

Tactic:
simp

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ -1 ≠ 0

Tactic:
norm_num

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ a ≤ ↑b ↔ ‖sqrt a * sqrt ↑b⁻¹‖ ≤ 1

Tactic:
rw [CFC.sqrt_eq_rpow (a := (↑b⁻¹ : A)), ← CFC.rpow_neg_one_eq_inv b,
  CFC.rpow_rpow (b : A) _ _ (by simp) (by norm_num), le_iff_norm_sqrt_mul_rpow b.isUnit ha hb]

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
b : Aˣ
ha : 0 ≤ a
hb : 0 ≤ ↑b
⊢ ‖sqrt a * ↑b ^ (-(1 / 2))‖ ≤ 1 ↔ ‖sqrt a * ↑b ^ (-1 * (1 / 2))‖ ≤ 1
-- Mathlib/FieldTheory/Minpoly/MinpolyDiv.lean
lemma minpolyDiv_eval_eq_zero_of_ne_of_aeval_eq_zero [IsDomain S]
    {y} (hxy : y ≠ x) (hy : aeval y (minpoly R x) = 0) : (minpolyDiv R x).eval y = 0

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
⊢ eval y (minpolyDiv R x) = 0

Tactic:
exact hy.resolve_right (by rwa [sub_eq_zero])

Result:
no goals

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : (aeval y) (minpoly R x) = 0
⊢ eval y (minpolyDiv R x) = 0

Tactic:
rw [aeval_def, ← eval_map, ← minpolyDiv_spec R x] at hy

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x * (X - C x)) = 0
⊢ eval y (minpolyDiv R x) = 0

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x * (X - C x)) = 0
⊢ eval y (minpolyDiv R x) = 0

Tactic:
simp only [eval_mul, eval_sub, eval_X, eval_C, mul_eq_zero] at hy

Result:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
⊢ eval y (minpolyDiv R x) = 0

Proof state:
R : Type u_2
S : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Algebra R S
x : S
inst✝ : IsDomain S
y : S
hxy : y ≠ x
hy : eval y (minpolyDiv R x) = 0 ∨ y - x = 0
⊢ ¬y - x = 0

Tactic:
rwa [sub_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Pullback.lean
lemma pullbackShiftFunctorZero_inv_app :
    (shiftFunctorZero _ A).inv.app X =
      (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 (by simp)).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero (PullbackShift C φ) A).inv.app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Tactic:
change (shiftFunctorZero C B).inv.app X ≫ _ = _

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫
      ((shiftMonoidalFunctor C B).map (Functor.LaxMonoidal.ε (Discrete.addMonoidalFunctor φ))).app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Proof state:
case e_a.e_self
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftMonoidalFunctor C B).map (eqToHom ⋯) = (pullbackShiftIso C φ 0 0 ⋯).inv

Tactic:
apply eqToHom_map

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫
      ((shiftMonoidalFunctor C B).map (Functor.LaxMonoidal.ε (Discrete.addMonoidalFunctor φ))).app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Tactic:
dsimp [Discrete.eqToHom, Discrete.addMonoidalFunctor_ε]

Result:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ ((shiftMonoidalFunctor C B).map (eqToHom ⋯)).app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Proof state:
C : Type u_1
inst✝³ : Category.{?u.4389, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
a₁ a₂ a₃ : A
h : a₁ + a₂ = a₃
b₁ b₂ b₃ : B
h₁ : b₁ = φ a₁
h₂ : b₂ = φ a₂
h₃ : b₃ = φ a₃
⊢ 0 = φ 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftFunctorZero C B).inv.app X ≫ ((shiftMonoidalFunctor C B).map (eqToHom ⋯)).app X =
    (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 ⋯).inv.app X

Tactic:
congr 2

Result:
case e_a.e_self
C : Type u_1
inst✝³ : Category.{u_4, u_1} C
A : Type u_2
B : Type u_3
inst✝² : AddMonoid A
inst✝¹ : AddMonoid B
φ : A →+ B
inst✝ : HasShift C B
X : PullbackShift C φ
⊢ (shiftMonoidalFunctor C B).map (eqToHom ⋯) = (pullbackShiftIso C φ 0 0 ⋯).inv
-- Mathlib/Logic/Basic.lean
theorem dite_dite_comm {B : Q → α} {C : ¬P → ¬Q → α} (h : P → ¬Q) :
    (if p : P then A p else if q : Q then B q else C p q) =
     if q : Q then B q else if p : P then A p else C p q :=
  dite_eq_iff'.2 ⟨
    fun p ↦ by rw [dif_neg (h p), dif_pos p],
    fun np ↦ by congr; funext _; rw [dif_neg np]⟩

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (if q : Q then B q else C np q) = if q : Q then B q else if p : P then A p else C p q

Tactic:
congr

Result:
case e_e
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q

Proof state:
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
p : P
⊢ A p = if q : Q then B q else if p : P then A p else C p q

Tactic:
rw [dif_neg (h p), dif_pos p]

Result:
no goals

Proof state:
case e_e.h
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝

Tactic:
rw [dif_neg np]

Result:
no goals

Proof state:
case e_e
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
⊢ (fun q => C np q) = fun q => if p : P then A p else C p q

Tactic:
funext _

Result:
case e_e.h
α : Sort u_1
P Q : Prop
inst✝¹ : Decidable P
A : P → α
inst✝ : Decidable Q
B : Q → α
C : ¬P → ¬Q → α
h : P → ¬Q
np : ¬P
x✝ : ¬Q
⊢ C np x✝ = if p : P then A p else C p x✝
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
@[reassoc]
lemma cochainsMap_f_1_comp_oneCochainsLequiv :
    (cochainsMap f φ).f 1 ≫ (oneCochainsLequiv B).toModuleIso.hom =
      (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ)

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 1)
x✝ : G
⊢ (ModuleCat.Hom.hom
        ((ModuleCat.ofHom (LinearMap.funLeft k ↑A.V fun x => ⇑f ∘ x) ≫
            ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (Fin 1 → G))) ≫
          (oneCochainsLequiv B).toModuleIso.hom))
      x x✝ =
    (ModuleCat.Hom.hom ((oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ))) x x✝

Tactic:
rfl

Result:
no goals

Proof state:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 1)
x✝ : G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 1 ≫ (oneCochainsLequiv B).toModuleIso.hom)) x x✝ =
    (ModuleCat.Hom.hom ((oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ))) x x✝

Tactic:
simp only [cochainsMap_f, Unique.eq_default (f ∘ _)]

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 1)
x✝ : G
⊢ (ModuleCat.Hom.hom
        ((ModuleCat.ofHom (LinearMap.funLeft k ↑A.V fun x => ⇑f ∘ x) ≫
            ModuleCat.ofHom ((ModuleCat.Hom.hom φ.hom).compLeft (Fin 1 → G))) ≫
          (oneCochainsLequiv B).toModuleIso.hom))
      x x✝ =
    (ModuleCat.Hom.hom ((oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ))) x x✝

Proof state:
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
⊢ (cochainsMap f φ).f 1 ≫ (oneCochainsLequiv B).toModuleIso.hom =
    (oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ)

Tactic:
ext x

Result:
case hf.h.h
k G H : Type u
inst✝² : CommRing k
inst✝¹ : Group G
inst✝ : Group H
A : Rep k H
B : Rep k G
f : G →* H
φ : (Action.res (ModuleCat k) f).obj A ⟶ B
x : ↑((inhomogeneousCochains A).X 1)
x✝ : G
⊢ (ModuleCat.Hom.hom ((cochainsMap f φ).f 1 ≫ (oneCochainsLequiv B).toModuleIso.hom)) x x✝ =
    (ModuleCat.Hom.hom ((oneCochainsLequiv A).toModuleIso.hom ≫ ModuleCat.ofHom (fOne f φ))) x x✝
-- Mathlib/Topology/FiberBundle/Basic.lean
theorem open_source' (i : ι) : IsOpen (Z.localTrivAsPartialEquiv i).source

Proof state:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source =
    (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ

Tactic:
ext p

Result:
case a.h
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : Z.TotalSpace
⊢ p ∈ (Z.localTrivAsPartialEquiv i).source ↔
    p ∈ (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ

Proof state:
case a.h
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
p : Z.TotalSpace
⊢ p ∈ (Z.localTrivAsPartialEquiv i).source ↔
    p ∈ (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ

Tactic:
simp only [localTrivAsPartialEquiv_apply, prod_mk_mem_set_prod_eq, mem_inter_iff, and_self_iff,
  mem_localTrivAsPartialEquiv_source, and_true, mem_univ, mem_preimage]

Result:
no goals

Proof state:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source ∈
    ⋃ i, ⋃ s, ⋃ (_ : IsOpen s), {(Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s}

Tactic:
simp only [exists_prop, mem_iUnion, mem_singleton_iff]

Result:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ ↑(Z.localTrivAsPartialEquiv i_1) ⁻¹' i_2

Proof state:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ ∃ i_1 i_2,
    IsOpen i_2 ∧
      (Z.localTrivAsPartialEquiv i).source =
        (Z.localTrivAsPartialEquiv i_1).source ∩ ↑(Z.localTrivAsPartialEquiv i_1) ⁻¹' i_2

Tactic:
refine ⟨i, Z.baseSet i ×ˢ univ, (Z.isOpen_baseSet i).prod isOpen_univ, ?_⟩

Result:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source =
    (Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' Z.baseSet i ×ˢ univ

Proof state:
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ IsOpen (Z.localTrivAsPartialEquiv i).source

Tactic:
apply TopologicalSpace.GenerateOpen.basic

Result:
case a
ι : Type u_1
B : Type u_2
F : Type u_3
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
Z : FiberBundleCore ι B F
i : ι
⊢ (Z.localTrivAsPartialEquiv i).source ∈
    ⋃ i, ⋃ s, ⋃ (_ : IsOpen s), {(Z.localTrivAsPartialEquiv i).source ∩ ↑(Z.localTrivAsPartialEquiv i) ⁻¹' s}
-- Mathlib/RingTheory/Finiteness/Defs.lean
theorem fg_iff_add_subgroup_fg {G : Type*} [AddCommGroup G] (P : Submodule ℤ G) :
    P.FG ↔ P.toAddSubgroup.FG :=
  ⟨fun ⟨S, hS⟩ => ⟨S, by simpa [← span_int_eq_addSubgroup_closure] using hS⟩, fun ⟨S, hS⟩ =>
    ⟨S, by simpa [← span_int_eq_addSubgroup_closure] using hS⟩⟩

Proof state:
G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.toAddSubgroup.FG
S : Finset G
hS : AddSubgroup.closure ↑S = P.toAddSubgroup
⊢ span ℤ ↑S = P

Tactic:
simpa [← span_int_eq_addSubgroup_closure] using hS

Result:
no goals

Proof state:
G : Type u_3
inst✝ : AddCommGroup G
P : Submodule ℤ G
x✝ : P.FG
S : Finset G
hS : span ℤ ↑S = P
⊢ AddSubgroup.closure ↑S = P.toAddSubgroup

Tactic:
simpa [← span_int_eq_addSubgroup_closure] using hS

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem pseudoZero_iff {P : C} (a : Over P) : a = (0 : P) ↔ a.hom = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a.hom = 0

Tactic:
rw [← pseudoZero_aux P a]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P : C
a : Over P
⊢ Quot.mk (PseudoEqual P) a = 0 ↔ a ≈ Over.mk 0

Tactic:
exact Quotient.eq'

Result:
no goals
-- Mathlib/Data/Finsupp/Basic.lean
theorem equivMapDomain_single (f : α ≃ β) (a : α) (b : M) :
    equivMapDomain f (single a b) = single (f a) b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
ext x

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ (equivMapDomain f (single a b)) x = (single (f a) b) x

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
x : β
⊢ (equivMapDomain f (single a b)) x = (single (f a) b) x

Tactic:
simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : Zero M
f : α ≃ β
a : α
b : M
⊢ equivMapDomain f (single a b) = single (f a) b

Tactic:
classical
  ext x
  simp only [single_apply, Equiv.apply_eq_iff_eq_symm_apply, equivMapDomain_apply]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/UnionFind/Basic.lean
theorem parentD_set {arr : Array UFNode} {x v i h} :
    parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i

Proof state:
case isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : i < arr.size
⊢ (arr.set x v h)[i].parent = if x = i then v.parent else arr[i].parent

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < arr.size then (arr.set x v h)[i].parent else i) =
    if x = i then v.parent else if h : i < arr.size then arr[i].parent else i

Tactic:
split

Result:
case isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : i < arr.size
⊢ (arr.set x v h)[i].parent = if x = i then v.parent else arr[i].parent

case isFalse
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : ¬i < arr.size
⊢ i = if x = i then v.parent else i

Proof state:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
h : x < arr.size
h✝ : ¬x < arr.size
⊢ x = v.parent

Tactic:
cases ‹¬_› h

Result:
no goals

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < (arr.set x v h).size then (arr.set x v h)[i].parent else i) = if x = i then v.parent else parentD arr i

Tactic:
simp only [Array.size_set, Array.get_eq_getElem, parentD]

Result:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < arr.size then (arr.set x v h)[i].parent else i) =
    if x = i then v.parent else if h : i < arr.size then arr[i].parent else i

Proof state:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝¹ : ¬i < arr.size
h✝ : x = i
⊢ i = v.parent

Tactic:
subst i

Result:
case isFalse.isTrue
arr : Array UFNode
x : Nat
v : UFNode
h : x < arr.size
h✝ : ¬x < arr.size
⊢ x = v.parent

Proof state:
case isFalse
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
h✝ : ¬i < arr.size
⊢ i = if x = i then v.parent else i

Tactic:
split <;> [(subst i; cases ‹¬_› h); rfl]

Result:
no goals

Proof state:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ parentD (arr.set x v h) i = if x = i then v.parent else parentD arr i

Tactic:
rw [parentD]

Result:
arr : Array UFNode
x : Nat
v : UFNode
i : Nat
h : x < arr.size
⊢ (if h_1 : i < (arr.set x v h).size then (arr.set x v h)[i].parent else i) = if x = i then v.parent else parentD arr i
-- Mathlib/Algebra/Order/Group/CompleteLattice.lean
@[to_additive]
lemma ciInf_div (hf : BddBelow (range f)) (a : G) : (⨅ i, f i) / a = ⨅ i, f i / a

Proof state:
ι : Type u_1
G : Type u_2
inst✝³ : Group G
inst✝² : ConditionallyCompleteLattice G
inst✝¹ : Nonempty ι
f : ι → G
inst✝ : MulRightMono G
hf : BddBelow (range f)
a : G
⊢ (⨅ i, f i) / a = ⨅ i, f i / a

Tactic:
simp only [div_eq_mul_inv, ciInf_mul hf]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Multiset.lean
theorem extract_gcd' (s t : Multiset α) (hs : ∃ x, x ∈ s ∧ x ≠ (0 : α))
    (ht : s = t.map (s.gcd * ·)) : t.gcd = 1 :=
  ((@mul_right_eq_self₀ _ _ s.gcd _).1 <| by
        conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]).resolve_right <| by
    contrapose! hs
    exact s.gcd_eq_zero_iff.1 hs

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map (fun x => s.gcd * x) t
hs : s.gcd = 0
⊢ ∀ x ∈ s, x = 0

Tactic:
exact s.gcd_eq_zero_iff.1 hs

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x ∈ s, x ≠ 0
ht : s = map (fun x => s.gcd * x) t
⊢ s.gcd * t.gcd = s.gcd

Tactic:
conv_lhs => rw [← normalize_gcd, ← gcd_map_mul, ← ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
hs : ∃ x ∈ s, x ≠ 0
ht : s = map (fun x => s.gcd * x) t
⊢ ¬s.gcd = 0

Tactic:
contrapose! hs

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s t : Multiset α
ht : s = map (fun x => s.gcd * x) t
hs : s.gcd = 0
⊢ ∀ x ∈ s, x = 0
-- Mathlib/Data/ENNReal/Inv.lean
theorem coe_div (hr : r ≠ 0) : (↑(p / r) : ℝ≥0∞) = p / r

Proof state:
r p : ℝ≥0
hr : r ≠ 0
⊢ ↑(p / r) = ↑p / ↑r

Tactic:
rw [div_eq_mul_inv, div_eq_mul_inv, coe_mul, coe_inv hr]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem aeval_esymm_eq_multiset_esymm [Algebra R S] (n : ℕ) (f : σ → S) :
    aeval f (esymm σ R n) = (univ.val.map f).esymm n

Proof state:
S : Type u_4
σ : Type u_5
R : Type u_6
inst✝³ : CommSemiring R
inst✝² : CommSemiring S
inst✝¹ : Fintype σ
inst✝ : Algebra R S
n : ℕ
f : σ → S
⊢ (aeval f) (esymm σ R n) = (Multiset.map f univ.val).esymm n

Tactic:
simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem map_pmap {p : α → Prop} (g : β → γ) (f : ∀ a, p a → β) (l : Vector α n) (H) :
    map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ map g (pmap f { toArray := l, size_toArray := ⋯ } H) =
    pmap (fun a h => g (f a h)) { toArray := l, size_toArray := ⋯ } H

Tactic:
simp [Array.map_pmap]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
n : Nat
p : α → Prop
g : β → γ
f : (a : α) → p a → β
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
⊢ map g (pmap f l H) = pmap (fun a h => g (f a h)) l H

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
p : α → Prop
g : β → γ
f : (a : α) → p a → β
l : Array α
H : ∀ (a : α), a ∈ { toArray := l, size_toArray := ⋯ } → p a
⊢ map g (pmap f { toArray := l, size_toArray := ⋯ } H) =
    pmap (fun a h => g (f a h)) { toArray := l, size_toArray := ⋯ } H