harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/HahnSeries/Multiplication.lean
theorem orderTop_nsmul_le_orderTop_pow {Γ} [LinearOrderedCancelAddCommMonoid Γ]
    [Semiring R] {x : HahnSeries Γ R} {n : ℕ} : n • x.orderTop ≤ (x ^ n).orderTop

Proof state:
case succ
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop

Tactic:
calc
  n • x.orderTop + 1 • x.orderTop ≤ (x ^ n).orderTop + 1 • x.orderTop :=
    add_le_add_right ih (1 • x.orderTop)
  (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop := by rw [one_nsmul]
  (x ^ n).orderTop + x.orderTop ≤ (x ^ n * x).orderTop := orderTop_add_le_mul
  (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop := by rw [pow_one]

Result:
no goals

Proof state:
case zero
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
⊢ 0 ≤ orderTop 1

Tactic:
by_cases h : (0 : R) = 1

Result:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
h : 0 = 1
⊢ 0 ≤ orderTop 1

case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
h : ¬0 = 1
⊢ 0 ≤ orderTop 1

Proof state:
case neg
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
h : ¬0 = 1
⊢ 0 ≤ orderTop 1

Tactic:
simp [nontrivial_of_ne 0 1 h]

Result:
no goals

Proof state:
case pos
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
h : 0 = 1
⊢ 0 ≤ orderTop 1

Tactic:
simp [subsingleton_iff_zero_eq_one.mp h]

Result:
no goals

Proof state:
case zero
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
⊢ 0 • x.orderTop ≤ (x ^ 0).orderTop

Tactic:
simp only [zero_smul, pow_zero]

Result:
case zero
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
⊢ 0 ≤ orderTop 1

Proof state:
case succ
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (n + 1) • x.orderTop ≤ (x ^ (n + 1)).orderTop

Tactic:
rw [add_nsmul, pow_add]

Result:
case succ
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ n • x.orderTop + 1 • x.orderTop ≤ (x ^ n * x ^ 1).orderTop

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n * x).orderTop ≤ (x ^ n * x ^ 1).orderTop

Tactic:
rw [pow_one]

Result:
no goals

Proof state:
R : Type u_3
Γ : Type u_6
inst✝¹ : LinearOrderedCancelAddCommMonoid Γ
inst✝ : Semiring R
x : HahnSeries Γ R
n : ℕ
ih : n • x.orderTop ≤ (x ^ n).orderTop
⊢ (x ^ n).orderTop + 1 • x.orderTop = (x ^ n).orderTop + x.orderTop

Tactic:
rw [one_nsmul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter
    (h : AEStronglyMeasurable f μ) : StronglyMeasurableAtFilter f l μ :=
  ⟨univ, univ_mem, by rwa [Measure.restrict_univ]⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : TopologicalSpace β
l : Filter α
f : α → β
μ : Measure α
h : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable f (μ.restrict univ)

Tactic:
rwa [Measure.restrict_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_le_integral (hf : Integrable f μ) : ∃ x, f x ≤ ∫ a, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
inst✝ : IsProbabilityMeasure μ
hf : Integrable f μ
⊢ ∃ x, f x ≤ ∫ (a : α), f a ∂μ

Tactic:
simpa only [average_eq_integral] using exists_le_average (IsProbabilityMeasure.ne_zero μ) hf

Result:
no goals
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem rel_eq {s t : Multiset α} : Rel (· = ·) s t ↔ s = t

Proof state:
case mpr
α : Type u_1
s : Multiset α
⊢ Rel (fun x1 x2 => x1 = x2) s s

Tactic:
exact rel_eq_refl

Result:
no goals

Proof state:
case mpr
α : Type u_1
s t : Multiset α
h : s = t
⊢ Rel (fun x1 x2 => x1 = x2) s t

Tactic:
subst h

Result:
case mpr
α : Type u_1
s : Multiset α
⊢ Rel (fun x1 x2 => x1 = x2) s s

Proof state:
case mp
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 => x1 = x2) s t → s = t

Tactic:
intro h

Result:
case mp
α : Type u_1
s t : Multiset α
h : Rel (fun x1 x2 => x1 = x2) s t
⊢ s = t

Proof state:
case mp
α : Type u_1
s t : Multiset α
h : Rel (fun x1 x2 => x1 = x2) s t
⊢ s = t

Tactic:
induction h <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 => x1 = x2) s t ↔ s = t

Tactic:
constructor

Result:
case mp
α : Type u_1
s t : Multiset α
⊢ Rel (fun x1 x2 => x1 = x2) s t → s = t

case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 => x1 = x2) s t

Proof state:
case mpr
α : Type u_1
s t : Multiset α
⊢ s = t → Rel (fun x1 x2 => x1 = x2) s t

Tactic:
intro h

