harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem map_zpow' [DivInvMonoid G] [DivInvMonoid H] [MonoidHomClass F G H]
    (f : F) (hf : ∀ x : G, f x⁻¹ = (f x)⁻¹) (a : G) : ∀ n : ℤ, f (a ^ n) = f a ^ n
  | (n : ℕ) => by rw [zpow_natCast, map_pow, zpow_natCast]
  | Int.negSucc n => by rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f (a ^ ↑n) = f a ^ ↑n

Tactic:
rw [zpow_natCast, map_pow, zpow_natCast]

Result:
no goals

Proof state:
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : DivInvMonoid G
inst✝¹ : DivInvMonoid H
inst✝ : MonoidHomClass F G H
f : F
hf : ∀ (x : G), f x⁻¹ = (f x)⁻¹
a : G
n : ℕ
⊢ f (a ^ Int.negSucc n) = f a ^ Int.negSucc n

Tactic:
rw [zpow_negSucc, hf, map_pow, ← zpow_negSucc]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean
theorem toIdeal_iSup {κ : Sort*} (s : κ → HomogeneousIdeal 𝒜) :
    (⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal

Proof state:
ι : Type u_1
σ : Type u_2
A : Type u_3
inst✝⁵ : Semiring A
inst✝⁴ : DecidableEq ι
inst✝³ : AddMonoid ι
inst✝² : SetLike σ A
inst✝¹ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝ : GradedRing 𝒜
κ : Sort u_4
s : κ → HomogeneousIdeal 𝒜
⊢ (⨆ i, s i).toIdeal = ⨆ i, (s i).toIdeal

Tactic:
rw [iSup, toIdeal_sSup, iSup_range]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem setSeq_prod_subset {N m n} (hm : N ≤ m) (hn : N ≤ n) :
    setSeq hf U_mem m ×ˢ setSeq hf U_mem n ⊆ U N := fun p hp => by
  refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux
  · exact setSeq_mono hf U_mem hm hp.1
  · exact setSeq_mono hf U_mem hn hp.2

Proof state:
case refine_2.a
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N

Tactic:
exact setSeq_mono hf U_mem hn hp.2

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p ∈ U N

Tactic:
refine (setSeqAux hf U_mem N).2.2 ⟨?_, ?_⟩ <;> apply setSeq_sub_aux

Result:
case refine_1.a
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N

case refine_2.a
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.2 ∈ setSeq hf U_mem N

Proof state:
case refine_1.a
α : Type u
uniformSpace : UniformSpace α
f : Filter α
hf : Cauchy f
U : ℕ → Set (α × α)
U_mem : ∀ (n : ℕ), U n ∈ 𝓤 α
N m n : ℕ
hm : N ≤ m
hn : N ≤ n
p : α × α
hp : p ∈ setSeq hf U_mem m ×ˢ setSeq hf U_mem n
⊢ p.1 ∈ setSeq hf U_mem N

Tactic:
exact setSeq_mono hf U_mem hm hp.1

Result:
no goals
-- Mathlib/Data/Nat/Choose/Basic.lean
theorem choose_eq_choose_pred_add {n k : ℕ} (hn : 0 < n) (hk : 0 < k) :
    choose n k = choose (n - 1) (k - 1) + choose (n - 1) k

Proof state:
n k : ℕ
hn : 0 < n
hk : 0 < k
⊢ n.choose k = (n - 1).choose (k - 1) + (n - 1).choose k

Tactic:
obtain ⟨l, rfl⟩ : ∃ l, k = l + 1 := Nat.exists_eq_add_of_le' hk

Result:
case intro
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)

Proof state:
case intro
n : ℕ
hn : 0 < n
l : ℕ
hk : 0 < l + 1
⊢ n.choose (l + 1) = (n - 1).choose (l + 1 - 1) + (n - 1).choose (l + 1)

Tactic:
rw [choose_succ_right _ _ hn, Nat.add_one_sub_one]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Basic.lean
theorem length_sub : (s - t).length = s.length + t.length

Proof state:
α : Type u_2
inst✝ : OrderedAddCommGroup α
s t : NonemptyInterval α
⊢ (s - t).length = s.length + t.length

Tactic:
simp [sub_eq_add_neg]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/AdicValuation.lean
theorem valuation_lt_one_iff_dvd (r : R) :
    v.valuation K r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ (valuation K v) ↑r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
rw [valuation_of_algebraMap]

Result:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
r : R
⊢ v.intValuation r < 1 ↔ v.asIdeal ∣ Ideal.span {r}

Tactic:
exact v.intValuation_lt_one_iff_dvd r

