harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem isRoot_cyclotomic_iff [NeZero (n : R)] {μ : R} :
    IsRoot (cyclotomic n R) μ ↔ IsPrimitiveRoot μ n

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
rw [← isRoot_map_iff hf, ← IsPrimitiveRoot.map_iff_of_injective hf, map_cyclotomic, ←
  isRoot_cyclotomic_iff']

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
have hf : Function.Injective _ := IsFractionRing.injective R (FractionRing R)

Result:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n

Proof state:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n

Tactic:
haveI : NeZero (n : FractionRing R) := NeZero.nat_of_injective hf

Result:
R : Type u_1
inst✝² : CommRing R
n : ℕ
inst✝¹ : IsDomain R
inst✝ : NeZero ↑n
μ : R
hf : Function.Injective ⇑(algebraMap R (FractionRing R))
this : NeZero ↑n
⊢ (cyclotomic n R).IsRoot μ ↔ IsPrimitiveRoot μ n
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem add_slash (k : ℤ) (A : GL(2, ℝ)⁺) (f g : ℍ → ℂ) :
    (f + g) ∣[k]A = f ∣[k]A + g ∣[k]A

Proof state:
case h
k : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x✝ : ℍ
⊢ (f (A • x✝) + g (A • x✝)) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ =
    f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ +
      g (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹

Tactic:
ring

Result:
no goals

Proof state:
k : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
⊢ (f + g) ∣[k]A = f ∣[k]A + g ∣[k]A

Tactic:
ext1

Result:
case h
k : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x✝ : ℍ
⊢ ((f + g) ∣[k]A) x✝ = (f ∣[k]A + g ∣[k]A) x✝

Proof state:
case h
k : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x✝ : ℍ
⊢ ((f + g) ∣[k]A) x✝ = (f ∣[k]A + g ∣[k]A) x✝

Tactic:
simp only [slash, Pi.add_apply, denom, zpow_neg]

Result:
case h
k : ℤ
A : ↥GL(2, ℝ)⁺
f g : ℍ → ℂ
x✝ : ℍ
⊢ (f (A • x✝) + g (A • x✝)) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ =
    f (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹ +
      g (A • x✝) * ↑(↑↑A).det ^ (k - 1) * ((↑(↑↑A 1 0) * ↑x✝ + ↑(↑↑A 1 1)) ^ k)⁻¹
-- Mathlib/Data/Finset/Sups.lean
@[simp] lemma diffs_compls_eq_infs (s t : Finset α) : s \\ tᶜˢ = s ⊼ t

Proof state:
α : Type u_2
inst✝¹ : BooleanAlgebra α
inst✝ : DecidableEq α
s t : Finset α
⊢ s \\ tᶜˢ = s ⊼ t

Tactic:
rw [← infs_compls_eq_diffs, compls_compls]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_eq_none : find? p l = none ↔ ∀ x ∈ l, ¬ p x

Proof state:
α✝ : Type u_1
p : α✝ → Bool
l : Array α✝
⊢ find? p l = none ↔ ∀ (x : α✝), x ∈ l → ¬p x = true

Tactic:
cases l

Result:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ find? p { toList := toList✝ } = none ↔ ∀ (x : α✝), x ∈ { toList := toList✝ } → ¬p x = true

Proof state:
case mk
α✝ : Type u_1
p : α✝ → Bool
toList✝ : List α✝
⊢ find? p { toList := toList✝ } = none ↔ ∀ (x : α✝), x ∈ { toList := toList✝ } → ¬p x = true

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem _root_.Real.nnnorm_rpow_of_nonneg {x y : ℝ} (hx : 0 ≤ x) : ‖x ^ y‖₊ = ‖x‖₊ ^ y

Proof state:
x y : ℝ
hx : 0 ≤ x
⊢ ‖x ^ y‖₊ = ‖x‖₊ ^ y

Tactic:
ext

Result:
case a
x y : ℝ
hx : 0 ≤ x
⊢ ↑‖x ^ y‖₊ = ↑(‖x‖₊ ^ y)

Proof state:
case a
x y : ℝ
hx : 0 ≤ x
⊢ ↑‖x ^ y‖₊ = ↑(‖x‖₊ ^ y)

Tactic:
exact Real.norm_rpow_of_nonneg hx

Result:
no goals
-- Mathlib/FieldTheory/MvRatFunc/Rank.lean
theorem MvRatFunc.rank_eq_max_lift
    {σ : Type u} {F : Type v} [Field F] [Nonempty σ] :
    Module.rank F (FractionRing (MvPolynomial σ F)) = lift.{u} #F ⊔ lift.{v} #σ ⊔ ℵ₀

Proof state:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))

Tactic:
have h1 := (IsScalarTower.toAlgHom F R K).toLinearMap.rank_le_of_injective hinj

Result:
case refine_2
σ : Type u
F : Type v
inst✝¹ : Field F
inst✝ : Nonempty σ
R : Type (max u v) := MvPolynomial σ F
K : Type (max u v) := FractionRing R
hinj : Function.Injective ⇑(algebraMap R K)
h1 : Module.rank F R ≤ Module.rank F K
⊢ lift.{u, v} #F ⊔ lift.{v, u} #σ ⊔ ℵ₀ ≤ Module.rank F (FractionRing (MvPolynomial σ F))
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
theorem DirichletCharacter.LSeries_eulerProduct_hasProd {N : ℕ} (χ : DirichletCharacter ℂ N)
    (hs : 1 < s.re) :
    HasProd (fun p : Primes ↦ (1 - χ p * (p : ℂ) ^ (-s))⁻¹) (L ↗χ s)

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n)

