harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/MvPowerSeries/PiTopology.lean
theorem variables_tendsto_zero [Semiring R] :
    Tendsto (X · : σ → MvPowerSeries σ R) cofinite (nhds 0)

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
by_cases h : ∃ i, d = Finsupp.single i 1

Result:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i => if d = Finsupp.single i 1 then 1 else 0) cofinite (nhds 0)

Tactic:
refine fun d ↦ tendsto_nhds_of_eventually_eq ?_

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Proof state:
case neg
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ¬∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
simpa only [ite_eq_right_iff] using
  Eventually.of_forall fun x h' ↦ (not_exists.mp h x h').elim

Result:
no goals

Proof state:
case h
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
j : σ
hj : j ≠ i
⊢ (if d = Finsupp.single j 1 then 1 else 0) = 0

Tactic:
simp [hi, Finsupp.single_eq_single_iff, hj.symm]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ Tendsto (fun x => X x) cofinite (nhds 0)

Tactic:
simp only [tendsto_iff_coeff_tendsto, ← coeff_apply, coeff_X, coeff_zero]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
⊢ ∀ (d : σ →₀ ℕ), Tendsto (fun i => if d = Finsupp.single i 1 then 1 else 0) cofinite (nhds 0)

Proof state:
case pos.intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
filter_upwards [eventually_cofinite_ne i] with j hj

Result:
case h
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
j : σ
hj : j ≠ i
⊢ (if d = Finsupp.single j 1 then 1 else 0) = 0

Proof state:
case pos
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
h : ∃ i, d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0

Tactic:
obtain ⟨i, hi⟩ := h

Result:
case pos.intro
σ : Type u_1
R : Type u_2
inst✝¹ : TopologicalSpace R
inst✝ : Semiring R
d : σ →₀ ℕ
i : σ
hi : d = Finsupp.single i 1
⊢ ∀ᶠ (x' : σ) in cofinite, (if d = Finsupp.single x' 1 then 1 else 0) = 0
-- Mathlib/Combinatorics/Additive/ApproximateSubgroup.lean
@[to_additive]
lemma pow_inter_pow (hA : IsApproximateSubgroup K A) (hB : IsApproximateSubgroup L B) (hm : 2 ≤ m)
    (hn : 2 ≤ n) :
    IsApproximateSubgroup (K ^ (2 * m - 1) * L ^ (2 * n - 1)) (A ^ m ∩ B ^ n) where
  one_mem := ⟨Set.one_mem_pow hA.one_mem, Set.one_mem_pow hB.one_mem⟩
  inv_eq_self

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 2 ≤ 2 * m

Tactic:
omega

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m ∩ B ^ n) ^ 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)

Tactic:
calc
  (A ^ m ∩ B ^ n) ^ 2 ⊆ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 := Set.inter_pow_subset
  _ = A ^ (2 * m) ∩ B ^ (2 * n) := by simp [pow_mul']

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m ∩ B ^ n)⁻¹ = A ^ m ∩ B ^ n

Tactic:
simp_rw [inter_inv, ← inv_pow, hA.inv_eq_self, hB.inv_eq_self]

Result:
no goals

Proof state:
case h₁.hs
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 1 ∈ A

case h₂.hs
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 1 ∈ B

Tactic:
exacts [hA.one_mem, hB.one_mem]

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 2 ≤ 2 * n

Tactic:
omega

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ CovBySMul G (K ^ (2 * m - 1) * L ^ (2 * n - 1)) ((A ^ m ∩ B ^ n) ^ 2) (A ^ m ∩ B ^ n)

Tactic:
refine (hA.pow_inter_pow_covBySMul_sq_inter_sq hB (by omega) (by omega)).subset ?_
  (by gcongr; exacts [hA.one_mem, hB.one_mem])

Result:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m ∩ B ^ n) ^ 2 ⊆ A ^ (2 * m) ∩ B ^ (2 * n)

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ A ^ 2 ∩ B ^ 2 ⊆ A ^ m ∩ B ^ n

Tactic:
gcongr

Result:
case h₁.hs
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 1 ∈ A

case h₂.hs
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ 1 ∈ B

Proof state:
G : Type u_1
inst✝ : Group G
A B : Set G
K L : ℝ
m n : ℕ
hA : IsApproximateSubgroup K A
hB : IsApproximateSubgroup L B
hm : 2 ≤ m
hn : 2 ≤ n
⊢ (A ^ m) ^ 2 ∩ (B ^ n) ^ 2 = A ^ (2 * m) ∩ B ^ (2 * n)

