harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Basic.lean
theorem dense_compl_singleton (x : X) [NeBot (𝓝[≠] x)] : Dense ({x}ᶜ : Set X)

Proof state:
case inr
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ y ∈ closure {x}ᶜ

Tactic:
exact subset_closure hne

Result:
no goals

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
⊢ Dense {x}ᶜ

Tactic:
intro y

Result:
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
⊢ y ∈ closure {x}ᶜ

Proof state:
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
⊢ y ∈ closure {x}ᶜ

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Result:
case inl
X : Type u
inst✝¹ : TopologicalSpace X
y : X
inst✝ : (𝓝[≠] y).NeBot
⊢ y ∈ closure {y}ᶜ

case inr
X : Type u
inst✝¹ : TopologicalSpace X
x : X
inst✝ : (𝓝[≠] x).NeBot
y : X
hne : y ≠ x
⊢ y ∈ closure {x}ᶜ

Proof state:
case inl
X : Type u
inst✝¹ : TopologicalSpace X
y : X
inst✝ : (𝓝[≠] y).NeBot
⊢ y ∈ closure {y}ᶜ

Tactic:
rwa [mem_closure_iff_nhdsWithin_neBot]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_eq (m n) : cmp m n = Ordering.eq ↔ m = n

Proof state:
m n : PosNum
⊢ Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)

Tactic:
cases cmp m n <;> intro this <;> simp at this ⊢ <;> try { exact this } <;>
simp [show m ≠ n from fun e => by rw [e] at this;exact lt_irrefl _ this]

Result:
no goals

Proof state:
m n : PosNum
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
have := cmp_to_nat m n

Result:
m n : PosNum
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n

Proof state:
m n : PosNum
this : Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m)
⊢ m.cmp n = Ordering.eq ↔ m = n

Tactic:
revert this

Result:
m n : PosNum
⊢ Ordering.casesOn (m.cmp n) (↑m < ↑n) (m = n) (↑n < ↑m) → (m.cmp n = Ordering.eq ↔ m = n)

Proof state:
case eq
m n : PosNum
this : m = n
⊢ m = n

Tactic:
exact this

Result:
no goals

Proof state:
m n : PosNum
this : ↑n < ↑n
e : m = n
⊢ False

Tactic:
exact lt_irrefl _ this

Result:
no goals

Proof state:
m n : PosNum
this : ↑n < ↑m
e : m = n
⊢ False

Tactic:
rw [e] at this

Result:
m n : PosNum
this : ↑n < ↑n
e : m = n
⊢ False
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem sup'_comm {t : Finset γ} (hs : s.Nonempty) (ht : t.Nonempty) (f : β → γ → α) :
    (s.sup' hs fun b => t.sup' ht (f b)) = t.sup' ht fun c => s.sup' hs fun b => f b c :=
  eq_of_forall_ge_iff fun a => by simpa using forall₂_swap

Proof state:
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝ : SemilatticeSup α
s : Finset β
t : Finset γ
hs : s.Nonempty
ht : t.Nonempty
f : β → γ → α
a : α
⊢ (s.sup' hs fun b => t.sup' ht (f b)) ≤ a ↔ (t.sup' ht fun c => s.sup' hs fun b => f b c) ≤ a

Tactic:
simpa using forall₂_swap

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem IsUniformInducing.uniformEquicontinuous_iff {F : ι → β → α} {u : α → γ}
    (hu : IsUniformInducing u) : UniformEquicontinuous F ↔ UniformEquicontinuous ((u ∘ ·) ∘ F)

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F)

Tactic:
have := UniformFun.postcomp_isUniformInducing (α := ι) hu

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F)

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformEquicontinuous F ↔ UniformEquicontinuous ((fun x => u ∘ x) ∘ F)

Tactic:
simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff]

Result:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformContinuous ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) ↔
    UniformContinuous (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F))

Proof state:
ι : Type u_1
α : Type u_6
β : Type u_8
γ : Type u_10
uα : UniformSpace α
uβ : UniformSpace β
uγ : UniformSpace γ
F : ι → β → α
u : α → γ
hu : IsUniformInducing u
this : IsUniformInducing (⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun)
⊢ UniformContinuous ((⇑ofFun ∘ (fun x => u ∘ x) ∘ ⇑toFun) ∘ ⇑ofFun ∘ swap F) ↔
    UniformContinuous (⇑ofFun ∘ swap ((fun x => u ∘ x) ∘ F))

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_atTop_zero_iff_le_of_antitone {β : Type*} [Nonempty β] [SemilatticeSup β]
    {f : β → ℝ≥0∞} (hf : Antitone f) :
    Filter.Tendsto f Filter.atTop (𝓝 0) ↔ ∀ ε, 0 < ε → ∃ n : β, f n ≤ ε

