harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem denom_ne_zero (g : GL(2, ℝ)⁺) (z : ℍ) : denom g z ≠ 0

Proof state:
case inr
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
hz : z.im = 0
⊢ False

Tactic:
exact z.prop.ne' hz

Result:
no goals

Proof state:
case inl
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
hg : ↑↑g 1 0 = 0
⊢ False

Tactic:
simp only [hg, Complex.ofReal_zero, denom, zero_mul, zero_add, Complex.ofReal_eq_zero] at H

Result:
case inl
g : ↥GL(2, ℝ)⁺
z : ℍ
DET : 0 < (↑↑g).det
hg : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
⊢ False

Tactic:
have DET := (mem_glpos _).1 g.prop

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < ↑(GeneralLinearGroup.det ↑g)
⊢ False

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
⊢ ↑↑g 1 0 = 0 ∨ z.im = 0

Tactic:
simpa [num, denom] using congr_arg Complex.im H

Result:
no goals

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
⊢ False

Tactic:
obtain hg | hz : g 1 0 = 0 ∨ z.im = 0 := by simpa [num, denom] using congr_arg Complex.im H

Result:
case inl
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
hg : ↑↑g 1 0 = 0
⊢ False

case inr
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
hz : z.im = 0
⊢ False

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < ↑(GeneralLinearGroup.det ↑g)
⊢ False

Tactic:
simp only [GeneralLinearGroup.val_det_apply] at DET

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
DET : 0 < (↑↑g).det
⊢ False

Proof state:
case inl
g : ↥GL(2, ℝ)⁺
z : ℍ
DET : 0 < (↑↑g).det
hg : ↑↑g 1 0 = 0
H : ↑↑g 1 1 = 0
⊢ False

Tactic:
simp only [Matrix.det_fin_two g.1.1, H, hg, mul_zero, sub_zero, lt_self_iff_false] at DET

Result:
no goals

Proof state:
g : ↥GL(2, ℝ)⁺
z : ℍ
⊢ denom g z ≠ 0

Tactic:
intro H

Result:
g : ↥GL(2, ℝ)⁺
z : ℍ
H : denom g z = 0
⊢ False
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem isPreirreducible_iff_subsingleton [T2Space X] {S : Set X} :
    IsPreirreducible S ↔ S.Subsingleton

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
⊢ IsPreirreducible S ↔ S.Subsingleton

Tactic:
refine ⟨fun h x hx y hy => ?_, Set.Subsingleton.isPreirreducible⟩

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ x = y

Proof state:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : ¬x = y
U V : Set X
hU : IsOpen U
hV : IsOpen V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False

Tactic:
exact ((h U V hU hV ⟨x, hx, hxU⟩ ⟨y, hy, hyV⟩).mono inter_subset_right).not_disjoint h'

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : ¬x = y
⊢ False

Tactic:
obtain ⟨U, V, hU, hV, hxU, hyV, h'⟩ := t2_separation e

Result:
case intro.intro.intro.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : ¬x = y
U V : Set X
hU : IsOpen U
hV : IsOpen V
hxU : x ∈ U
hyV : y ∈ V
h' : Disjoint U V
⊢ False

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
⊢ x = y

Tactic:
by_contra e

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
S : Set X
h : IsPreirreducible S
x : X
hx : x ∈ S
y : X
hy : y ∈ S
e : ¬x = y
⊢ False
-- Mathlib/Analysis/Complex/Tietze.lean
theorem exists_norm_eq_restrict_eq (f : s →ᵇ E) :
    ∃ g : X →ᵇ E, ‖g‖ = ‖f‖ ∧ g.restrict s = f

Proof state:
case neg.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
⊢ ∃ g, ‖g‖ = ‖f‖ ∧ g.restrict s = f

Tactic:
refine ⟨g', ?_, by ext x; congrm($(hg) x)⟩

Result:
case neg.intro.intro
X : Type u
inst✝⁵ : TopologicalSpace X
inst✝⁴ : NormalSpace X
s : Set X
hs : IsClosed s
𝕜 : Type v
inst✝³ : RCLike 𝕜
E : Type w
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : FiniteDimensional 𝕜 E
f : ↑s →ᵇ E
hf : ¬‖f‖ = 0
this : TietzeExtension ↑(Metric.closedBall 0 ‖f‖)
hf' : ∀ (x : ↑s), f x ∈ Metric.closedBall 0 ‖f‖
g : C(X, E)
hg : ContinuousMap.restrict s g = ↑f
hg_mem : ∀ (x : X), ‖g x‖ ≤ ‖f‖
g' : X →ᵇ E := ofNormedAddCommGroup ⇑g ⋯ ‖f‖ hg_mem
⊢ ‖g'‖ = ‖f‖
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
    (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n)

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x ^^^ y) <<< n).getLsbD i = (x <<< n ^^^ y <<< n).getLsbD i