Tactic:
simp [pow_mul']

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem isNoetherianRing : IsNoetherianRing A

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsNoetherianRing A

Tactic:
refine isNoetherianRing_iff.mpr ⟨fun I : Ideal A => ?_⟩

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
⊢ Submodule.FG I

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG I

Tactic:
rw [hI]

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG ⊥

Proof state:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG ⊥

Tactic:
apply Submodule.fg_bot

Result:
no goals

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : ¬I = ⊥
⊢ Submodule.FG I

Tactic:
have hI : (I : FractionalIdeal A⁰ (FractionRing A)) ≠ 0 := coeIdeal_ne_zero.mpr hI

Result:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI✝ : ¬I = ⊥
hI : ↑I ≠ 0
⊢ Submodule.FG I

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
⊢ Submodule.FG I

Tactic:
by_cases hI : I = ⊥

Result:
case pos
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : I = ⊥
⊢ Submodule.FG I

case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI : ¬I = ⊥
⊢ Submodule.FG I

Proof state:
case neg
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
I : Ideal A
hI✝ : ¬I = ⊥
hI : ↑I ≠ 0
⊢ Submodule.FG I

Tactic:
exact I.fg_of_isUnit (IsFractionRing.injective A (FractionRing A)) (h.isUnit hI)

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/UniformConvergence.lean
lemma summand_bound_of_mem_verticalStrip {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 → ℤ)
    {A B : ℝ} (hB : 0 < B) (hz : z ∈ verticalStrip A B) :
    ‖x 0 * (z : ℂ) + x 1‖ ^ (-k) ≤ r ⟨⟨A, B⟩, hB⟩ ^ (-k) * ‖x‖ ^ (-k)

Proof state:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ 0 ≤ ‖x‖ ^ (-k)

Tactic:
positivity

Result:
no goals

Proof state:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ ‖↑(x 0) * ↑z + ↑(x 1)‖ ^ (-k) ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-k) * ‖x‖ ^ (-k)

Tactic:
refine (summand_bound z hk x).trans (mul_le_mul_of_nonneg_right ?_ (by positivity))

Result:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ r z ^ (-k) ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-k)

Proof state:
z : ℍ
k : ℝ
hk : 0 ≤ k
x : Fin 2 → ℤ
A B : ℝ
hB : 0 < B
hz : z ∈ verticalStrip A B
⊢ r z ^ (-k) ≤ r ⟨{ re := A, im := B }, hB⟩ ^ (-k)

Tactic:
exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
  (neg_nonpos.mpr hk)

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosed_iff {s : Set (CofiniteTopology X)} : IsClosed s ↔ s = univ ∨ s.Finite

Proof state:
X : Type u
s : Set (CofiniteTopology X)
⊢ IsClosed s ↔ s = univ ∨ s.Finite

Tactic:
simp only [← isOpen_compl_iff, isOpen_iff', compl_compl, compl_empty_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Defs.lean
theorem inclusion_self (x : H) : inclusion le_rfl x = x

Proof state:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion ⋯) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
x : ↥H
⊢ (inclusion ⋯) x = x

Tactic:
cases x

Result:
case mk
G : Type u_1
inst✝² : Group G
S : Type u_4
H : S
inst✝¹ : SetLike S G
inst✝ : SubgroupClass S G
val✝ : G
property✝ : val✝ ∈ H
⊢ (inclusion ⋯) ⟨val✝, property✝⟩ = ⟨val✝, property✝⟩
-- Mathlib/Algebra/Order/Disjointed.lean
theorem disjointed_add_one [NoMaxOrder ι] (f : ι → α) (i : ι) :
    disjointed f (i + 1) = f (i + 1) \ partialSups f i

Proof state:
α : Type u_1
ι : Type u_2
inst✝⁶ : GeneralizedBooleanAlgebra α
inst✝⁵ : LinearOrder ι
inst✝⁴ : LocallyFiniteOrderBot ι
inst✝³ : Add ι
inst✝² : One ι
inst✝¹ : SuccAddOrder ι
inst✝ : NoMaxOrder ι
f : ι → α
i : ι
⊢ disjointed f (i + 1) = f (i + 1) \ (partialSups f) i

Tactic:
simpa only [succ_eq_add_one] using disjointed_succ f (not_isMax i)

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions/ComposableArrows.lean
lemma essSurj_mapComposableArrows [W.HasLeftCalculusOfFractions] (n : ℕ) :
    (L.mapComposableArrows n).EssSurj

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
n : ℕ
this : (L.op.mapComposableArrows n).EssSurj
⊢ (L.mapComposableArrows n).EssSurj