Result:
no goals
-- Mathlib/Topology/FiberBundle/Constructions.lean
theorem Pullback.continuous_lift (f : B' → B) : Continuous (@Pullback.lift B F E B' f)

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝

Tactic:
exact inf_le_right

Result:
no goals

Proof state:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ Continuous (Pullback.lift f)

Tactic:
rw [continuous_iff_le_induced, Pullback.TotalSpace.topologicalSpace, pullbackTopology_def]

Result:
B : Type u
F : Type v
E : B → Type w₁
B' : Type w₂
inst✝¹ : TopologicalSpace B'
inst✝ : TopologicalSpace (TotalSpace F E)
f : B' → B
⊢ induced TotalSpace.proj inst✝¹ ⊓ induced (Pullback.lift f) inst✝ ≤ induced (Pullback.lift f) inst✝
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Summable.toNNReal {f : α → ℝ} (hf : Summable f) : Summable fun n => (f n).toNNReal

Proof state:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun n => (f n).toNNReal

Tactic:
apply NNReal.summable_coe.1

Result:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun a => ↑(f a).toNNReal

Proof state:
α : Type u_1
f : α → ℝ
hf : Summable f
n : α
⊢ ↑(f n).toNNReal ≤ |f n|

Tactic:
simp only [le_abs_self, Real.coe_toNNReal', max_le_iff, abs_nonneg, and_self_iff]

Result:
no goals

Proof state:
α : Type u_1
f : α → ℝ
hf : Summable f
⊢ Summable fun a => ↑(f a).toNNReal

Tactic:
refine .of_nonneg_of_le (fun n => NNReal.coe_nonneg _) (fun n => ?_) hf.abs

Result:
α : Type u_1
f : α → ℝ
hf : Summable f
n : α
⊢ ↑(f n).toNNReal ≤ |f n|
-- Mathlib/Algebra/Star/Unitary.lean
lemma map_mem {r : R} (hr : r ∈ unitary R) : f r ∈ unitary S

Proof state:
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
r : R
hr : star r * r = 1 ∧ r * star r = 1
⊢ f r ∈ unitary S

Tactic:
simpa [map_star, map_mul] using And.intro congr(f $(hr.1)) congr(f $(hr.2))

Result:
no goals

Proof state:
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
r : R
hr : r ∈ unitary R
⊢ f r ∈ unitary S

Tactic:
rw [unitary.mem_iff] at hr

Result:
F : Type u_2
R : Type u_3
S : Type u_4
inst✝⁶ : Monoid R
inst✝⁵ : StarMul R
inst✝⁴ : Monoid S
inst✝³ : StarMul S
inst✝² : FunLike F R S
inst✝¹ : StarHomClass F R S
inst✝ : MonoidHomClass F R S
f : F
r : R
hr : star r * r = 1 ∧ r * star r = 1
⊢ f r ∈ unitary S
-- Mathlib/RingTheory/PowerBasis.lean
theorem algHom_ext {S' : Type*} [Semiring S'] [Algebra R S'] (pb : PowerBasis R S)
    ⦃f g : S →ₐ[R] S'⦄ (h : f pb.gen = g pb.gen) : f = g

Proof state:
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
⊢ f = g

Tactic:
ext x

Result:
case H
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
x : S
⊢ f x = g x

Proof state:
case H
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f g : S →ₐ[R] S'
h : f pb.gen = g pb.gen
x : S
⊢ f x = g x

Tactic:
obtain ⟨f, rfl⟩ := pb.exists_eq_aeval' x

Result:
case H.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ f✝ ((aeval pb.gen) f) = g ((aeval pb.gen) f)

Proof state:
case H.intro
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
S' : Type u_7
inst✝¹ : Semiring S'
inst✝ : Algebra R S'
pb : PowerBasis R S
f✝ g : S →ₐ[R] S'
h : f✝ pb.gen = g pb.gen
f : R[X]
⊢ f✝ ((aeval pb.gen) f) = g ((aeval pb.gen) f)

Tactic:
rw [← Polynomial.aeval_algHom_apply, ← Polynomial.aeval_algHom_apply, h]

Result:
no goals
-- Mathlib/Topology/Category/Stonean/EffectiveEpi.lean
theorem effectiveEpi_tfae
    {B X : Stonean.{u}} (π : X ⟶ B) :
    TFAE
    [ EffectiveEpi π
    , Epi π
    , Function.Surjective π
    ]

Proof state:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_finish

Result:
no goals

Proof state:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 2 ↔ 3 := epi_iff_surjective π

Result:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : Stonean
π : X ⟶ B
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 1 → 2 := fun _ ↦ inferInstance

Result:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Proof state:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE

Tactic:
tfae_have 3 → 1 := fun hπ ↦ ⟨⟨effectiveEpiStruct π hπ⟩⟩

Result:
B X : Stonean
π : X ⟶ B
tfae_1_to_2 : EffectiveEpi π → Epi π
tfae_2_iff_3 : Epi π ↔ Function.Surjective ⇑(ConcreteCategory.hom π)
tfae_3_to_1 : Function.Surjective ⇑(ConcreteCategory.hom π) → EffectiveEpi π
⊢ [EffectiveEpi π, Epi π, Function.Surjective ⇑(ConcreteCategory.hom π)].TFAE
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthInf_of_eventually_ge {u v : ℕ → ℝ≥0∞} {c : ℝ≥0∞} (hc : c ≠ 0)
    (h : ∀ᶠ n in atTop, c * u n ≤ v n) :
    expGrowthInf u ≤ expGrowthInf v

Proof state:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x => c) + expGrowthInf u

Tactic:
rcases eq_top_or_lt_top c with rfl | c_top

Result:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x => ⊤) + expGrowthInf u