Tactic:
simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) ^^ y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) ^^ !decide (i < n) && y.getLsbD (i - n))

Proof state:
w : Nat
x y : BitVec w
n : Nat
⊢ (x ^^^ y) <<< n = x <<< n ^^^ y <<< n

Tactic:
ext i h

Result:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ ((x ^^^ y) <<< n).getLsbD i = (x <<< n ^^^ y <<< n).getLsbD i

Proof state:
case pred
w : Nat
x y : BitVec w
n i : Nat
h : i < w
⊢ (!decide (i < n) && (x.getLsbD (i - n) ^^ y.getLsbD (i - n))) =
    (!decide (i < n) && x.getLsbD (i - n) ^^ !decide (i < n) && y.getLsbD (i - n))

Tactic:
by_cases h' : i < n <;> simp [h']

Result:
no goals
-- Mathlib/Analysis/MeanInequalitiesPow.lean
theorem rpow_arith_mean_le_arith_mean2_rpow (w₁ w₂ z₁ z₂ : ℝ≥0∞) (hw' : w₁ + w₂ = 1) {p : ℝ}
    (hp : 1 ≤ p) : (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Proof state:
case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
simpa [Fin.sum_univ_succ] using h

Result:
no goals

Proof state:
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

Tactic:
have h := rpow_arith_mean_le_arith_mean_rpow univ ![w₁, w₂] ![z₁, z₂] ?_ hp

Result:
case refine_2
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
h :
  (∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i) ^ p ≤
    ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i * ![z₁, z₂] i ^ p
⊢ (w₁ * z₁ + w₂ * z₂) ^ p ≤ w₁ * z₁ ^ p + w₂ * z₂ ^ p

case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1

Proof state:
case refine_1
w₁ w₂ z₁ z₂ : ℝ≥0∞
hw' : w₁ + w₂ = 1
p : ℝ
hp : 1 ≤ p
⊢ ∑ i : Fin (Nat.succ 0).succ, ![w₁, w₂] i = 1

Tactic:
simp [hw', Fin.sum_univ_succ]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem single_eq_of_sigma_eq {i j} {xi : β i} {xj : β j} (h : (⟨i, xi⟩ : Sigma β) = ⟨j, xj⟩) :
    DFinsupp.single i xi = DFinsupp.single j xj

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : ⟨i, xi⟩ = ⟨j, xj⟩
⊢ single i xi = single j xj

Tactic:
cases h

Result:
case refl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = single i xi

Proof state:
case refl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = single i xi

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Sub.lean
theorem sub_add_cancel_of_le [IsFiniteMeasure ν] (h₁ : ν ≤ μ) : μ - ν + ν = μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
h₁ : ν ≤ μ
s : Set α
h_s_meas : MeasurableSet s
⊢ (μ - ν + ν) s = μ s

Tactic:
rw [add_apply, sub_apply h_s_meas h₁, tsub_add_cancel_of_le (h₁ s)]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
h₁ : ν ≤ μ
⊢ μ - ν + ν = μ

Tactic:
ext1 s h_s_meas

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : IsFiniteMeasure ν
h₁ : ν ≤ μ
s : Set α
h_s_meas : MeasurableSet s
⊢ (μ - ν + ν) s = μ s
-- Mathlib/SetTheory/Game/PGame.lean
theorem zero_lf_star : 0 ⧏ star

Proof state:
case h

⊢ ∀ (j : (star.moveLeft default).RightMoves), 0 ⧏ (star.moveLeft default).moveRight j

Tactic:
rintro ⟨⟩

Result:
no goals

Proof state:
⊢ 0 ⧏ star

Tactic:
rw [zero_lf]

Result:
⊢ ∃ i, ∀ (j : (star.moveLeft i).RightMoves), 0 ⧏ (star.moveLeft i).moveRight j

Proof state:
⊢ ∃ i, ∀ (j : (star.moveLeft i).RightMoves), 0 ⧏ (star.moveLeft i).moveRight j

Tactic:
use default

Result:
case h

⊢ ∀ (j : (star.moveLeft default).RightMoves), 0 ⧏ (star.moveLeft default).moveRight j
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b

Proof state:
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ b * a

Tactic:
exact mul_pos IH a0

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b

Tactic:
induction b using limitRecOn with
| H₁ => exact h0
| H₂ b IH =>
  rw [opow_succ]
  exact mul_pos IH a0
| H₃ b l _ =>
  exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ b

Tactic:
have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one]

Result:
a b : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ b

Proof state:
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ succ b

Tactic:
rw [opow_succ]

Result:
case H₂
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
IH : 0 < a ^ b
⊢ 0 < a ^ b * a

Proof state:
case H₃
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
b : Ordinal.{u_1}
l : b.IsLimit
a✝ : ∀ o' < b, 0 < a ^ o'
⊢ 0 < a ^ b

Tactic:
exact (lt_opow_of_limit (Ordinal.pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩

Result:
no goals

Proof state:
case H₁
a : Ordinal.{u_1}
a0 : 0 < a
h0 : 0 < a ^ 0
⊢ 0 < a ^ 0

Tactic:
exact h0

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
a0 : 0 < a
⊢ 0 < a ^ 0

Tactic:
simp only [opow_zero, zero_lt_one]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Injective/Preserves.lean
theorem Functor.preservesMonomorphisms_of_adjunction_of_preservesInjectiveObjects
    [EnoughInjectives D] {F : C ⥤ D} {G : D ⥤ C} (adj : F ⊣ G) [G.PreservesInjectiveObjects] :
    F.PreservesMonomorphisms where
  preserves {X Y} f _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ Mono (F.map f)

Tactic:
suffices ∃ h, F.map f ≫ h = Injective.ι (F.obj X) from mono_of_mono_fac this.choose_spec

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
this : Injective (G.obj (Injective.under (F.obj X)))
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)

Tactic:
exact ⟨F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι _)) f) ≫
  adj.counit.app (Injective.under (F.obj X)), by simp [← Functor.map_comp_assoc]⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