Tactic:
have := Functor.essSurj_of_iso (L.mapComposableArrowsOpIso n).symm

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
n : ℕ
this✝ : (L.op.mapComposableArrows n).EssSurj
this : (L.mapComposableArrows n ⋙ (opEquivalence D n).functor.rightOp).EssSurj
⊢ (L.mapComposableArrows n).EssSurj

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
n : ℕ
this✝ : (L.op.mapComposableArrows n).EssSurj
this : (L.mapComposableArrows n ⋙ (opEquivalence D n).functor.rightOp).EssSurj
⊢ (L.mapComposableArrows n).EssSurj

Tactic:
exact Functor.essSurj_of_comp_fully_faithful _ (opEquivalence D n).functor.rightOp

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
n : ℕ
⊢ (L.mapComposableArrows n).EssSurj

Tactic:
have := essSurj_mapComposableArrows_of_hasRightCalculusOfFractions L.op W.op n

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_3, u_1} C
inst✝² : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : W.HasLeftCalculusOfFractions
n : ℕ
this : (L.op.mapComposableArrows n).EssSurj
⊢ (L.mapComposableArrows n).EssSurj
-- Mathlib/RingTheory/Coalgebra/Basic.lean
theorem sum_counit_tmul_map_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, counit (R := R) (repr.left i) ⊗ₜ f (repr.right i) = 1 ⊗ₜ[R] f a

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.lTensor R ↑f) (∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i) =
    (LinearMap.lTensor R ↑f) (1 ⊗ₜ[R] a)
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

Tactic:
simp_all only [map_sum, LinearMap.lTensor_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, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

Tactic:
apply_fun LinearMap.lTensor 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.lTensor R ↑f) (∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i) =
    (LinearMap.lTensor R ↑f) (1 ⊗ₜ[R] a)
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

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, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a

Tactic:
have := sum_counit_tmul_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, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] f (repr.right i) = 1 ⊗ₜ[R] f a
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem Ici_eq_finset_subtype : Ici a = (Icc (a : ℕ) n).fin n

Proof state:
case h
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ Ici a ↔ a✝ ∈ Finset.fin n (Icc (↑a) n)

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
a : Fin n
⊢ Ici a = Finset.fin n (Icc (↑a) n)

Tactic:
ext