Result:
case mpr
α : Type u_1
s t : Multiset α
h : s = t
⊢ Rel (fun x1 x2 => x1 = x2) s t
-- Mathlib/AlgebraicTopology/FundamentalGroupoid/SimplyConnected.lean
theorem simply_connected_iff_paths_homotopic {Y : Type*} [TopologicalSpace Y] :
    SimplyConnectedSpace Y ↔
      PathConnectedSpace Y ∧ ∀ x y : Y, Subsingleton (Path.Homotopic.Quotient x y) :=
  ⟨by intro; constructor <;> infer_instance, fun h => by
    cases h; rw [simply_connected_iff_unique_homotopic]
    exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩⟩

Proof state:
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
constructor <;> infer_instance

Result:
no goals

Proof state:
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
rw [simply_connected_iff_unique_homotopic]

Result:
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))

Proof state:
Y : Type u_1
inst✝ : TopologicalSpace Y
⊢ SimplyConnectedSpace Y → PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Tactic:
intro

Result:
Y : Type u_1
inst✝ : TopologicalSpace Y
a✝ : SimplyConnectedSpace Y
⊢ PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)

Proof state:
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ Nonempty Y ∧ ∀ (x y : Y), Nonempty (Unique (Path.Homotopic.Quotient x y))

Tactic:
exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩

Result:
no goals

Proof state:
Y : Type u_1
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
cases h

Result:
case intro
Y : Type u_1
inst✝ : TopologicalSpace Y
left✝ : PathConnectedSpace Y
right✝ : ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/Cospan.lean
theorem cospanExt_app_left : (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
f : X ⟶ Z
g : Y ⟶ Z
f' : X' ⟶ Z'
g' : Y' ⟶ Z'
wf : iX.hom ≫ f' = f ≫ iZ.hom
wg : iY.hom ≫ g' = g ≫ iZ.hom
⊢ (cospanExt iX iY iZ wf wg).app WalkingCospan.left = iX

Tactic:
dsimp [cospanExt]

Result:
no goals
-- Mathlib/RingTheory/RingHom/StandardSmooth.lean
lemma IsStandardSmoothOfRelativeDimension.comp {g : S →+* T} {f : R →+* S}
    (hg : IsStandardSmoothOfRelativeDimension.{t', w'} n g)
    (hf : IsStandardSmoothOfRelativeDimension.{t, w} m f) :
    IsStandardSmoothOfRelativeDimension.{max t t', max w w'} (n + m) (g.comp f)

Proof state:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmoothOfRelativeDimension n S T
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension m R S
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
exact Algebra.IsStandardSmoothOfRelativeDimension.trans m n R S T

Result:
no goals

Proof state:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Tactic:
algebraize [f, g, (g.comp f)]

Result:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
algInst✝² : Algebra R S := f.toAlgebra
algInst✝¹ : Algebra S T := g.toAlgebra
algInst✝ : Algebra R T := (g.comp f).toAlgebra
scalarTowerInst✝ : IsScalarTower R S T := IsScalarTower.of_algebraMap_eq' (Eq.refl (algebraMap R T))
algebraizeInst✝¹ : Algebra.IsStandardSmoothOfRelativeDimension n S T
algebraizeInst✝ : Algebra.IsStandardSmoothOfRelativeDimension m R S
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T

Proof state:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ IsStandardSmoothOfRelativeDimension (n + m) (g.comp f)

Tactic:
rw [IsStandardSmoothOfRelativeDimension]

Result:
n m : ℕ
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
T : Type u_1
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : IsStandardSmoothOfRelativeDimension n g
hf : IsStandardSmoothOfRelativeDimension m f
⊢ Algebra.IsStandardSmoothOfRelativeDimension (n + m) R T
-- Mathlib/NumberTheory/FermatPsp.lean
theorem coprime_of_probablePrime {n b : ℕ} (h : ProbablePrime n b) (h₁ : 1 ≤ n) (h₂ : 1 ≤ b) :
    Nat.Coprime n b

Proof state:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0

Tactic:
omega

Result:
no goals

Proof state:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ False

Tactic:
apply Nat.Prime.not_dvd_one hk

Result:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ k ∣ 1

Proof state:
case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b

Tactic:
rw [show n = 1 by omega]

Result:
case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b

Proof state:
case pos.H
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b

Tactic:
rintro k hk ⟨m, rfl⟩ ⟨j, rfl⟩

Result:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ False

Proof state:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : (k * m).ProbablePrime (k * j)
⊢ k ∣ 1

Tactic:
replace h := dvd_of_mul_right_dvd h

Result:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1

Proof state:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)

Tactic:
refine dvd_of_mul_right_dvd (dvd_pow_self (k * j) ?_)

Result:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k * m - 1 ≠ 0