case inr
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
c_top : c < ⊤
⊢ expGrowthInf u ≤ (expGrowthInf fun x => c) + expGrowthInf u

Proof state:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x => ⊤) + expGrowthInf u

Tactic:
rw [← Pi.top_def, expGrowthInf_top]

Result:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthInf u ≤ ⊤ + expGrowthInf u

Proof state:
case inr
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
c_top : c < ⊤
⊢ expGrowthInf u ≤ (expGrowthInf fun x => c) + expGrowthInf u

Tactic:
rw [expGrowthInf_const hc c_top.ne, zero_add]

Result:
no goals

Proof state:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
apply (expGrowthInf_eventually_monotone h).trans' (le_expGrowthInf_mul.trans' _)

Result:
u v : ℕ → ℝ≥0∞
c : ℝ≥0∞
hc : c ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, c * u n ≤ v n
⊢ expGrowthInf u ≤ (expGrowthInf fun x => c) + expGrowthInf u

Proof state:
case inl
u v : ℕ → ℝ≥0∞
hc : ⊤ ≠ 0
h : ∀ᶠ (n : ℕ) in atTop, ⊤ * u n ≤ v n
⊢ expGrowthInf u ≤ ⊤ + expGrowthInf u

Tactic:
exact le_add_of_nonneg_left le_top

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_eq_zero :
    emultiplicity a b = 0 ↔ ¬a ∣ b

Proof state:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
by_cases hf : FiniteMultiplicity a b

Result:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Proof state:
case neg
α : Type u_1
inst✝ : Monoid α
a b : α
hf : ¬FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
simpa [emultiplicity_eq_top.2 hf] using FiniteMultiplicity.not_iff_forall.1 hf 1

Result:
no goals

Proof state:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ emultiplicity a b = 0 ↔ ¬a ∣ b

Tactic:
rw [← ENat.coe_zero, emultiplicity_eq_coe]

Result:
case pos
α : Type u_1
inst✝ : Monoid α
a b : α
hf : FiniteMultiplicity a b
⊢ a ^ 0 ∣ b ∧ ¬a ^ (0 + 1) ∣ b ↔ ¬a ∣ b
-- Mathlib/NumberTheory/Modular.lean
theorem abs_two_mul_re_lt_one_of_mem_fdo (h : z ∈ 𝒟ᵒ) : |2 * z.re| < 1

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |2 * z.re| < 1

Tactic:
rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)]

Result:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Proof state:
z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |z.re| < 1 / 2

Tactic:
exact h.2

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
lemma isExtensionPair_iff_cod : L.IsExtensionPair M N ↔
    ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ g.1.cod ∧ f ≤ g

Proof state:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
⊢ (∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g) → L.IsExtensionPair M N

Tactic:
intro h f m

Result:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g

Proof state:
case refine_2
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g

Tactic:
obtain ⟨g, h1, h2⟩ := h f.symm m

Result:
case refine_2.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
g : L.FGEquiv N M
h1 : m ∈ (↑g).cod
h2 : f.symm ≤ g
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g

Proof state:
case refine_2.intro.intro
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
h : ∀ (f : L.FGEquiv N M) (m : M), ∃ g, m ∈ (↑g).cod ∧ f ≤ g
f : L.FGEquiv M N
m : M
g : L.FGEquiv N M
h1 : m ∈ (↑g).cod
h2 : f.symm ≤ g
⊢ ∃ g, m ∈ (↑g).dom ∧ f ≤ g