Proof state:
case refine_2.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
exact ⟨n, fun m hm ↦ (hf hm).trans hn⟩

Result:
no goals

Proof state:
case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Result:
case refine_2.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
n : β
hn : f n ≤ ε
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Proof state:
case refine_1.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : ∀ n_1 ≥ n, f n_1 ≤ ε
⊢ ∃ n, f n ≤ ε

Tactic:
exact ⟨n, hn n le_rfl⟩

Result:
no goals

Proof state:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε

Tactic:
refine ⟨fun h ↦ fun ε hε ↦ ?_, fun h ↦ fun ε hε ↦ ?_⟩

Result:
case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

case refine_2
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε
ε : ℝ≥0∞
hε : ε > 0
⊢ ∃ N, ∀ n ≥ N, f n ≤ ε

Proof state:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ Tendsto f atTop (𝓝 0) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε

Tactic:
rw [ENNReal.tendsto_atTop_zero]

Result:
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
⊢ (∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε) ↔ ∀ (ε : ℝ≥0∞), 0 < ε → ∃ n, f n ≤ ε

Proof state:
case refine_1
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
⊢ ∃ n, f n ≤ ε

Tactic:
obtain ⟨n, hn⟩ := h ε hε

Result:
case refine_1.intro
β : Type u_4
inst✝¹ : Nonempty β
inst✝ : SemilatticeSup β
f : β → ℝ≥0∞
hf : Antitone f
h : ∀ ε > 0, ∃ N, ∀ n ≥ N, f n ≤ ε
ε : ℝ≥0∞
hε : 0 < ε
n : β
hn : ∀ n_1 ≥ n, f n_1 ≤ ε
⊢ ∃ n, f n ≤ ε
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem factorial_mul_pow_le_factorial : ∀ {m n : ℕ}, m ! * (m + 1) ^ n ≤ (m + n)!
  | m, 0 => by simp
  | m, n + 1 => by
    rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]
    exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

Proof state:
m n : ℕ
⊢ m ! * (m + 1) ^ (n + 1) ≤ (m + (n + 1))!

Tactic:
rw [← Nat.add_assoc, factorial_succ, Nat.mul_comm (_ + 1), Nat.pow_succ, ← Nat.mul_assoc]

Result:
m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)

Proof state:
m : ℕ
⊢ m ! * (m + 1) ^ 0 ≤ (m + 0)!

Tactic:
simp

Result:
no goals

Proof state:
m n : ℕ
⊢ m ! * (m + 1) ^ n * (m + 1) ≤ (m + n)! * (m + n + 1)

Tactic:
exact Nat.mul_le_mul factorial_mul_pow_le_factorial (succ_le_succ (le_add_right _ _))

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Turan.lean
theorem equivalence_not_adj : Equivalence (¬G.Adj · ·) where
  refl

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ {x y : V}, ¬G.Adj x y → ¬G.Adj y x

Tactic:
simp [adj_comm]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Fintype V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
r : ℕ
h : G.IsTuranMaximal r
⊢ ∀ (x : V), ¬G.Adj x x

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem topologicalSpace_eq :
    UniformOnFun.topologicalSpace α β 𝔖 =
      ⨅ (s : Set α) (_ : s ∈ 𝔖), TopologicalSpace.induced
        (UniformFun.ofFun ∘ s.restrict ∘ toFun 𝔖) (UniformFun.topologicalSpace s β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ topologicalSpace α β 𝔖 =
    ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)

Tactic:
simp only [UniformOnFun.topologicalSpace, UniformSpace.toTopologicalSpace_iInf]

Result:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace =
    ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : UniformSpace β
𝔖 : Set (Set α)
⊢ ⨅ i ∈ 𝔖, UniformSpace.toTopologicalSpace =
    ⨅ s ∈ 𝔖, TopologicalSpace.induced (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.topologicalSpace (↑s) β)

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem card_Ioo_eq_card_Ico_sub_one (a b : α) : #(Ioo a b) = #(Ico a b) - 1

Proof state:
case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ioo_eq_empty h, Ico_eq_empty h, card_empty, Nat.zero_sub]

Result:
no goals

Proof state:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1

Tactic:
exact (Nat.add_sub_cancel _ _).symm

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
by_cases h : a < b

Result:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

case neg
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : ¬a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Proof state:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ico a b) - 1

Tactic:
rw [Ico_eq_cons_Ioo h, card_cons]