Proof state:
case pos
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ n.Coprime b

Tactic:
apply Nat.coprime_of_dvd

Result:
case pos.H
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ ∀ (k : ℕ), Prime k → k ∣ n → ¬k ∣ b

Proof state:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n = 1

Tactic:
omega

Result:
no goals

Proof state:
case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ Coprime 1 b

Tactic:
norm_num

Result:
no goals

Proof state:
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
⊢ n.Coprime b

Tactic:
by_cases h₃ : 2 ≤ n

Result:
case pos
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : 2 ≤ n
⊢ n.Coprime b

case neg
n b : ℕ
h : n.ProbablePrime b
h₁ : 1 ≤ n
h₂ : 1 ≤ b
h₃ : ¬2 ≤ n
⊢ n.Coprime b

Proof state:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ 1

Tactic:
rw [Nat.dvd_add_iff_right h, Nat.sub_add_cancel (Nat.one_le_pow _ _ h₂)]

Result:
case pos.H.intro.intro
k : ℕ
hk : Prime k
m : ℕ
h₁ : 1 ≤ k * m
h₃ : 2 ≤ k * m
j : ℕ
h₂ : 1 ≤ k * j
h : k ∣ (k * j) ^ (k * m - 1) - 1
⊢ k ∣ (k * j) ^ (k * m - 1)
-- Mathlib/Data/Finsupp/Single.lean
theorem erase_single {a : α} {b : M} : erase a (single a b) = 0

Proof state:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
⊢ (erase a (single a b)) s = 0 s

Tactic:
by_cases hs : s = a

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ (erase a (single a b)) s = 0 s

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ (erase a (single a b)) s = 0 s

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ (erase a (single a b)) s = 0 s

Tactic:
rw [erase_ne hs]

Result:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ (single a b) s = 0 s

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
⊢ erase a (single a b) = 0

Tactic:
ext s

Result:
case h
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
⊢ (erase a (single a b)) s = 0 s

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : s = a
⊢ (erase a (single a b)) s = 0 s