Tactic:
exact ⟨g.symm, h1, monotone_symm h2⟩

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem of_nonneg_disjoint_union_eq_zero {s : SignedMeasure α} {A B : Set α} (h : Disjoint A B)
    (hA₁ : MeasurableSet A) (hB₁ : MeasurableSet B) (hA₂ : 0 ≤ s A) (hB₂ : 0 ≤ s B)
    (hAB : s (A ∪ B) = 0) : s A = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0

Tactic:
linarith

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s (A ∪ B) = 0
⊢ ↑s A = 0

Tactic:
rw [of_union h hA₁ hB₁] at hAB

Result:
α : Type u_1
m : MeasurableSpace α
s : SignedMeasure α
A B : Set α
h : Disjoint A B
hA₁ : MeasurableSet A
hB₁ : MeasurableSet B
hA₂ : 0 ≤ ↑s A
hB₂ : 0 ≤ ↑s B
hAB : ↑s A + ↑s B = 0
⊢ ↑s A = 0
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma toNNReal_mul_add_neg_mul_add_mul_neg_eq (f g : C(X, ℝ)) :
    (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
      (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
⊢ (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal

Tactic:
ext x

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ ↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) x) =
    ↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) x)

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ f x * g x ⊔ 0 + (-(f x * (g x ⊔ 0)) + (f x ⊔ 0) * (g x ⊔ 0)) + (-((f x ⊔ 0) * g x) + (f x ⊔ 0) * (g x ⊔ 0)) =
    -(f x * g x) + f x * g x ⊔ 0 + (f x ⊔ 0) * (g x ⊔ 0) +
      (-((f x ⊔ 0) * g x) + f x * g x + (-(f x * (g x ⊔ 0)) + (f x ⊔ 0) * (g x ⊔ 0)))

Tactic:
abel

Result:
no goals

Proof state:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ ↑(((f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal) x) =
    ↑(((-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal) x)

Tactic:
simp [max_neg_zero, add_mul, mul_add]

Result:
case h.a
X : Type u_1
inst✝ : TopologicalSpace X
f g : C(X, ℝ)
x : X
⊢ f x * g x ⊔ 0 + (-(f x * (g x ⊔ 0)) + (f x ⊔ 0) * (g x ⊔ 0)) + (-((f x ⊔ 0) * g x) + (f x ⊔ 0) * (g x ⊔ 0)) =
    -(f x * g x) + f x * g x ⊔ 0 + (f x ⊔ 0) * (g x ⊔ 0) +
      (-((f x ⊔ 0) * g x) + f x * g x + (-(f x * (g x ⊔ 0)) + (f x ⊔ 0) * (g x ⊔ 0)))
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem lift_self_apply (h : IsAdjoinRoot S f) (x : S) :
    h.lift (algebraMap R S) h.root h.aeval_root x = x

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
f : R[X]
h : IsAdjoinRoot S f
x : S
⊢ (lift (algebraMap R S) h.root h ⋯) x = x

Tactic:
rw [← h.map_repr x, lift_map, ← aeval_def, h.aeval_eq]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Function.Bijective.cauchySeq_comp_iff {f : ℕ → ℕ} (hf : Bijective f) (u : ℕ → α) :
    CauchySeq (u ∘ f) ↔ CauchySeq u

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
⊢ CauchySeq (u ∘ f) ↔ CauchySeq u

Tactic:
refine ⟨fun H => ?_, fun H => H.comp_injective hf.injective⟩

Result:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u

Proof state:
α : Type u
uniformSpace : UniformSpace α
f : ℕ → ℕ
hf : Bijective f
u : ℕ → α
H : CauchySeq (u ∘ f)
⊢ CauchySeq u

Tactic:
lift f to ℕ ≃ ℕ using hf

Result:
case intro
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ⇑f)
⊢ CauchySeq u

Proof state:
case intro
α : Type u
uniformSpace : UniformSpace α
u : ℕ → α
f : ℕ ≃ ℕ
H : CauchySeq (u ∘ ⇑f)
⊢ CauchySeq u

Tactic:
simpa only [Function.comp_def, f.apply_symm_apply] using H.comp_injective f.symm.injective

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem upperCrossingTime_le : upperCrossingTime a b f N n ω ≤ N

Proof state:
case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N

Tactic:
simp only [upperCrossingTime_succ, hitting_le]

Result:
no goals

Proof state:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ upperCrossingTime a b f N n ω ≤ N

Tactic:
cases n

Result:
case zero
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
⊢ upperCrossingTime a b f N 0 ω ≤ N

case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N

Proof state:
case zero
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
⊢ upperCrossingTime a b f N 0 ω ≤ N

Tactic:
simp only [upperCrossingTime_zero, Pi.bot_apply, bot_le]

Result:
no goals