Result:
case pos
α : Type u_2
inst✝¹ : PartialOrder α
inst✝ : LocallyFiniteOrder α
a b : α
h : a < b
⊢ #(Ioo a b) = #(Ioo a b) + 1 - 1
-- Mathlib/Probability/Kernel/Basic.lean
theorem setLIntegral_piecewise (a : α) (g : β → ℝ≥0∞) (t : Set β) :
    ∫⁻ b in t, g b ∂piecewise hs κ η a =
      if a ∈ s then ∫⁻ b in t, g b ∂κ a else ∫⁻ b in t, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, g b ∂(piecewise hs κ η) a = if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a

Tactic:
simp_rw [piecewise_apply]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝ : DecidablePred fun x => x ∈ s
a : α
g : β → ℝ≥0∞
t : Set β
⊢ (∫⁻ (b : β) in t, g b ∂if a ∈ s then κ a else η a) =
    if a ∈ s then ∫⁻ (b : β) in t, g b ∂κ a else ∫⁻ (b : β) in t, g b ∂η a

Tactic:
split_ifs <;> rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem smul_integral_comp_mul_add (c d) :
    (c • ∫ x in a..b, f (c * x + d)) = ∫ x in c * a + d..c * b + d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
c d : ℝ
⊢ c • ∫ (x : ℝ) in a..b, f (c * x + d) = ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
by_cases hc : c = 0 <;> simp [hc, integral_comp_mul_add]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem cardQuot_mul [IsDedekindDomain S] [Module.Free ℤ S] (I J : Ideal S) :
    cardQuot (I * J) = cardQuot I * cardQuot J

Proof state:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I J : Ideal S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
let b := Module.Free.chooseBasis ℤ S

Result:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Proof state:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I✝ J✝ : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
this : Infinite S
I J : Submodule S S
hI : IsUnit J
⊢ (I * J).cardQuot = I.cardQuot * J.cardQuot

Tactic:
simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top]

Result:
no goals

Proof state:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
haveI : Infinite S := Infinite.of_surjective _ b.repr.toEquiv.surjective

Result:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
this : Infinite S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Proof state:
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDedekindDomain S
inst✝ : Module.Free ℤ S
I J : Ideal S
b : Basis (Module.Free.ChooseBasisIndex ℤ S) ℤ S := Module.Free.chooseBasis ℤ S
this : Infinite S
⊢ cardQuot (I * J) = cardQuot I * cardQuot J

Tactic:
exact UniqueFactorizationMonoid.multiplicative_of_coprime cardQuot I J (cardQuot_bot _ _)
    (fun {I J} hI => by simp [Ideal.isUnit_iff.mp hI, Ideal.mul_top])
    (fun {I} i hI =>
      have : Ideal.IsPrime I := Ideal.isPrime_of_prime hI
      cardQuot_pow_of_prime hI.ne_zero)
    fun {I J} hIJ => cardQuot_mul_of_coprime <| Ideal.isCoprime_iff_sup_eq.mpr
      (Ideal.isUnit_iff.mp
        (hIJ (Ideal.dvd_iff_le.mpr le_sup_left) (Ideal.dvd_iff_le.mpr le_sup_right)))

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem exists_lt_of_le_liminf [AddMonoid α] [AddLeftStrictMono α] {x ε : α} {u : ℕ → α}
    (hu_bdd : IsBoundedUnder GE.ge atTop u) (hu : x ≤ Filter.liminf u atTop) (hε : ε < 0) :
    ∃ n : PNat, x + ε < u n

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
⊢ ∃ n, x + ε < u ↑n

Tactic:
have h : ∀ᶠ n : ℕ in atTop, x + ε < u n := eventually_add_neg_lt_of_le_liminf hu_bdd hu hε

Result:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∀ᶠ (n : ℕ) in atTop, x + ε < u n
⊢ ∃ n, x + ε < u ↑n

Proof state:
case intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
n : ℕ
hn : ∀ b ≥ n, x + ε < u b
⊢ ∃ n, x + ε < u ↑n

Tactic:
exact ⟨⟨n + 1, Nat.succ_pos _⟩, hn (n + 1) (Nat.le_succ _)⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∀ᶠ (n : ℕ) in atTop, x + ε < u n
⊢ ∃ n, x + ε < u ↑n

Tactic:
simp only [eventually_atTop] at h

Result:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∃ a, ∀ b ≥ a, x + ε < u b
⊢ ∃ n, x + ε < u ↑n

