harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Module/Equiv.lean
theorem inverse_id : (id R M).inverse = id R M

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ (id R M).inverse = id R M

Tactic:
rw [← ring_inverse_eq_map_inverse]

Result:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Ring.inverse (id R M) = id R M

Proof state:
R : Type u_3
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Ring.inverse (id R M) = id R M

Tactic:
exact Ring.inverse_one _

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inl_fst :
    (inl φ).comp (fst φ).1 (neg_add_cancel 1) = Cochain.ofHom (𝟙 F)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (inl φ).comp ↑(fst φ) ⋯ = Cochain.ofHom (𝟙 F)

Tactic:
ext p

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ ((inl φ).comp ↑(fst φ) ⋯).v p p ⋯ = (Cochain.ofHom (𝟙 F)).v p p ⋯

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ ((inl φ).comp ↑(fst φ) ⋯).v p p ⋯ = (Cochain.ofHom (𝟙 F)).v p p ⋯

Tactic:
simp [Cochain.comp_v _ _ (neg_add_cancel 1) p (p-1) p rfl (by omega)]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p : ℤ
⊢ p - 1 + 1 = p

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem pointwise_smul_toAddSubmonoid (a : M) (S : Ideal R)
    (ha : Function.Surjective fun r : R => a • r) :
    (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Proof state:
case h
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ x✝ ∈ (a • S).toAddSubmonoid ↔ x✝ ∈ a • S.toAddSubmonoid

Tactic:
exact Ideal.mem_map_iff_of_surjective _ <| by exact ha

Result:
no goals

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ Function.Surjective ⇑(MulSemiringAction.toRingHom M R a)

Tactic:
exact ha

Result:
no goals

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
⊢ (a • S).toAddSubmonoid = a • S.toAddSubmonoid

Tactic:
ext

Result:
case h
M : Type u_1
R : Type u_2
inst✝² : Monoid M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
ha : Function.Surjective fun r => a • r
x✝ : R
⊢ x✝ ∈ (a • S).toAddSubmonoid ↔ x✝ ∈ a • S.toAddSubmonoid
-- Mathlib/Data/Matroid/Loop.lean
/-- A version of `restrict_loops_eq` without the hypothesis that `R ⊆ M.E` -/
lemma restrict_loops_eq' (M : Matroid α) (R : Set α) :
    (M ↾ R).loops = (M.loops ∩ R) ∪ (R \ M.E)

Proof state:
α : Type u_1
M : Matroid α
R : Set α
⊢ (M ↾ R).loops = M.loops ∩ R ∪ R \ M.E

Tactic:
rw [loops, restrict_closure_eq', empty_inter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isNone_or : (or o o').isNone = (o.isNone && o'.isNone)

Proof state:
α✝ : Type u_1
o o' : Option α✝
⊢ (o.or o').isNone = (o.isNone && o'.isNone)

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem mem_map {a : α} {s : Stream' α} : a ∈ s → f a ∈ map f s := fun ⟨n, h⟩ =>
  Exists.intro n (by rw [get_map, h])

Proof state:
α : Type u
β : Type v
f : α → β
a : α
s : Stream' α
x✝ : a ∈ s
n : ℕ
h : (fun b => a = b) (s.get n)
⊢ (fun b => f a = b) ((map f s).get n)

Tactic:
rw [get_map, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_eq_getKeyD [BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {a fallback : α}
    (h : containsKey a l = true) :
    getKey a l h = getKeyD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l : List ((a : α) × β a)
a fallback : α
h : containsKey a l = true
⊢ getKey a l h = getKeyD a l fallback

Tactic:
rw [getKeyD_eq_getKey?, getKey, Option.get_eq_getD]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
@[simp, norm_cast]
lemma coe_succ_of_mem [SuccOrder α] {a : s} (h : succ ↑a ∈ s) :
    (succ a).1 = succ ↑a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(succ a) = succ ↑a

Tactic:
classical
change Subtype.val (dite ..) = _
split_ifs <;> trivial

Result:
no goals

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = succ ↑a

Tactic:
split_ifs <;> trivial

Result:
no goals

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(succ a) = succ ↑a

Tactic:
change Subtype.val (dite ..) = _

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : SuccOrder α
a : ↑s
h : succ ↑a ∈ s
⊢ ↑(if h : pred ↑(ofDual a) ∈ ⇑ofDual ⁻¹' s then ⟨pred ↑(ofDual a), h⟩ else ofDual a) = succ ↑a
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem map_comap_eq_self
    {f : K →+* L} {s : Subfield L} (h : s ≤ f.fieldRange) : (s.comap f).map f = s

Proof state:
K : Type u
L : Type v
inst✝¹ : DivisionRing K
inst✝ : DivisionRing L
f : K →+* L
s : Subfield L
h : s ≤ f.fieldRange
⊢ map f (comap f s) = s

Tactic:
simpa only [inf_of_le_left h] using map_comap_eq f s

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem of_injective : Function.Injective (@of α) := fun _ _ H => by
  let ⟨L₁, hx, hy⟩ := Red.exact.1 H
  simp [Red.singleton_iff] at hx hy; aesop

Proof state:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
⊢ x✝¹ = x✝

Tactic:
let ⟨L₁, hx, hy⟩ := Red.exact.1 H

Result:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝

Proof state:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : Red [(x✝¹, true)] L₁
hy : Red [(x✝, true)] L₁
⊢ x✝¹ = x✝

Tactic:
simp [Red.singleton_iff] at hx hy

Result:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝

Proof state:
α : Type u
x✝¹ x✝ : α
H : of x✝¹ = of x✝
L₁ : List (α × Bool)
hx : L₁ = [(x✝¹, true)]
hy : L₁ = [(x✝, true)]
⊢ x✝¹ = x✝

Tactic:
aesop

Result:
no goals
-- Mathlib/GroupTheory/Commutator/Basic.lean
theorem commutatorElement_eq_one_iff_mul_comm : ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Proof state:
G : Type u_1
inst✝ : Group G
g₁ g₂ : G
⊢ ⁅g₁, g₂⁆ = 1 ↔ g₁ * g₂ = g₂ * g₁

Tactic:
rw [commutatorElement_def, mul_inv_eq_one, mul_inv_eq_iff_eq_mul]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem of_le (N : Submonoid R) (h₁ : M ≤ N) (h₂ : ∀ r ∈ N, IsUnit (algebraMap R S r)) :
    IsLocalization N S where
  map_units' r := h₂ r r.2
  surj' s :=
    have ⟨⟨x, y, hy⟩, H⟩ := IsLocalization.surj M s
    ⟨⟨x, y, h₁ hy⟩, H⟩
  exists_of_eq {x y}

Proof state:
case intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
c : ↥M
hc : ↑c * x = ↑c * y
⊢ ∃ c, ↑c * x = ↑c * y

Tactic:
exact ⟨⟨c, h₁ c.2⟩, hc⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y

Tactic:
rintro ⟨c, hc⟩

Result:
case intro
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
c : ↥M
hc : ↑c * x = ↑c * y
⊢ ∃ c, ↑c * x = ↑c * y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (algebraMap R S) x = (algebraMap R S) y → ∃ c, ↑c * x = ↑c * y

Tactic:
rw [IsLocalization.eq_iff_exists M]

Result:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
N : Submonoid R
h₁ : M ≤ N
h₂ : ∀ r ∈ N, IsUnit ((algebraMap R S) r)
x y : R
⊢ (∃ c, ↑c * x = ↑c * y) → ∃ c, ↑c * x = ↑c * y
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem rightDualIso_id {X Y : C} (p : ExactPairing X Y) : rightDualIso p p = Iso.refl Y

Proof state:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (rightDualIso p p).hom = (Iso.refl Y).hom

Tactic:
simp only [rightDualIso, Iso.refl_hom, @rightAdjointMate_id _ _ _ _ ⟨Y⟩]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ rightDualIso p p = Iso.refl Y

Tactic:
ext

Result:
case w
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : C
p : ExactPairing X Y
⊢ (rightDualIso p p).hom = (Iso.refl Y).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem eq_of_mem_singleton (h : a ∈ #[b]) : a = b

Proof state:
α✝ : Type u_1
b a : α✝
h : a ∈ #[b]
⊢ a = b

Tactic:
simpa using h

Result:
no goals
-- Mathlib/RingTheory/Localization/Submodule.lean
theorem coeSubmodule_top : coeSubmodule S (⊤ : Ideal R) = 1

Proof state:
R : Type u_1
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ coeSubmodule S ⊤ = 1

Tactic:
rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_ne_zero : exp x ≠ 0 := fun h =>
  zero_ne_one (α := ℂ) <| by rw [← exp_zero, ← add_neg_cancel x, exp_add, h]; simp

Proof state:
x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)

Tactic:
simp

Result:
no goals

Proof state:
x : ℂ
h : cexp x = 0
⊢ 0 = 1

Tactic:
rw [← exp_zero, ← add_neg_cancel x, exp_add, h]

Result:
x : ℂ
h : cexp x = 0
⊢ x + -x = 0 * cexp (-x)
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_bot : (⊥ : SimpleGraph V).edgeFinset = ∅

Proof state:
V : Type u_1
⊢ ⊥.edgeFinset = ∅

Tactic:
simp [edgeFinset]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Equiv.lean
lemma commAlgEquiv_C_X (i) : commAlgEquiv R S₁ S₂ (.C (.X i)) = .X i

Proof state:
R : Type u_2
S₁ : Type u_3
S₂ : Type u_4
inst✝ : CommSemiring R
i : S₂
⊢ (commAlgEquiv R S₁ S₂) (C (X i)) = X i

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Algebra.lean
theorem hasProd_apply {γ : Type*} [CommMonoid β] [ContinuousMul β]
    {f : γ → C(α, β)} {g : C(α, β)} (hf : HasProd f g) (x : α) :
    HasProd (fun i : γ => f i x) (g x)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
hf : HasProd f g
x : α
⊢ HasProd (fun i => (f i) x) (g x)

Tactic:
let ev : C(α, β) →* β := (Pi.evalMonoidHom _ x).comp coeFnMonoidHom

Result:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
hf : HasProd f g
x : α
ev : C(α, β) →* β := (Pi.evalMonoidHom (fun a => β) x).comp coeFnMonoidHom
⊢ HasProd (fun i => (f i) x) (g x)

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
γ : Type u_3
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
f : γ → C(α, β)
g : C(α, β)
hf : HasProd f g
x : α
ev : C(α, β) →* β := (Pi.evalMonoidHom (fun a => β) x).comp coeFnMonoidHom
⊢ HasProd (fun i => (f i) x) (g x)

Tactic:
exact hf.map ev (continuous_eval_const x)

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem supIndep_pair [DecidableEq ι] {i j : ι} (hij : i ≠ j) :
    ({i, j} : Finset ι).SupIndep f ↔ Disjoint (f i) (f j)

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
suffices Disjoint (f i) (f j) → Disjoint (f j) ((Finset.erase {i, j} j).sup f) by
  simpa [supIndep_iff_disjoint_erase, hij]

Result:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)

Tactic:
rw [pair_comm]

Result:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({j, i}.erase j).sup f)

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
this : Disjoint (f i) (f j) → Disjoint (f j) (({i, j}.erase j).sup f)
⊢ {i, j}.SupIndep f ↔ Disjoint (f i) (f j)

Tactic:
simpa [supIndep_iff_disjoint_erase, hij]

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_3
inst✝² : Lattice α
inst✝¹ : OrderBot α
f : ι → α
inst✝ : DecidableEq ι
i j : ι
hij : i ≠ j
⊢ Disjoint (f i) (f j) → Disjoint (f j) (({j, i}.erase j).sup f)

Tactic:
simp [hij.symm, disjoint_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_eq_append_iff {l₁ : Vector α (n + m)} {l₂ : Vector β (n + m)} {l₁' : Vector (α × β) n} {l₂' : Vector (α × β) m} :
    zip l₁ l₂ = l₁' ++ l₂' ↔
      ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z

Proof state:
α : Type u_1
n m : Nat
β : Type u_2
l₁ : Vector α (n + m)
l₂ : Vector β (n + m)
l₁' : Vector (α × β) n
l₂' : Vector (α × β) m
⊢ l₁.zip l₂ = l₁' ++ l₂' ↔ ∃ w x y z, l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = w.zip y ∧ l₂' = x.zip z

Tactic:
simp [zip_eq_zipWith, zipWith_eq_append_iff]

Result:
no goals
-- Mathlib/Topology/DiscreteSubset.lean
lemma tendsto_cofinite_cocompact_iff :
    Tendsto f cofinite (cocompact _) ↔ ∀ K, IsCompact K → Set.Finite (f ⁻¹' K)

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite

Tactic:
simp only [mem_compl_iff, eventually_cofinite, not_not, preimage]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
⊢ Tendsto f cofinite (cocompact Y) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
rw [hasBasis_cocompact.tendsto_right_iff]

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
⊢ (∀ (i : Set Y), IsCompact i → ∀ᶠ (x : X) in cofinite, f x ∈ iᶜ) ↔ ∀ (K : Set Y), IsCompact K → (f ⁻¹' K).Finite

Tactic:
refine forall₂_congr (fun K _ ↦ ?_)

Result:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace Y
f : X → Y
K : Set Y
x✝ : IsCompact K
⊢ (∀ᶠ (x : X) in cofinite, f x ∈ Kᶜ) ↔ (f ⁻¹' K).Finite
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem isCoseparator_prod_of_isCoseparator_right (G H : C) [HasBinaryProduct G H]
    (hH : IsCoseparator H) : IsCoseparator (G ⨯ H) :=
  (isCoseparator_prod _ _).2 <| IsCoseparating.mono hH <| by simp

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroMorphisms C
G H : C
inst✝ : HasBinaryProduct G H
hH : IsCoseparator H
⊢ {H} ⊆ {G, H}

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem pi_div_two_ne_zero : ((π / 2 : ℝ) : Angle) ≠ 0

Proof state:
⊢ π / 2 ≠ 0

Tactic:
exact div_ne_zero Real.pi_ne_zero two_ne_zero

Result:
no goals

Proof state:
⊢ ↑(π / 2) ≠ 0

Tactic:
rw [← toReal_injective.ne_iff, toReal_pi_div_two, toReal_zero]

Result:
⊢ π / 2 ≠ 0
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
/-- If a functor inverts homotopy equivalences, it sends homotopic maps to the same map. -/
lemma _root_.Homotopy.map_eq_of_inverts_homotopyEquivalences
    {φ₀ φ₁ : F ⟶ G} (h : Homotopy φ₀ φ₁)(hc : ∀ j, ∃ i, c.Rel i j)
    [∀ i, HasBinaryBiproduct (F.X i) (F.X i)]
    [HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))]
    {D : Type*} [Category D] (H : HomologicalComplex C c ⥤ D)
    (hH : (homotopyEquivalences C c).IsInvertedBy H) :
    H.map φ₀ = H.map φ₁

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_4, u_1} C
inst✝⁴ : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
inst✝³ : DecidableRel c.Rel
φ₀ φ₁ : F ⟶ G
h : Homotopy φ₀ φ₁
hc : ∀ (j : ι), ∃ i, c.Rel i j
inst✝² : ∀ (i : ι), HasBinaryBiproduct (F.X i) (F.X i)
inst✝¹ : HasHomotopyCofiber (biprod.lift (𝟙 F) (-𝟙 F))
D : Type u_3
inst✝ : Category.{u_5, u_3} D
H : HomologicalComplex C c ⥤ D
hH : (homotopyEquivalences C c).IsInvertedBy H
⊢ H.map φ₀ = H.map φ₁

Tactic:
simp only [← cylinder.ι₀_desc _ _ h, ← cylinder.ι₁_desc _ _ h, H.map_comp,
  cylinder.map_ι₀_eq_map_ι₁ _ hc _ hH]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem IsSuccLimit.natCast_lt [AddMonoidWithOne α] [SuccAddOrder α] [CanonicallyOrderedAdd α]
    (hx : IsSuccLimit x) : ∀ n : ℕ, n < x

Proof state:
α : Type u_1
x : α
inst✝³ : PartialOrder α
inst✝² : AddMonoidWithOne α
inst✝¹ : SuccAddOrder α
inst✝ : CanonicallyOrderedAdd α
hx : IsSuccLimit x
⊢ ∀ (n : ℕ), ↑n < x

Tactic:
simpa [bot_eq_zero] using hx.add_natCast_lt hx.bot_lt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem beq_as_aig : ∀ (a b : Bool), (!(a && !b) && !(!a && b)) = (a == b)

Proof state:
⊢ ∀ (a b : Bool), (!(a && !b) && !(!a && b)) = (a == b)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_false_right : atLeastTwo a b false = (a && b)

Proof state:
a b : Bool
⊢ a.atLeastTwo b false = (a && b)

Tactic:
simp [atLeastTwo]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem absolutelyContinuous_of_isMulLeftInvariant [IsMulLeftInvariant ν] (hν : ν ≠ 0) : μ ≪ ν

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0
⊢ μ s = 0

Tactic:
exact h1

Result:
no goals

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
⊢ μ s = 0

Tactic:
have h1 := measure_mul_lintegral_eq μ ν sm 1 measurable_one

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s * ∫⁻ (y : G), 1 y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * 1 x⁻¹ ∂μ
⊢ μ s = 0

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
⊢ μ ≪ ν

Tactic:
refine AbsolutelyContinuous.mk fun s sm hνs => ?_

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
⊢ μ s = 0

Proof state:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s * ∫⁻ (y : G), 1 y ∂ν = ∫⁻ (x : G), ν ((fun z => z * x) ⁻¹' s) * 1 x⁻¹ ∂μ
⊢ μ s = 0

Tactic:
simp_rw [Pi.one_apply, lintegral_one, mul_one, (measure_mul_right_null ν _).mpr hνs,
  lintegral_zero, mul_eq_zero (M₀ := ℝ≥0∞), measure_univ_eq_zero.not.mpr hν, or_false] at h1

Result:
G : Type u_1
inst✝⁷ : MeasurableSpace G
inst✝⁶ : Group G
inst✝⁵ : MeasurableMul₂ G
μ ν : Measure G
inst✝⁴ : SFinite ν
inst✝³ : SFinite μ
inst✝² : MeasurableInv G
inst✝¹ : μ.IsMulLeftInvariant
inst✝ : ν.IsMulLeftInvariant
hν : ν ≠ 0
s : Set G
sm : MeasurableSet s
hνs : ν s = 0
h1 : μ s = 0
⊢ μ s = 0
-- Mathlib/MeasureTheory/Measure/Haar/Unique.lean
/-- **Uniqueness of Haar measures**:
Two Haar measures on a compact group coincide up to a multiplicative factor. -/
@[to_additive isAddInvariant_eq_smul_of_compactSpace]
lemma isMulInvariant_eq_smul_of_compactSpace [CompactSpace G] (μ' μ : Measure G)
    [IsHaarMeasure μ] [IsMulLeftInvariant μ'] [IsFiniteMeasureOnCompacts μ'] :
    μ' = haarScalarFactor μ' μ • μ

Proof state:
case h
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : CompactSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ'
s : Set G
_hs : MeasurableSet s
⊢ μ' s = (μ'.haarScalarFactor μ • μ) s

Tactic:
exact measure_isMulInvariant_eq_smul_of_isCompact_closure _ _ isClosed_closure.isCompact

Result:
no goals

Proof state:
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : CompactSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ'
⊢ μ' = μ'.haarScalarFactor μ • μ

Tactic:
ext s _hs

Result:
case h
G : Type u_1
inst✝⁸ : TopologicalSpace G
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MeasurableSpace G
inst✝⁴ : BorelSpace G
inst✝³ : CompactSpace G
μ' μ : Measure G
inst✝² : μ.IsHaarMeasure
inst✝¹ : μ'.IsMulLeftInvariant
inst✝ : IsFiniteMeasureOnCompacts μ'
s : Set G
_hs : MeasurableSet s
⊢ μ' s = (μ'.haarScalarFactor μ • μ) s
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
lemma trim_withDensity {m m0 : MeasurableSpace α} {μ : Measure α}
    (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
    (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ (μ.withDensity f).trim hm = (μ.trim hm).withDensity f

Tactic:
refine @Measure.ext _ m _ _ (fun s hs ↦ ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ((μ.trim hm).withDensity f) s

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
s : Set α
hs : MeasurableSet s
⊢ ((μ.withDensity f).trim hm) s = ((μ.trim hm).withDensity f) s

Tactic:
rw [withDensity_apply _ hs, restrict_trim _ _ hs, lintegral_trim _ hf, trim_measurableSet_eq _ hs,
  withDensity_apply _ (hm s hs)]

Result:
no goals
-- Mathlib/Topology/Algebra/Valued/LocallyCompact.lean
lemma norm_unit (u : 𝒪[K]ˣ) : ‖(u : 𝒪[K])‖ = 1

Proof state:
K : Type u_1
inst✝¹ : NontriviallyNormedField K
inst✝ : IsUltrametricDist K
u : (↥𝒪[K])ˣ
⊢ ‖↑u‖ = 1

Tactic:
simp

Result:
no goals