Result:
case h
n : ℕ
a a✝ : Fin n
⊢ a✝ ∈ Ici a ↔ a✝ ∈ Finset.fin n (Icc (↑a) n)
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem eq_sign_of_surjective_hom {s : Perm α →* ℤˣ} (hs : Surjective s) : s = sign :=
  have : ∀ {f}, IsSwap f → s f = -1 := fun {f} ⟨x, y, hxy, hxy'⟩ =>
    hxy'.symm ▸
      by_contradiction fun h => by
        have : ∀ f, IsSwap f → s f = 1 := fun f ⟨a, b, hab, hab'⟩ => by
          rw [← isConj_iff_eq, ← Or.resolve_right (Int.units_eq_one_or _) h, hab']
          exact s.map_isConj (isConj_swap hab hxy)
        let ⟨g, hg⟩ := hs (-1)
        let ⟨l, hl⟩ := (truncSwapFactors g).out
        have : ∀ a ∈ l.map s, a = (1 : ℤˣ) := fun a ha =>
          let ⟨g, hg⟩ := List.mem_map.1 ha
          hg.2 ▸ this _ (hl.2 _ hg.1)
        have : s l.prod = 1

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this✝ : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
this : ∀ a ∈ List.map (⇑s) l, a = 1
⊢ s l.prod = 1

Tactic:
rw [← l.prod_hom s, List.eq_replicate_length.2 this, List.prod_replicate, one_pow]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
⊢ False

Tactic:
let ⟨l, hl⟩ := (truncSwapFactors g).out

Result:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Perm α →* ℤˣ
hs : Surjective ⇑s
f : Perm α
x✝ : f.IsSwap
x y : α
hxy : x ≠ y
hxy' : f = swap x y
h : ¬s (swap x y) = -1
this : ∀ (f : Perm α), f.IsSwap → s f = 1
g : Perm α
hg : s g = -1
l : List (Perm α)
hl : l.prod = g ∧ ∀ g ∈ l, g.IsSwap
⊢ False
-- Mathlib/Combinatorics/Additive/Corner/Roth.lean
private lemma farFromTriangleFree_graph [Fintype G] [DecidableEq G] (hε : ε * card G ^ 2 ≤ #A) :
    (graph <| triangleIndices A).FarFromTriangleFree (ε / 9)

Proof state:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ (graph (Corners.triangleIndices A)).FarFromTriangleFree (ε / 9)

Tactic:
refine farFromTriangleFree _ ?_

Result:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(#(Corners.triangleIndices A))

Proof state:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)

Tactic:
simpa only [mul_comm] using hε

Result:
no goals

Proof state:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε / 9 * ↑((Fintype.card G + Fintype.card G + Fintype.card G) ^ 2) ≤ ↑(#(Corners.triangleIndices A))

Tactic:
simp_rw [card_triangleIndices, mul_comm_div, Nat.cast_pow, Nat.cast_add]

Result:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ((↑(Fintype.card G) + ↑(Fintype.card G) + ↑(Fintype.card G)) ^ 2 / 9) ≤ ↑(#A)

Proof state:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ((↑(Fintype.card G) + ↑(Fintype.card G) + ↑(Fintype.card G)) ^ 2 / 9) ≤ ↑(#A)

Tactic:
ring_nf

Result:
G : Type u_1
inst✝² : AddCommGroup G
A : Finset (G × G)
ε : ℝ
inst✝¹ : Fintype G
inst✝ : DecidableEq G
hε : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
⊢ ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#A)
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem exists_mem_normalizedFactors_of_dvd {a p : α} (ha0 : a ≠ 0) (hp : Irreducible p) :
    p ∣ a → ∃ q ∈ normalizedFactors a, p ~ᵤ q := fun ⟨b, hb⟩ =>
  have hb0 : b ≠ 0 := fun hb0 => by simp_all
  have : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a) :=
    factors_unique
      (fun _ hx =>
        (Multiset.mem_cons.1 hx).elim (fun h => h.symm ▸ hp) (irreducible_of_normalized_factor _))
      irreducible_of_normalized_factor
      (Associated.symm <|
        calc
          Multiset.prod (normalizedFactors a) ~ᵤ a := prod_normalizedFactors ha0
          _ = p * b := hb
          _ ~ᵤ Multiset.prod (p ::ₘ normalizedFactors b)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b = 0
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
this : Multiset.Rel Associated (p ::ₘ normalizedFactors b) (normalizedFactors a)
⊢ p ∈ p ::ₘ normalizedFactors b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod

Tactic:
exact (prod_normalizedFactors hb0).symm.mul_left _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ (p ::ₘ normalizedFactors b).prod

Tactic:
rw [Multiset.prod_cons]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
ha0 : a ≠ 0
hp : Irreducible p
x✝ : p ∣ a
b : α
hb : a = p * b
hb0 : b ≠ 0
⊢ p * b ~ᵤ p * (normalizedFactors b).prod
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem not_mem_uIcc_of_lt : c < a → c < b → c ∉ [[a, b]]

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → c ∉ [[a, b]]

Tactic:
rw [mem_uIcc]

Result:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → ¬(a ⊓ b ≤ c ∧ c ≤ a ⊔ b)

Tactic:
exact Set.not_mem_uIcc_of_lt

Result:
no goals
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Iio : (Iio b).map Fin.valEmbedding = Iio ↑b

Proof state:
n : ℕ
b : Fin n
⊢ map valEmbedding (Iio b) = Iio ↑b

Tactic:
simp [Iio_eq_finset_subtype, Finset.fin, Finset.map_map]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_ofSubsingleton_id_le [Subsingleton ι] (i : ι) :
    ‖ofSubsingleton 𝕜 G G i (.id _ _)‖ ≤ 1

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
⊢ ‖ContinuousLinearMap.id 𝕜 G‖ ≤ 1

Tactic:
apply ContinuousLinearMap.norm_id_le

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
⊢ ‖(ofSubsingleton 𝕜 G G i) (ContinuousLinearMap.id 𝕜 G)‖ ≤ 1

Tactic:
rw [norm_ofSubsingleton]

Result:
𝕜 : Type u
ι : Type v
G : Type wG
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : SeminormedAddCommGroup G
inst✝² : NormedSpace 𝕜 G
inst✝¹ : Fintype ι
inst✝ : Subsingleton ι
i : ι
⊢ ‖ContinuousLinearMap.id 𝕜 G‖ ≤ 1