Tactic:
rw [hs, erase_same, coe_zero, Pi.zero_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
a : α
b : M
s : α
hs : ¬s = a
⊢ (single a b) s = 0 s

Tactic:
exact single_eq_of_ne (Ne.symm hs)

Result:
no goals
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
lemma LinearOrderedCommGroupWithZero.wellFoundedOn_setOf_le_lt_iff_nonempty_discrete_of_ne_zero
    {G₀ : Type*} [LinearOrderedCommGroupWithZero G₀] [Nontrivial G₀ˣ] {g : G₀} (hg : g ≠ 0) :
    Set.WellFoundedOn {x : G₀ | g ≤ x} (· < ·) ↔ Nonempty (G₀ ≃*o ℤₘ₀)

Proof state:
case refine_4
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ ≃*o ℤₘ₀
a✝ b✝ : G₀ˣ
⊢ ↑((WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun a✝) ≤
      ↑((WithZero.withZeroUnitsEquiv.trans ↑f).unzero.toFun b✝) ↔
    a✝ ≤ b✝

Tactic:
simp [WithZero.withZeroUnitsEquiv, MulEquiv.unzero]

Result:
no goals

Proof state:
case refine_2.inr.inr
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
this : ({x | g ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2) ↔ {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
f : G₀ˣ ≃*o Multiplicative ℤ
a b : G₀
ha : a ≠ 0
hb : b ≠ 0
⊢ (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun a ≤
      (WithZero.withZeroUnitsEquiv.symm.trans f.withZero).toFun b ↔
    a ≤ b

Tactic:
simp [WithZero.withZeroUnitsEquiv, MulEquiv.withZero, ha, hb, ← Units.val_le_val]

Result:
no goals

Proof state:
case refine_5
G₀ : Type u_2
inst✝¹ : LinearOrderedCommGroupWithZero G₀
inst✝ : Nontrivial G₀ˣ
g : G₀
hg : g ≠ 0
h✝ : {x | Units.mk0 g hg ≤ x}.WellFoundedOn fun x1 x2 => x1 < x2
a✝² : G₀
a✝¹ : g ≤ a✝²
ha0 : ¬a✝² = 0
b✝ : G₀
a✝ : g ≤ b✝
hb0 : ¬b✝ = 0
h : a✝² < b✝
⊢ (if h : a✝² = 0 then 1 else Units.mk0 a✝² h) < if h : b✝ = 0 then 1 else Units.mk0 b✝ h

Tactic:
simp [ha0, hb0, ← Units.val_lt_val, h]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/TransfiniteComposition.lean
lemma transfiniteCompositions_le [IsStableUnderTransfiniteComposition.{w} W] :
    transfiniteCompositions.{w} W ≤ W

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W f

Tactic:
rw [transfiniteCompositions_iff] at hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
⊢ W f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : ∃ J x x_1 x_2, ∃ (x_3 : WellFoundedLT J), W.transfiniteCompositionsOfShape J f
⊢ W f

Tactic:
obtain ⟨J, _, _, _, _, hf⟩ := hf

Result:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W.transfiniteCompositionsOfShape J f
⊢ W f

Proof state:
case intro.intro.intro.intro.intro
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
J : Type w
w✝³ : LinearOrder J
w✝² : SuccOrder J
w✝¹ : OrderBot J
w✝ : WellFoundedLT J
hf : W.transfiniteCompositionsOfShape J f
⊢ W f

Tactic:
exact W.transfiniteCompositionsOfShape_le J _ hf

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
⊢ transfiniteCompositions.{w, v, u} W ≤ W

Tactic:
intro _ _ f hf

Result:
C : Type u
inst✝¹ : Category.{v, u} C
W : MorphismProperty C
inst✝ : W.IsStableUnderTransfiniteComposition
X✝ Y✝ : C
f : X✝ ⟶ Y✝
hf : transfiniteCompositions.{w, v, u} W f
⊢ W f
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem memℓp_zero_iff {f : ∀ i, E i} : Memℓp f 0 ↔ Set.Finite { i | f i ≠ 0 }

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if 0 = 0 then {i | ¬f i = 0}.Finite else Summable fun i => ‖f i‖ ^ 0) ↔ {i | ¬f i = 0}.Finite

Tactic:
rw [if_pos rfl]

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ Memℓp f 0 ↔ {i | f i ≠ 0}.Finite

Tactic:
dsimp [Memℓp]

Result:
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f : (i : α) → E i
⊢ (if 0 = 0 then {i | ¬f i = 0}.Finite else Summable fun i => ‖f i‖ ^ 0) ↔ {i | ¬f i = 0}.Finite
-- Mathlib/Topology/Algebra/Monoid.lean
theorem Filter.tendsto_cocompact_mul_right {a b : M} (ha : a * b = 1) :
    Filter.Tendsto (fun x : M => x * a) (Filter.cocompact M) (Filter.cocompact M)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)

Tactic:
simp only [comp_mul_right, ha, mul_one]

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x) (cocompact M) (cocompact M)

Tactic:
exact Filter.tendsto_id

Result:
no goals

Proof state:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto (fun x => x * a) (cocompact M) (cocompact M)

Tactic:
refine Filter.Tendsto.of_tendsto_comp ?_ (Filter.comap_cocompact_le (continuous_mul_right b))

Result:
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : Monoid M
inst✝ : ContinuousMul M
a b : M
ha : a * b = 1
⊢ Tendsto ((fun b_1 => b_1 * b) ∘ fun x => x * a) (cocompact M) (cocompact M)
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
@[simp] lemma mem_piAntidiag : f ∈ piAntidiag s n ↔ s.sum f = n ∧ ∀ i, f i ≠ 0 → i ∈ s

Proof state:
case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
constructor

Result:
case a.mp
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f) →
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) →
    ∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f

Proof state:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∑ i : Fin #s, (f ∘ Subtype.val ∘ ⇑e.symm) i = ∑ x ∈ s.attach, f ↑x

Tactic:
exact Fintype.sum_equiv e.symm _ _ (by simp)

Result:
no goals

Proof state:
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
⊢ f ∈
      Trunc.lift
        (fun e =>
          map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Fintype.truncEquivFinOfCardEq ⋯) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Tactic:
induction' Fintype.truncEquivFinOfCardEq (Fintype.card_coe s) using Trunc.ind with e

Result:
case a
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ f ∈
      Trunc.lift
        (fun e =>
          map { toFun := fun f i => if hi : i ∈ s then f (e ⟨i, hi⟩) else 0, inj' := ⋯ } (finAntidiagonal (#s) n))
        ⋯ (Trunc.mk e) ↔
    s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s

Proof state:
case a.mpr
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
n : μ
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
⊢ (s.sum f = n ∧ ∀ (i : ι), f i ≠ 0 → i ∈ s) →
    ∃ a, ∑ i : Fin #s, a i = n ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f

Tactic:
rintro ⟨rfl, hf⟩

Result:
case a.mpr.intro
ι : Type u_1
μ : Type u_2
inst✝³ : DecidableEq ι
inst✝² : AddCommMonoid μ
inst✝¹ : HasAntidiagonal μ
inst✝ : DecidableEq μ
s : Finset ι
f : ι → μ
e : { x // x ∈ s } ≃ Fin #s
hf : ∀ (i : ι), f i ≠ 0 → i ∈ s
⊢ ∃ a, ∑ i : Fin #s, a i = s.sum f ∧ (fun i => if hi : i ∈ s then a (e ⟨i, hi⟩) else 0) = f