Tactic:
convert eulerProduct_completely_multiplicative_hasProd <| summable_dirichletSummand χ hs

Result:
no goals

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (L (fun n => χ ↑n) s)

Tactic:
rw [← tsum_dirichletSummand χ hs]

Result:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ HasProd (fun p => (1 - χ ↑↑p * ↑↑p ^ (-s))⁻¹) (∑' (n : ℕ), (dirichletSummandHom χ ⋯) n)
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem mem_support_iff {f : SkewMonoidAlgebra k G} {a : G} : a ∈ f.support ↔ f.coeff a ≠ 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
f : SkewMonoidAlgebra k G
a : G
⊢ a ∈ f.support ↔ f.coeff a ≠ 0

Tactic:
rcases f with ⟨⟩

Result:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝ : G →₀ k
⊢ a ∈ { toFinsupp := toFinsupp✝ }.support ↔ { toFinsupp := toFinsupp✝ }.coeff a ≠ 0

Proof state:
case ofFinsupp
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G
toFinsupp✝ : G →₀ k
⊢ a ∈ { toFinsupp := toFinsupp✝ }.support ↔ { toFinsupp := toFinsupp✝ }.coeff a ≠ 0

Tactic:
simp only [coeff, support_ofFinsupp, Finsupp.mem_support_iff, ne_eq, implies_true]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma mu_eq_neg_sum_Ico_of_ne (hab : a ≠ b) :
    mu 𝕜 a b = -∑ x ∈ Ico a b, mu 𝕜 a x

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
rw [mu_apply, if_neg hab]

Result:
no goals
-- Mathlib/Data/Multiset/Pi.lean
theorem cons_map (b : δ a) (f : ∀ a' ∈ m, δ a')
    {δ' : α → Sort*} (φ : ∀ ⦃a'⦄, δ a' → δ' a') :
    Pi.cons _ _ (φ b) (fun a' ha' ↦ φ (f a' ha')) = (fun a' ha' ↦ φ ((cons _ _ b f) a' ha'))

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ cons m a (φ b) (fun a' ha' => φ (f a' ha')) a' ha' = φ (cons m a b f a' ha')

Tactic:
refine (congrArg₂ _ ?_ rfl).trans (apply_dite (@φ _) (a' = a) _ _).symm

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ (fun h => ⋯ ▸ φ b) = fun h => φ (⋯ ▸ b)

Proof state:
case h.h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
b : δ a'
ha' : a' ∈ a' ::ₘ m
⊢ ⋯ ▸ φ b = φ (⋯ ▸ b)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
⊢ (cons m a (φ b) fun a' ha' => φ (f a' ha')) = fun a' ha' => φ (cons m a b f a' ha')

Tactic:
ext a' ha'

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ cons m a (φ b) (fun a' ha' => φ (f a' ha')) a' ha' = φ (cons m a b f a' ha')

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
a : α
b : δ a
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
ha' : a' ∈ a ::ₘ m
⊢ (fun h => ⋯ ▸ φ b) = fun h => φ (⋯ ▸ b)

Tactic:
ext rfl

Result:
case h.h.h
α : Type u_1
inst✝ : DecidableEq α
δ : α → Sort u_2
m : Multiset α
f : (a' : α) → a' ∈ m → δ a'
δ' : α → Sort u_3
φ : ⦃a' : α⦄ → δ a' → δ' a'
a' : α
b : δ a'
ha' : a' ∈ a' ::ₘ m
⊢ ⋯ ▸ φ b = φ (⋯ ▸ b)
-- Mathlib/Analysis/ODE/Gronwall.lean
theorem hasDerivAt_gronwallBound_shift (δ K ε x a : ℝ) :
    HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x

Proof state:
case h.e'_9
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1

Tactic:
rw [id, mul_one]

Result:
no goals

Proof state:
δ K ε x a : ℝ
⊢ HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x

Tactic:
convert (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1

Result:
case h.e'_9
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem liftNC_smul [MulOneClass G] {R : Type*} [Semiring R] (f : k →+* R) (g : G →* R) (c : k)
    (φ : MonoidAlgebra k G) : liftNC (f : k →+ R) g (c • φ) = f c * liftNC (f : k →+ R) g φ

Proof state:
case H.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c)).comp (singleAddHom x✝¹)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom x✝¹)) x✝

Tactic:
simp_rw [AddMonoidHom.comp_apply, singleAddHom_apply, smulAddHom_apply,
  AddMonoidHom.coe_mulLeft, smul_single', liftNC_single, AddMonoidHom.coe_coe, map_mul, mul_assoc]

Result:
no goals

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ (liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)

Tactic:
ext

Result:
case H.h
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
x✝¹ : G
x✝ : k
⊢ (((liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c)).comp (singleAddHom x✝¹)) x✝ =
    (((AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)).comp (singleAddHom x✝¹)) x✝

Proof state:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ (liftNC ↑f ⇑g) (c • φ) = f c * (liftNC ↑f ⇑g) φ

Tactic:
suffices (liftNC (↑f) g).comp (smulAddHom k (MonoidAlgebra k G) c) =
    (AddMonoidHom.mulLeft (f c)).comp (liftNC (↑f) g) from
  DFunLike.congr_fun this φ

Result:
k : Type u₁
G : Type u₂
inst✝² : Semiring k
inst✝¹ : MulOneClass G
R : Type u_3
inst✝ : Semiring R
f : k →+* R
g : G →* R
c : k
φ : MonoidAlgebra k G
⊢ (liftNC ↑f ⇑g).comp ((smulAddHom k (MonoidAlgebra k G)) c) = (AddMonoidHom.mulLeft (f c)).comp (liftNC ↑f ⇑g)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem ofNat_add {n} (x y : Nat) : BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y

Proof state:
n x y : Nat
⊢ BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y

Tactic:
apply eq_of_toNat_eq

Result:
case a
n x y : Nat
⊢ (BitVec.ofNat n (x + y)).toNat = (BitVec.ofNat n x + BitVec.ofNat n y).toNat

Proof state:
case a
n x y : Nat
⊢ (BitVec.ofNat n (x + y)).toNat = (BitVec.ofNat n x + BitVec.ofNat n y).toNat

Tactic:
simp [BitVec.ofNat, Fin.ofNat'_add]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma bi_min_div_two_lt_one : b (min_bi b) / 2 < 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ b (min_bi b) / 2 < 1

Tactic:
have gt_zero : 0 < b (min_bi b) := R.b_pos (min_bi b)

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < b (min_bi b)

Tactic:
aesop (add safe apply div_two_lt_of_pos)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
gt_zero : 0 < b (min_bi b)
⊢ b (min_bi b) / 2 < 1

Tactic:
calc b (min_bi b) / 2 < b (min_bi b) := by aesop (add safe apply div_two_lt_of_pos)
                    _ < 1 := R.b_lt_one _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_erase [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} :
    Const.get? (m.erase k) a = if k == a then none else get? m a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
⊢ get? (m.erase k) a = if (k == a) = true then none else get? m a

Tactic:
simp_to_model [erase] using List.getValue?_eraseKey

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem pairwise_disjoint_of_mem_zpowers :
    Pairwise fun (i j : f.cycleFactorsFinset) ↦
      ∀ (x y : Perm α), x ∈ Subgroup.zpowers ↑i → y ∈ Subgroup.zpowers ↑j → Disjoint x y :=
  fun c d  hcd ↦ fun x y hx hy ↦ by
  obtain ⟨m, hm⟩ := hx; obtain ⟨n, hn⟩ := hy
  simp only [← hm, ← hn]
  apply Disjoint.zpow_disjoint_zpow
  exact f.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr hcd)

Proof state:
case intro.intro.hστ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ (↑c).Disjoint ↑d

Tactic:
exact f.cycleFactorsFinset_pairwise_disjoint c.prop d.prop (Subtype.coe_ne_coe.mpr hcd)

Result:
no goals

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ x.Disjoint y

Tactic:
simp only [← hm, ← hn]

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ (↑c ^ m).Disjoint (↑d ^ n)

Proof state:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
hy : y ∈ Subgroup.zpowers ↑d
m : ℤ
hm : (fun x => ↑c ^ x) m = x
⊢ x.Disjoint y

Tactic:
obtain ⟨n, hn⟩ := hy

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ x.Disjoint y

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
hx : x ∈ Subgroup.zpowers ↑c
hy : y ∈ Subgroup.zpowers ↑d
⊢ x.Disjoint y

Tactic:
obtain ⟨m, hm⟩ := hx

Result:
case intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
hy : y ∈ Subgroup.zpowers ↑d
m : ℤ
hm : (fun x => ↑c ^ x) m = x
⊢ x.Disjoint y

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ (↑c ^ m).Disjoint (↑d ^ n)

Tactic:
apply Disjoint.zpow_disjoint_zpow

Result:
case intro.intro.hστ
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f : Perm α
c d : { x // x ∈ f.cycleFactorsFinset }
hcd : c ≠ d
x y : Perm α
m : ℤ
hm : (fun x => ↑c ^ x) m = x
n : ℤ
hn : (fun x => ↑d ^ x) n = y
⊢ (↑c).Disjoint ↑d
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
/-- Let `{a | p a}` be a subsemigroup of a commutative monoid `M`. If `m` is a subadditive function
(`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division by a natural and `f` is a function
valued in that subsemigroup, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
lemma le_expect_of_subadditive_on_pred (h_zero : m 0 = 0)
    (h_add : ∀ a b, p a → p b → m (a + b) ≤ m a + m b) (hp_add : ∀ a b, p a → p b → p (a + b))
    (h_div : ∀ (n : ℕ) a, p a → m (a /ℚ n) = m a /ℚ n)
    (hs : ∀ i ∈ s, p (f i)) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Proof state:
case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
exact le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs

Result:
no goals

Proof state:
case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ ∅, p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

Tactic:
simp [h_zero]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)

Tactic:
obtain rfl | hs_nonempty := s.eq_empty_or_nonempty

Result:
case inl
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ ∅, p (f i)
⊢ m (𝔼 i ∈ ∅, f i) ≤ 𝔼 i ∈ ∅, m (f i)

case inr
ι : Type u_1
M : Type u_4
N : Type u_5
inst✝⁴ : AddCommMonoid M
inst✝³ : Module ℚ≥0 M
inst✝² : OrderedAddCommMonoid N
inst✝¹ : Module ℚ≥0 N
inst✝ : PosSMulMono ℚ≥0 N
m : M → N
p : M → Prop
f : ι → M
s : Finset ι
h_zero : m 0 = 0
h_add : ∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b
hp_add : ∀ (a b : M), p a → p b → p (a + b)
h_div : ∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a
hs : ∀ i ∈ s, p (f i)
hs_nonempty : s.Nonempty
⊢ m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)
-- Mathlib/MeasureTheory/OuterMeasure/Basic.lean
theorem measure_biUnion_le {I : Set ι} (μ : F) (hI : I.Countable) (s : ι → Set α) :
    μ (⋃ i ∈ I, s i) ≤ ∑' i : I, μ (s i)

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
rw [biUnion_eq_iUnion]

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ x, s ↑x) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
apply measure_iUnion_le

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
⊢ μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)

Tactic:
have := hI.to_subtype

Result:
α : Type u_1
ι : Type u_2
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
I : Set ι
μ : F
hI : I.Countable
s : ι → Set α
this : Countable ↑I
⊢ μ (⋃ i ∈ I, s i) ≤ ∑' (i : ↑I), μ (s ↑i)
-- Mathlib/Algebra/Regular/SMul.lean
theorem of_mul_eq_one (h : a * b = 1) : IsSMulRegular M b :=
  of_mul (a := a) (by rw [h]; exact one M)

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1

Tactic:
exact one M

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M (a * b)

Tactic:
rw [h]

Result:
R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
-- Mathlib/Topology/ApproximateUnit.lean
/-- In a topological unital magma, `𝓝 1` is the largest approximate unit. -/
lemma iff_neBot_and_le_nhds_one [ContinuousMul α] {l : Filter α} :
    IsApproximateUnit l ↔ l.NeBot ∧ l ≤ 𝓝 1 :=
  ⟨fun hl ↦ ⟨hl.neBot, by simpa using hl.tendsto_mul_left 1⟩,
    And.elim fun _ hl ↦ nhds_one α |>.mono hl⟩

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : MulOneClass α
inst✝ : ContinuousMul α
l : Filter α
hl : l.IsApproximateUnit
⊢ l ≤ 𝓝 1

Tactic:
simpa using hl.tendsto_mul_left 1

Result:
no goals
-- Mathlib/Order/Directed.lean
theorem directedOn_range {f : ι → α} : Directed r f ↔ DirectedOn r (Set.range f)

Proof state:
α : Type u
ι : Sort w
r : α → α → Prop
f : ι → α
⊢ Directed r f ↔ DirectedOn r (Set.range f)

Tactic:
simp_rw [Directed, DirectedOn, Set.forall_mem_range, Set.exists_range_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/NatCast.lean
/-- See `zero_lt_four'` for a version with the type explicit. -/
@[simp] lemma zero_lt_four : (0 : α) < 4

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3 + 1

Tactic:
exact lt_add_of_lt_of_nonneg zero_lt_three zero_le_one

Result:
no goals

Proof state:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 4

Tactic:
rw [← three_add_one_eq_four]

Result:
α : Type u_1
inst✝⁴ : AddMonoidWithOne α
inst✝³ : PartialOrder α
inst✝² : ZeroLEOneClass α
inst✝¹ : NeZero 1
inst✝ : AddLeftMono α
⊢ 0 < 3 + 1