Proof state:
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
h : ∃ a, ∀ b ≥ a, x + ε < u b
⊢ ∃ n, x + ε < u ↑n

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case intro
α : Type u_1
inst✝² : ConditionallyCompleteLinearOrder α
inst✝¹ : AddMonoid α
inst✝ : AddLeftStrictMono α
x ε : α
u : ℕ → α
hu_bdd : IsBoundedUnder GE.ge atTop u
hu : x ≤ liminf u atTop
hε : ε < 0
n : ℕ
hn : ∀ b ≥ n, x + ε < u b
⊢ ∃ n, x + ε < u ↑n
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem toMeasure_normalize_eq_of_nonzero (nonzero : μ ≠ 0) :
    (μ.normalize : Measure Ω) = μ.mass⁻¹ • μ

Proof state:
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
⊢ ↑μ.normalize = μ.mass⁻¹ • ↑μ

Tactic:
ext1 s _s_mble

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.normalize s = (μ.mass⁻¹ • ↑μ) s

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.normalize s = (μ.mass⁻¹ • ↑μ) s

Tactic:
rw [← μ.normalize.ennreal_coeFn_eq_coeFn_toMeasure s, μ.normalize_eq_of_nonzero nonzero s,
  ENNReal.coe_mul, ennreal_coeFn_eq_coeFn_toMeasure]

Result:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.mass⁻¹ * ↑μ s = (μ.mass⁻¹ • ↑μ) s

Proof state:
case h
Ω : Type u_1
inst✝ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
nonzero : μ ≠ 0
s : Set Ω
_s_mble : MeasurableSet s
⊢ ↑μ.mass⁻¹ * ↑μ s = (μ.mass⁻¹ • ↑μ) s

Tactic:
exact Measure.coe_nnreal_smul_apply _ _ _

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma exact_of_f_is_kernel (hS : IsLimit (KernelFork.ofι S.f S.zero))
    [S.HasHomology] : S.Exact

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ S.Exact

Tactic:
rw [exact_iff_epi_toCycles]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ Epi S.toCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
this : IsSplitEpi S.toCycles
⊢ Epi S.toCycles

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = S.iCycles

Tactic:
exact Fork.IsLimit.lift_ι hS

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.toCycles = 𝟙 S.cycles

Tactic:
rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ hS.lift (KernelFork.ofι S.iCycles ⋯) ≫ S.f = S.iCycles

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
⊢ Epi S.toCycles

Tactic:
have : IsSplitEpi S.toCycles :=
  ⟨⟨{ section_ := hS.lift (KernelFork.ofι S.iCycles S.iCycles_g)
      id := by
        rw [← cancel_mono S.iCycles, assoc, toCycles_i, id_comp]
        exact Fork.IsLimit.lift_ι hS }⟩⟩

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
S : ShortComplex C
hS : IsLimit (KernelFork.ofι S.f ⋯)
inst✝ : S.HasHomology
this : IsSplitEpi S.toCycles
⊢ Epi S.toCycles
-- Mathlib/Data/List/OfFn.lean
theorem mem_ofFn' {n} (f : Fin n → α) (a : α) : a ∈ ofFn f ↔ a ∈ Set.range f

Proof state:
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ n_1, f (Fin.cast ⋯ n_1) = a
i : Fin (ofFn f).length
hi : f (Fin.cast ⋯ i) = a
⊢ (ofFn f).length = n

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ a ∈ ofFn f ↔ a ∈ Set.range f

Tactic:
simp only [mem_iff_get, Set.mem_range, get_ofFn]

Result:
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast ⋯ n_1) = a) ↔ ∃ y, f y = a

Proof state:
α : Type u
n : ℕ
f : Fin n → α
a : α
⊢ (∃ n_1, f (Fin.cast ⋯ n_1) = a) ↔ ∃ y, f y = a

Tactic:
exact ⟨fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩, fun ⟨i, hi⟩ => ⟨Fin.cast (by simp) i, hi⟩⟩

Result:
no goals

Proof state:
α : Type u
n : ℕ
f : Fin n → α
a : α
x✝ : ∃ y, f y = a
i : Fin n
hi : f i = a
⊢ n = (ofFn f).length

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroup.lean
theorem map_comp_apply {f : α → β} {g : β → γ} (x : FreeAbelianGroup α) :
    map (g ∘ f) x = (map g) ((map f) x)

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ (map (g ∘ f)) x = (map g) ((map f) x)

Tactic:
rw [map_comp]

Result:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ((map g).comp (map f)) x = (map g) ((map f) x)

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
x : FreeAbelianGroup α
⊢ ((map g).comp (map f)) x = (map g) ((map f) x)

Tactic:
rfl

Result:
no goals