harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/ClosureSwap.lean
theorem finite_compl_fixedBy_closure_iff {S : Set G} :
    (∀ g ∈ closure S, (fixedBy α g)ᶜ.Finite) ↔ ∀ g ∈ S, (fixedBy α g)ᶜ.Finite :=
  ⟨fun h g hg ↦ h g (subset_closure hg), fun h g hg ↦ by
    refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
      (by simp) hg
    simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]⟩

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ (fixedBy α 1)ᶜ.Finite

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g✝ : G
hg✝ : g✝ ∈ closure S
g g' : G
x✝¹ : g ∈ closure S
x✝ : g' ∈ closure S
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ

Tactic:
simp_rw [← compl_inter, compl_subset_compl, fixedBy_mul]

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ ∀ x ∈ closure S, (fixedBy α x)ᶜ.Finite → (fixedBy α x⁻¹)ᶜ.Finite

Tactic:
simp

Result:
no goals

Proof state:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g : G
hg : g ∈ closure S
⊢ (fixedBy α g)ᶜ.Finite

Tactic:
refine closure_induction h (by simp) (fun g g' _ _ hg hg' ↦ (hg.union hg').subset ?_)
  (by simp) hg

Result:
G : Type u_1
α : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G α
S : Set G
h : ∀ g ∈ S, (fixedBy α g)ᶜ.Finite
g✝ : G
hg✝ : g✝ ∈ closure S
g g' : G
x✝¹ : g ∈ closure S
x✝ : g' ∈ closure S
hg : (fixedBy α g)ᶜ.Finite
hg' : (fixedBy α g')ᶜ.Finite
⊢ (fixedBy α (g * g'))ᶜ ⊆ (fixedBy α g)ᶜ ∪ (fixedBy α g')ᶜ
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : c ⟶ f.left}
    (w : S.map η ≫ f.hom = S.map η' ≫ f.hom) : η = η'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f : CostructuredArrow S T
h : f.IsUniversal
c : C
η η' : c ⟶ f.left
w : S.map η ≫ f.hom = S.map η' ≫ f.hom
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoUniformlyOn_iff_tendsto {F : ι → α → β} {f : α → β} {p : Filter ι} {s : Set α} :
    TendstoUniformlyOn F f p s ↔
    Tendsto (fun q : ι × α => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
s : Set α
⊢ TendstoUniformlyOn F f p s ↔ Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 β)

Tactic:
simp [tendstoUniformlyOn_iff_tendstoUniformlyOnFilter, tendstoUniformlyOnFilter_iff_tendsto]

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_lt (n : ℕ) (hn : 1 < n) : φ n < n :=
  (card_lt_card (filter_ssubset.2 ⟨0, by simp [hn.ne', pos_of_gt hn]⟩)).trans_eq (card_range n)

Proof state:
n : ℕ
hn : 1 < n
⊢ 0 ∈ range n ∧ ¬n.Coprime 0

Tactic:
simp [hn.ne', pos_of_gt hn]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem beq_self_right : ∀(a b : Bool), ((a == b) == b) = a

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

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.neg_eq [AddGroup α] [InvolutiveNeg β] (h : Antiperiodic f c) :
    f (-c) = -f 0

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddGroup α
inst✝ : InvolutiveNeg β
h : Antiperiodic f c
⊢ f (-c) = -f 0

Tactic:
simpa only [zero_add] using h.neg 0

Result:
no goals
-- Mathlib/Algebra/Lie/Normalizer.lean
@[simp]
lemma _root_.LieIdeal.idealizer_eq_normalizer (I : LieIdeal R L) :
    I.idealizer = I.normalizer

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x y : L
⊢ ⁅x, y⁆ ∈ I ↔ ⁅y, x⁆ ∈ I

Tactic:
simp only [← lie_skew x y, neg_mem_iff]

Result:
no goals

Proof state:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ idealizer I ↔ x ∈ normalizer I

Tactic:
exact forall_congr' fun y ↦ by simp only [← lie_skew x y, neg_mem_iff]

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ idealizer I = normalizer I

Tactic:
ext x

Result:
case h
R : Type u_1
L : Type u_2
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ idealizer I ↔ x ∈ normalizer I
-- Mathlib/Topology/Algebra/Constructions.lean
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead. -/
@[to_additive "An auxiliary lemma that can be used to prove that coercion `AddUnits M → M` is a
topological embedding. Use `AddUnits.isEmbedding_val` or `toAddUnits_homeomorph` instead."]
lemma isEmbedding_val_mk' {M : Type*} [Monoid M] [TopologicalSpace M] {f : M → M}
    (hc : ContinuousOn f {x : M | IsUnit x}) (hf : ∀ u : Mˣ, f u.1 = ↑u⁻¹) :
    IsEmbedding (val : Mˣ → M)

Proof state:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f ↑u)
⊢ (fun u => f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)

Tactic:
exact ⟨_, mem_inf_principal.1 (hc u u.isUnit hs), fun u' hu' ↦ hu' u'.isUnit⟩

Result:
no goals

Proof state:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u => ↑u⁻¹) x

Tactic:
intros u s hs

Result:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 ((fun u => ↑u⁻¹) u)
⊢ s ∈ Filter.map (fun u => ↑u⁻¹) (𝓝 u)

Proof state:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ IsEmbedding val

Tactic:
refine ⟨⟨?_⟩, ext⟩

Result:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝

Proof state:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 ((fun u => ↑u⁻¹) u)
⊢ s ∈ Filter.map (fun u => ↑u⁻¹) (𝓝 u)

Tactic:
simp only [← hf, nhds_induced, Filter.mem_map] at hs ⊢

Result:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
u : Mˣ
s : Set M
hs : s ∈ 𝓝 (f ↑u)
⊢ (fun u => f ↑u) ⁻¹' s ∈ comap val (𝓝 ↑u)

Proof state:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ instTopologicalSpaceUnits = TopologicalSpace.induced val inst✝

Tactic:
rw [topology_eq_inf, inf_eq_left, ← continuous_iff_le_induced,
  @continuous_iff_continuousAt _ _ (.induced _ _)]

Result:
M : Type u_3
inst✝¹ : Monoid M
inst✝ : TopologicalSpace M
f : M → M
hc : ContinuousOn f {x | IsUnit x}
hf : ∀ (u : Mˣ), f ↑u = ↑u⁻¹
⊢ ∀ (x : Mˣ), ContinuousAt (fun u => ↑u⁻¹) x
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma Exact.isZero_X₂_iff (hS : S.Exact) : IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0

Proof state:
case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 ∧ S.g = 0 → IsZero S.X₂

Tactic:
rintro ⟨hf, hg⟩

Result:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero S.X₂

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ IsZero S.X₂ → S.f = 0 ∧ S.g = 0

Tactic:
intro h

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : IsZero S.X₂
⊢ S.f = 0 ∧ S.g = 0

Proof state:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
h : IsZero S.X₂
⊢ S.f = 0 ∧ S.g = 0

Tactic:
exact ⟨h.eq_of_tgt _ _, h.eq_of_src _ _⟩

Result:
no goals

Proof state:
case mpr.intro
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
hf : S.f = 0
hg : S.g = 0
⊢ IsZero S.X₂

Tactic:
exact hS.isZero_X₂ hf hg

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ IsZero S.X₂ → S.f = 0 ∧ S.g = 0

case mpr
C : Type u_1
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Preadditive C
S : ShortComplex C
hS : S.Exact
⊢ S.f = 0 ∧ S.g = 0 → IsZero S.X₂
-- Mathlib/Topology/Constructions.lean
theorem Filter.HasBasis.prod_nhds {ιX ιY : Type*} {px : ιX → Prop} {py : ιY → Prop}
    {sx : ιX → Set X} {sy : ιY → Set Y} {x : X} {y : Y} (hx : (𝓝 x).HasBasis px sx)
    (hy : (𝓝 y).HasBasis py sy) :
    (𝓝 (x, y)).HasBasis (fun i : ιX × ιY => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2

Tactic:
exact hx.prod hy

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 (x, y)).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2

Tactic:
rw [nhds_prod_eq]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
ιX : Type u_5
ιY : Type u_6
px : ιX → Prop
py : ιY → Prop
sx : ιX → Set X
sy : ιY → Set Y
x : X
y : Y
hx : (𝓝 x).HasBasis px sx
hy : (𝓝 y).HasBasis py sy
⊢ (𝓝 x ×ˢ 𝓝 y).HasBasis (fun i => px i.1 ∧ py i.2) fun i => sx i.1 ×ˢ sy i.2
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_add_left' (a b : α) : toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp (p + a) b = toIcoDiv hp a b - 1

Tactic:
rw [add_comm, toIcoDiv_add_right']

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem comap_pure {b : β} : comap m (pure b) = 𝓟 (m ⁻¹' {b})

Proof state:
α : Type u_1
β : Type u_2
m : α → β
b : β
⊢ comap m (pure b) = 𝓟 (m ⁻¹' {b})

Tactic:
rw [← principal_singleton, comap_principal]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem collinear_of_sin_eq_zero {p₁ p₂ p₃ : P} (h : Real.sin (∠ p₁ p₂ p₃) = 0) :
    Collinear ℝ ({p₁, p₂, p₃} : Set P)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : sin (∠ p₁ p₂ p₃) = 0
⊢ Collinear ℝ {p₁, p₂, p₃}

Tactic:
revert h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ¬Collinear ℝ {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0

Tactic:
exact sin_ne_zero_of_not_collinear

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ sin (∠ p₁ p₂ p₃) = 0 → Collinear ℝ {p₁, p₂, p₃}

Tactic:
contrapose

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
⊢ ¬Collinear ℝ {p₁, p₂, p₃} → ¬sin (∠ p₁ p₂ p₃) = 0
-- Mathlib/Data/List/Intervals.lean
theorem filter_le_of_bot {n m : ℕ} (hnm : n < m) : ((Ico n m).filter fun x => x ≤ n) = [n]

Proof state:
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)

Tactic:
exact filter_congr fun _ _ => by
  simpa using Nat.lt_succ_iff.symm

Result:
no goals

Proof state:
n m : ℕ
hnm : n < m
x✝¹ : ℕ
x✝ : x✝¹ ∈ Ico n m
⊢ decide (x✝¹ ≤ n) = decide (x✝¹ < n + 1)

Tactic:
simpa using Nat.lt_succ_iff.symm

Result:
no goals

Proof state:
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = [n]

Tactic:
rw [← filter_lt_of_succ_bot hnm]

Result:
n m : ℕ
hnm : n < m
⊢ filter (fun x => decide (x ≤ n)) (Ico n m) = filter (fun x => decide (x < n + 1)) (Ico n m)
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem rank_le_of_injective_injective
    (i : R' →+* R) (j : S →+* S') (hi : Injective i) (hj : Injective j)
    (hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S') :
    Module.rank R S ≤ Module.rank R' S'

Proof state:
R : Type w
S : Type v
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring S
inst✝³ : Algebra R S
R' : Type w'
inst✝² : CommSemiring R'
S' : Type v
inst✝¹ : Semiring S'
inst✝ : Algebra R' S'
i : R' →+* R
j : S →+* S'
hi : Injective ⇑i
hj : Injective ⇑j
hc : (j.comp (algebraMap R S)).comp i = algebraMap R' S'
⊢ Module.rank R S ≤ Module.rank R' S'

Tactic:
simpa only [lift_id] using lift_rank_le_of_injective_injective i j hi hj hc

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem of_int_add (m : ℤ) (h : Irrational (m + x)) : Irrational x

Proof state:
x : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x

Tactic:
exact h.of_rat_add m

Result:
no goals

Proof state:
x : ℝ
m : ℤ
h : Irrational (↑m + x)
⊢ Irrational x

Tactic:
rw [← cast_intCast] at h

Result:
x : ℝ
m : ℤ
h : Irrational (↑↑m + x)
⊢ Irrational x
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsTopologicalGroup.t2Space_of_one_sep (H : ∀ x : G, x ≠ 1 → ∃ U ∈ 𝓝 (1 : G), x ∉ U) :
    T2Space G

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T1Space G

Tactic:
refine t1Space_iff_specializes_imp_eq.2 fun x y hspec ↦ by_contra fun hne ↦ ?_

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
⊢ False

Proof state:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ False

Tactic:
exact hU <| mem_of_mem_nhds <| hspec.map (continuous_mul_right y⁻¹) (by rwa [mul_inv_cancel])

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T2Space G

Tactic:
suffices T1Space G from inferInstance

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
⊢ T1Space G

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
⊢ False

Tactic:
rcases H (x * y⁻¹) (by rwa [Ne, mul_inv_eq_one]) with ⟨U, hU₁, hU⟩

Result:
case intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ False

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
⊢ x * y⁻¹ ≠ 1

Tactic:
rwa [Ne, mul_inv_eq_one]

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
H : ∀ (x : G), x ≠ 1 → ∃ U ∈ 𝓝 1, x ∉ U
x y : G
hspec : x ⤳ y
hne : ¬x = y
U : Set G
hU₁ : U ∈ 𝓝 1
hU : x * y⁻¹ ∉ U
⊢ U ∈ 𝓝 (y * y⁻¹)

Tactic:
rwa [mul_inv_cancel]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem eq_univ_of_powerset_subset {A : Class} (hA : powerset A ⊆ A) : A = univ :=
  eq_univ_of_forall
    (by
      by_contra! hnA
      exact
        WellFounded.min_mem ZFSet.mem_wf _ hnA
          (hA fun x hx =>
            Classical.not_not.1 fun hB =>
              WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx))

Proof state:
A : Class.{u_1}
hA : A.powerset ⊆ A
hnA : ∃ x, ¬A x
⊢ False

Tactic:
exact
  WellFounded.min_mem ZFSet.mem_wf _ hnA
    (hA fun x hx =>
      Classical.not_not.1 fun hB =>
        WellFounded.not_lt_min ZFSet.mem_wf _ hnA hB <| coe_apply.1 hx)

Result:
no goals

Proof state:
A : Class.{u_1}
hA : A.powerset ⊆ A
⊢ ∀ (x : ZFSet.{u_1}), A x

Tactic:
by_contra! hnA

Result:
A : Class.{u_1}
hA : A.powerset ⊆ A
hnA : ∃ x, ¬A x
⊢ False
-- Mathlib/FieldTheory/Galois/Infinite.lean
lemma fixedField_bot [IsGalois k K] :
    IntermediateField.fixedField (⊤ : Subgroup (K ≃ₐ[k] K)) = ⊥

Proof state:
k : Type u_1
K : Type u_2
inst✝³ : Field k
inst✝² : Field K
inst✝¹ : Algebra k K
inst✝ : IsGalois k K
⊢ IntermediateField.fixedField ⊤ = ⊥

Tactic:
rw [← IntermediateField.fixingSubgroup_bot, fixedField_fixingSubgroup]

Result:
no goals
-- Mathlib/Probability/Density.lean
theorem lintegral_eq_measure_univ {X : Ω → E} [HasPDF X ℙ μ] :
    ∫⁻ x, pdf X ℙ μ x ∂μ = ℙ Set.univ

Proof state:
Ω : Type u_1
E : Type u_2
inst✝¹ : MeasurableSpace E
m : MeasurableSpace Ω
ℙ : Measure Ω
μ : Measure E
X : Ω → E
inst✝ : HasPDF X ℙ μ
⊢ ∫⁻ (x : E), pdf X ℙ μ x ∂μ = ℙ Set.univ

Tactic:
rw [← setLIntegral_univ, ← map_eq_setLIntegral_pdf X ℙ μ MeasurableSet.univ,
  map_apply_of_aemeasurable (HasPDF.aemeasurable X ℙ μ) MeasurableSet.univ, Set.preimage_univ]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Finsupp.lean
theorem support_factorization {n : α} :
    (factorization n).support = (normalizedFactors n).toFinset

Proof state:
α : Type u_1
inst✝³ : CancelCommMonoidWithZero α
inst✝² : UniqueFactorizationMonoid α
inst✝¹ : NormalizationMonoid α
inst✝ : DecidableEq α
n : α
⊢ (factorization n).support = (normalizedFactors n).toFinset

Tactic:
simp [factorization, Multiset.toFinsupp_support]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_smul_self_of_nonneg (x : V) {r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) :
    o.oangle (r₁ • x) (r₂ • x) = 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
rcases hr₁.lt_or_eq with (h | h)

Result:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 < r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 = r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Proof state:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 = r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r₁ r₂ : ℝ
hr₁ : 0 ≤ r₁
hr₂ : 0 ≤ r₂
h : 0 < r₁
⊢ o.oangle (r₁ • x) (r₂ • x) = 0

Tactic:
simp [h, hr₂]

Result:
no goals
-- Mathlib/Topology/DiscreteQuotient.lean
theorem map_ofLE (cond : LEComap f A B) (h : A' ≤ A) (c : A') :
    map f cond (ofLE h c) = map f (cond.mono h le_rfl) c

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
⊢ map f cond (ofLE h c) = map f ⋯ c

Tactic:
rcases c with ⟨⟩

Result:
case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk (⇑A'.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A'.toSetoid) a✝)

Proof state:
case mk
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
A A' : DiscreteQuotient X
B : DiscreteQuotient Y
cond : LEComap f A B
h : A' ≤ A
c : Quotient A'.toSetoid
a✝ : X
⊢ map f cond (ofLE h (Quot.mk (⇑A'.toSetoid) a✝)) = map f ⋯ (Quot.mk (⇑A'.toSetoid) a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem isOneCoboundary_of_mem_oneCoboundaries
    (f : G → A) (hf : f ∈ oneCoboundaries (Rep.ofDistribMulAction k G A)) :
    IsOneCoboundary f

Proof state:
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
f : G → A
hf : f ∈ oneCoboundaries (Rep.ofDistribMulAction k G A)
⊢ IsOneCoboundary f

Tactic:
rcases hf with ⟨a, rfl⟩

Result:
case intro
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : ↑(Rep.ofDistribMulAction k G A).V
⊢ IsOneCoboundary ((dZero (Rep.ofDistribMulAction k G A)) a)

Proof state:
case intro
k G A : Type u
inst✝⁵ : CommRing k
inst✝⁴ : Group G
inst✝³ : AddCommGroup A
inst✝² : Module k A
inst✝¹ : DistribMulAction G A
inst✝ : SMulCommClass G k A
a : ↑(Rep.ofDistribMulAction k G A).V
⊢ IsOneCoboundary ((dZero (Rep.ofDistribMulAction k G A)) a)

Tactic:
exact ⟨a, fun _ => rfl⟩

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem castSucc_lt_or_lt_succ (p : Fin (n + 1)) (i : Fin n) : castSucc i < p ∨ p < i.succ

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ

Tactic:
simp [Fin.lt_def, -val_fin_lt]

Result:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑i < ↑p ∨ ↑p < ↑i + 1

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ ↑i < ↑p ∨ ↑p < ↑i + 1

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem associator_monoidal (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
    tensorμ (X₁ ⊗ X₂) X₃ (Y₁ ⊗ Y₂) Y₃ ≫
        (tensorμ X₁ X₂ Y₁ Y₂ ▷ (X₃ ⊗ Y₃)) ≫ (α_ (X₁ ⊗ Y₁) (X₂ ⊗ Y₂) (X₃ ⊗ Y₃)).hom =
      ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫
        tensorμ X₁ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃) ≫ ((X₁ ⊗ Y₁) ◁ tensorμ X₂ X₃ Y₂ Y₃)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ 𝟙 (((X₁ ⊗ X₂) ⊗ X₃) ⊗ (Y₁ ⊗ Y₂) ⊗ Y₃) ⊗≫
      X₁ ◁ X₂ ◁ (β_ X₃ Y₁).hom ▷ Y₂ ▷ Y₃ ⊗≫
        X₁ ◁ ((β_ X₂ Y₁).hom ▷ (X₃ ⊗ Y₂) ≫ (Y₁ ⊗ X₂) ◁ (β_ X₃ Y₂).hom) ▷ Y₃ ⊗≫ 𝟙 ((X₁ ⊗ Y₁) ⊗ (X₂ ⊗ Y₂) ⊗ X₃ ⊗ Y₃) =
    ((α_ X₁ X₂ X₃).hom ⊗ (α_ Y₁ Y₂ Y₃).hom) ≫
      ((α_ X₁ (X₂ ⊗ X₃) (Y₁ ⊗ Y₂ ⊗ Y₃)).hom ≫
          X₁ ◁ (α_ (X₂ ⊗ X₃) Y₁ (Y₂ ⊗ Y₃)).inv ≫
            X₁ ◁
                ((α_ X₂ X₃ Y₁).hom ≫
                    X₂ ◁ (β_ X₃ Y₁).hom ≫ (α_ X₂ Y₁ X₃).inv ≫ (β_ X₂ Y₁).hom ▷ X₃ ≫ (α_ Y₁ X₂ X₃).hom) ▷
                  (Y₂ ⊗ Y₃) ≫
              X₁ ◁ (α_ Y₁ (X₂ ⊗ X₃) (Y₂ ⊗ Y₃)).hom ≫ (α_ X₁ Y₁ ((X₂ ⊗ X₃) ⊗ Y₂ ⊗ Y₃)).inv) ≫
        (X₁ ⊗ Y₁) ◁
          ((α_ X₂ X₃ (Y₂ ⊗ Y₃)).hom ≫
            X₂ ◁ (α_ X₃ Y₂ Y₃).inv ≫ X₂ ◁ (β_ X₃ Y₂).hom ▷ Y₃ ≫ X₂ ◁ (α_ Y₂ X₃ Y₃).hom ≫ (α_ X₂ Y₂ (X₃ ⊗ Y₃)).inv)

Tactic:
monoidal

Result:
no goals