this : Injective (G.obj (Injective.under (F.obj X)))
⊢ F.map f ≫
      F.map (Injective.factorThru (adj.unit.app X ≫ G.map (Injective.ι (F.obj X))) f) ≫
        adj.counit.app (Injective.under (F.obj X)) =
    Injective.ι (F.obj X)

Tactic:
simp [← Functor.map_comp_assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)

Tactic:
have : Injective (G.obj (Injective.under (F.obj X))) := G.injective_obj _

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : EnoughInjectives D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
inst✝ : G.PreservesInjectiveObjects
X Y : C
f : X ⟶ Y
x✝ : Mono f
this : Injective (G.obj (Injective.under (F.obj X)))
⊢ ∃ h, F.map f ≫ h = Injective.ι (F.obj X)
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem exists_closed_nhds_one_inv_eq_mul_subset {U : Set G} (hU : U ∈ 𝓝 1) :
    ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed W
hW : W ⊆ V
⊢ (W ∩ W⁻¹)⁻¹ = W ∩ W⁻¹

Tactic:
simp [inter_comm]

Result:
no goals

Proof state:
case intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
⊢ ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_mem_nhds_isClosed_subset (V_open.mem_nhds V_mem) with ⟨W, W_mem, W_closed, hW⟩

Result:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed W
hW : W ⊆ V
⊢ ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed W
hW : W ⊆ V
⊢ W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U

Tactic:
calc
W ∩ W⁻¹ * (W ∩ W⁻¹)
  ⊆ W * W := mul_subset_mul inter_subset_left inter_subset_left
_ ⊆ V * V := mul_subset_mul hW hW
_ ⊆ U := hV

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed W
hW : W ⊆ V
⊢ ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
refine ⟨W ∩ W⁻¹, Filter.inter_mem W_mem (inv_mem_nhds_one G W_mem), W_closed.inter W_closed.inv,
  by simp [inter_comm], ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
W : Set G
W_mem : W ∈ 𝓝 1
W_closed : IsClosed W
hW : W ⊆ V
⊢ W ∩ W⁻¹ * (W ∩ W⁻¹) ⊆ U

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
⊢ ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U

Tactic:
rcases exists_open_nhds_one_mul_subset hU with ⟨V, V_open, V_mem, hV⟩

Result:
case intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
U : Set G
hU : U ∈ 𝓝 1
V : Set G
V_open : IsOpen V
V_mem : 1 ∈ V
hV : V * V ⊆ U
⊢ ∃ V ∈ 𝓝 1, IsClosed V ∧ V⁻¹ = V ∧ V * V ⊆ U
-- Mathlib/CategoryTheory/Limits/Shapes/KernelPair.lean
theorem of_isIso_of_mono [IsIso a] [Mono f] : IsKernelPair f a a

Proof state:
case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f

Tactic:
convert (IsPullback.of_horiz_isIso ⟨(rfl : a ≫ 𝟙 X = _ )⟩).paste_vert (IsKernelPair.id_of_mono f)

Result:
case h.e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f

Proof state:
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsKernelPair f a a

Tactic:
change IsPullback _ _ _ _

Result:
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ IsPullback a a f f

Proof state:
case h.e'_8
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ a = a ≫ 𝟙 X

case h.e'_9
C : Type u
inst✝² : Category.{v, u} C
R X Y : C
f : X ⟶ Y
a : R ⟶ X
inst✝¹ : IsIso a
inst✝ : Mono f
⊢ f = 𝟙 X ≫ f

Tactic:
all_goals { simp }

Result:
no goals
-- Mathlib/RingTheory/FreeCommRing.lean
theorem isSupported_int {i : ℤ} {s : Set α} : IsSupported (↑i) s :=
  Int.induction_on i isSupported_zero
    (fun i hi => by rw [Int.cast_add, Int.cast_one]; exact isSupported_add hi isSupported_one)
    fun i hi => by rw [Int.cast_sub, Int.cast_one]; exact isSupported_sub hi isSupported_one

Proof state:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i - 1)).IsSupported s

Tactic:
rw [Int.cast_sub, Int.cast_one]

Result:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i) - 1).IsSupported s

Proof state:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑(-↑i)).IsSupported s
⊢ (↑(-↑i) - 1).IsSupported s

Tactic:
exact isSupported_sub hi isSupported_one

Result:
no goals

Proof state:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑(↑i + 1)).IsSupported s

Tactic:
rw [Int.cast_add, Int.cast_one]

Result:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑↑i + 1).IsSupported s

Proof state:
α : Type u
i✝ : ℤ
s : Set α
i : ℕ
hi : (↑↑i).IsSupported s
⊢ (↑↑i + 1).IsSupported s

Tactic:
exact isSupported_add hi isSupported_one

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_append_left {l : List α} (w : l ++ l' ≠ []) (h : l' = []) :
    (l ++ l').getLast w = l.getLast (by simp_all)

Proof state:
α : Type u_1
l' l : List α
w : l ++ l' ≠ []
h : l' = []
⊢ (l ++ l').getLast w = l.getLast ⋯

Tactic:
rw [getLast_append, dif_pos (by simp_all)]

Result:
no goals

Proof state:
α : Type u_1
l' l : List α
w : l ++ l' ≠ []
h : l' = []
⊢ l'.isEmpty = true

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.316033
l' l : List α
w : l ++ l' ≠ []
h : l' = []
⊢ l ≠ []

Tactic:
simp_all

Result:
no goals
-- Mathlib/Order/Interval/Set/SurjOn.lean
theorem surjOn_Ici_of_monotone_surjective (h_mono : Monotone f) (h_surj : Function.Surjective f)
    (a : α) : SurjOn f (Ici a) (Ici (f a))

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})

Tactic:
exact
  (surjOn_Ioi_of_monotone_surjective h_mono h_surj a).union_union
    (@image_singleton _ _ f a ▸ surjOn_image _ _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ici a) (Ici (f a))

Tactic:
rw [← Ioi_union_left, ← Ioi_union_left]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
h_mono : Monotone f
h_surj : Surjective f
a : α
⊢ SurjOn f (Ioi a ∪ {a}) (Ioi (f a) ∪ {f a})
-- Mathlib/CategoryTheory/Generator/Basic.lean
theorem HasSeparator.hasCoseparator_of_hasSeparator_op [h : HasSeparator Cᵒᵖ] :
    HasCoseparator C

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
h : HasSeparator Cᵒᵖ
⊢ HasCoseparator C

Tactic:
simp_all

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem hasMFDerivWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x

Tactic:
exact extChartAt_preimage_mem_nhdsWithin h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ HasMFDerivWithinAt I I' f (s ∩ t) x f' ↔ HasMFDerivWithinAt I I' f s x f'

Tactic:
rw [HasMFDerivWithinAt, HasMFDerivWithinAt, extChartAt_preimage_inter_eq,
  hasFDerivWithinAt_inter', continuousWithinAt_inter' h]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
f' : TangentSpace I x →L[𝕜] TangentSpace I' (f x)
h : t ∈ 𝓝[s] x
⊢ ↑(extChartAt I x).symm ⁻¹' t ∈ 𝓝[↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I] ↑(extChartAt I x) x