harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/MulAction.lean
theorem AddTorsor.connectedSpace : ConnectedSpace P :=
  { isPreconnected_univ

Proof state:
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ IsPreconnected Set.univ

Tactic:
convert
  isPreconnected_univ.image (Equiv.vaddConst (Classical.arbitrary P) : G → P)
    (continuous_id.vadd continuous_const).continuousOn

Result:
case h.e'_3
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ Set.univ = ⇑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ

Proof state:
case h.e'_3
G : Type u_1
P : Type u_2
inst✝⁵ : AddGroup G
inst✝⁴ : AddTorsor G P
inst✝³ : TopologicalSpace G
inst✝² : PreconnectedSpace G
inst✝¹ : TopologicalSpace P
inst✝ : ContinuousVAdd G P
⊢ Set.univ = ⇑(Equiv.vaddConst (Classical.arbitrary P)) '' Set.univ

Tactic:
rw [Set.image_univ, Equiv.range_eq_univ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem degree_C_mul_T_ite [DecidableEq R] (n : ℤ) (a : R) :
    degree (C a * T n) = if a = 0 then ⊥ else ↑n

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : DecidableEq R
n : ℤ
a : R
⊢ (C a * T n).degree = if a = 0 then ⊥ else ↑n

Tactic:
split_ifs with h <;>
  simp only [h, map_zero, zero_mul, degree_zero, degree_C_mul_T, Ne,
    not_false_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/LogBounds.lean
/-- Represent `log (1 + z)` as an integral over the unit interval -/
lemma log_eq_integral {z : ℂ} (hz : 1 + z ∈ slitPlane) :
    log (1 + z) = z * ∫ (t : ℝ) in (0 : ℝ)..1, (1 + t • z)⁻¹

Proof state:
case h.e'_2
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = log (1 + z) - log 1

Tactic:
simp only [log_one, sub_zero]

Result:
no goals

Proof state:
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = z * ∫ (t : ℝ) in 0 ..1, (1 + t • z)⁻¹

Tactic:
convert (integral_unitInterval_deriv_eq_sub (continuousOn_one_add_mul_inv hz)
  (fun _ ht ↦ hasDerivAt_log <|
    StarConvex.add_smul_mem starConvex_one_slitPlane hz ht.1 ht.2)).symm using 1

Result:
case h.e'_2
z : ℂ
hz : 1 + z ∈ slitPlane
⊢ log (1 + z) = log (1 + z) - log 1
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem liftOn₂_mk' {p : Sort*} (f : M → S → M → S → p) (H) (a c : M) (b d : S) :
    liftOn₂ ((monoidOf S).mk' a b) ((monoidOf S).mk' c d) f H = f a b c d

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
p : Sort u_4
f : M → ↥S → M → ↥S → p
H :
  ∀ {a a' : M} {b b' : ↥S} {c c' : M} {d d' : ↥S},
    (r S) (a, b) (a', b') → (r S) (c, d) (c', d') → f a b c d = f a' b' c' d'
a c : M
b d : ↥S
⊢ ((monoidOf S).mk' a b).liftOn₂ ((monoidOf S).mk' c d) f H = f a b c d

Tactic:
rw [← mk_eq_monoidOf_mk', liftOn₂_mk]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_mono : ∀ {a b : Associates α}, a ≤ b → a.factors ≤ b.factors
  | s, t, ⟨d, eq⟩ => by rw [eq, factors_mul]; exact le_add_of_nonneg_right bot_le

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ t.factors

Tactic:
rw [eq, factors_mul]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ s.factors + d.factors

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
s t : Associates α
d : Associates α
eq : t = s * d
⊢ s.factors ≤ s.factors + d.factors

Tactic:
exact le_add_of_nonneg_right bot_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem atLeastTwo_true_mid    : atLeastTwo a true c  = (a || c)

Proof state:
a c : Bool
⊢ a.atLeastTwo true c = (a || c)

Tactic:
cases a <;> cases c <;> simp [atLeastTwo]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_node3L (l : Ordnode α) (x : α) (m : Ordnode α) (y : α) (r : Ordnode α) :
    dual (node3L l x m y r) = node3R (dual r) y (dual m) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ (l.node3L x m y r).dual = r.dual.node3R y m.dual x l.dual

Tactic:
simp [node3L, node3R, dual_node', add_comm]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem getElem_eq_getElem_rotate (l : List α) (n : ℕ) (k : Nat) (hk : k < l.length) :
    l[k] = ((l.rotate n)[(l.length - n % l.length + k) % l.length]'
      ((Nat.mod_lt _ (k.zero_le.trans_lt hk)).trans_eq (length_rotate _ _).symm))

Proof state:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = l[((l.length - n % l.length + k) % l.length + n) % l.length]

Tactic:
refine congr_arg l.get (Fin.eq_of_val_eq ?_)

Result:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ ↑⟨k, hk⟩ = ↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩

Proof state:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length

Tactic:
rw [← add_mod_mod, Nat.add_right_comm, Nat.sub_add_cancel, add_mod_left, mod_eq_of_lt]

Result:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Proof state:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = (l.rotate n)[(l.length - n % l.length + k) % l.length]

Tactic:
rw [getElem_rotate]

Result:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ l[k] = l[((l.length - n % l.length + k) % l.length + n) % l.length]

Proof state:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ ↑⟨k, hk⟩ = ↑⟨((l.length - n % l.length + k) % l.length + n) % l.length, ⋯⟩

Tactic:
simp only [mod_add_mod]

Result:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k = (l.length - n % l.length + k + n) % l.length

Proof state:
α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ k < l.length

α : Type u
l : List α
n k : ℕ
hk : k < l.length
⊢ n % l.length ≤ l.length

Tactic:
exacts [hk, (mod_lt _ (k.zero_le.trans_lt hk)).le]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MapIdx.lean
theorem getLast?_mapIdx {l : List α} {f : Nat → α → β} :
    (mapIdx f l).getLast? = (getLast? l).map (f (l.length - 1))

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : Nat → α → β
⊢ (mapIdx f l).getLast? = Option.map (f (l.length - 1)) l.getLast?

Tactic:
cases l

Result:
case nil
α : Type u_1
β : Type u_2
f : Nat → α → β
⊢ (mapIdx f []).getLast? = Option.map (f ([].length - 1)) [].getLast?

case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
⊢ (mapIdx f (head✝ :: tail✝)).getLast? = Option.map (f ((head✝ :: tail✝).length - 1)) (head✝ :: tail✝).getLast?

Proof state:
case cons
α : Type u_1
β : Type u_2
f : Nat → α → β
head✝ : α
tail✝ : List α
⊢ (mapIdx f (head✝ :: tail✝)).getLast? = Option.map (f ((head✝ :: tail✝).length - 1)) (head✝ :: tail✝).getLast?

Tactic:
rw [getLast?_eq_getLast, getLast?_eq_getLast, getLast_mapIdx] <;> simp

Result:
no goals

Proof state:
case nil
α : Type u_1
β : Type u_2
f : Nat → α → β
⊢ (mapIdx f []).getLast? = Option.map (f ([].length - 1)) [].getLast?

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_monomial (h : r ≠ 0) : (monomial s r).vars = s.support

Proof state:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).vars = s.support

Tactic:
rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst✝ : CommSemiring R
h : r ≠ 0
⊢ ((monomial s) r).vars = s.support

Tactic:
classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem unattach_attachWith {p : α → Prop} {l : Array α}
    {H : ∀ a ∈ l, p a} :
    (l.attachWith p H).unattach = l

Proof state:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ ({ toList := toList✝ }.attachWith p H).unattach = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ (l.attachWith p H).unattach = l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ ({ toList := toList✝ }.attachWith p H).unattach = { toList := toList✝ }
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_inter' (a : α) (s t : Set α) : 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t

Tactic:
rw [← inf_principal, inf_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝[s ∩ t] a = 𝓝[s] a ⊓ 𝓟 t

Tactic:
delta nhdsWithin

Result:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s t : Set α
⊢ 𝓝 a ⊓ 𝓟 (s ∩ t) = 𝓝 a ⊓ 𝓟 s ⊓ 𝓟 t
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem sameCycle_zpow_right {n : ℤ} : SameCycle f x ((f ^ n) y) ↔ SameCycle f x y

Proof state:
α : Type u_2
f : Perm α
x y : α
n : ℤ
⊢ f.SameCycle x ((f ^ n) y) ↔ f.SameCycle x y

Tactic:
rw [sameCycle_comm, sameCycle_zpow_left, sameCycle_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Deriv.lean
theorem Complex.logDeriv_cos : logDeriv (Complex.cos) = -Complex.tan

Proof state:
case h
x✝ : ℂ
⊢ logDeriv cos x✝ = (-tan) x✝

Tactic:
rw [logDeriv, Complex.deriv_cos', Pi.div_apply, Pi.neg_apply, Complex.tan, neg_div]

Result:
no goals

Proof state:
⊢ logDeriv cos = -tan

Tactic:
ext

Result:
case h
x✝ : ℂ
⊢ logDeriv cos x✝ = (-tan) x✝
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem QInfty_f_comp_PInfty_f (n : ℕ) : (QInfty.f n : X _⦋n⦌ ⟶ _) ≫ PInfty.f n = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (𝟙 K[X] - PInfty).f n ≫ PInfty.f n = 0

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, sub_comp, id_comp,
  PInfty_f_idem, sub_self]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ QInfty.f n ≫ PInfty.f n = 0

Tactic:
dsimp only [QInfty]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (𝟙 K[X] - PInfty).f n ≫ PInfty.f n = 0
-- Mathlib/MeasureTheory/Function/ContinuousMapDense.lean
theorem Integrable.exists_boundedContinuous_lintegral_sub_le [μ.WeaklyRegular] {f : α → E}
    (hf : Integrable f μ) {ε : ℝ≥0∞} (hε : ε ≠ 0) :
    ∃ g : α →ᵇ E, ∫⁻ x, ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Integrable g μ

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
hf : Integrable f μ
ε : ℝ≥0∞
hε : ε ≠ 0
⊢ ∃ g, ∫⁻ (x : α), ‖f x - g x‖ₑ ∂μ ≤ ε ∧ Integrable (⇑g) μ

Tactic:
simp only [← memLp_one_iff_integrable, ← eLpNorm_one_eq_lintegral_enorm] at hf ⊢

Result:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g, eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ MemLp (⇑g) 1 μ

Proof state:
α : Type u_1
inst✝⁶ : TopologicalSpace α
inst✝⁵ : NormalSpace α
inst✝⁴ : MeasurableSpace α
inst✝³ : BorelSpace α
E : Type u_2
inst✝² : NormedAddCommGroup E
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : μ.WeaklyRegular
f : α → E
ε : ℝ≥0∞
hε : ε ≠ 0
hf : MemLp f 1 μ
⊢ ∃ g, eLpNorm (fun x => f x - g x) 1 μ ≤ ε ∧ MemLp (⇑g) 1 μ

Tactic:
exact hf.exists_boundedContinuous_eLpNorm_sub_le ENNReal.one_ne_top hε

Result:
no goals
-- Mathlib/Topology/UniformSpace/Cauchy.lean
theorem Cauchy.ultrafilter_of {l : Filter α} (h : Cauchy l) :
    Cauchy (@Ultrafilter.of _ l h.1 : Filter α)

Proof state:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this✝ : l.NeBot
this : ↑(Ultrafilter.of l) ≤ l
⊢ Cauchy ↑(Ultrafilter.of l)

Tactic:
exact ⟨Ultrafilter.neBot _, (Filter.prod_mono this this).trans h.2⟩

Result:
no goals

Proof state:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
⊢ Cauchy ↑(Ultrafilter.of l)

Tactic:
haveI := h.1

Result:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this : l.NeBot
⊢ Cauchy ↑(Ultrafilter.of l)

Proof state:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this : l.NeBot
⊢ Cauchy ↑(Ultrafilter.of l)

Tactic:
have := Ultrafilter.of_le l

Result:
α : Type u
uniformSpace : UniformSpace α
l : Filter α
h : Cauchy l
this✝ : l.NeBot
this : ↑(Ultrafilter.of l) ≤ l
⊢ Cauchy ↑(Ultrafilter.of l)
-- Mathlib/Data/List/Indexes.lean
theorem foldrIdxM_eq_foldrM_enum {β} (f : ℕ → α → β → m β) (b : β) (as : List α) [LawfulMonad m] :
    foldrIdxM f b as = foldrM (uncurry f) b (enum as)

Proof state:
α : Type u
m : Type u → Type v
inst✝¹ : Monad m
β : Type u
f : ℕ → α → β → m β
b : β
as : List α
inst✝ : LawfulMonad m
⊢ foldrIdxM f b as = foldrM (uncurry f) b as.enum

Tactic:
simp (config := { unfoldPartialApp := true }) only [foldrIdxM, foldrM_eq_foldr,
  foldrIdx_eq_foldr_enum, uncurry]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem isCongruenceSubgroup_trans (H K : Subgroup SL(2, ℤ)) (h : H ≤ K)
    (h2 : IsCongruenceSubgroup H) : IsCongruenceSubgroup K

Proof state:
case intro
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Γ(↑N) ≤ H
⊢ IsCongruenceSubgroup K

Tactic:
exact ⟨N, le_trans hN h⟩

Result:
no goals

Proof state:
H K : Subgroup SL(2, ℤ)
h : H ≤ K
h2 : IsCongruenceSubgroup H
⊢ IsCongruenceSubgroup K

Tactic:
obtain ⟨N, hN⟩ := h2

Result:
case intro
H K : Subgroup SL(2, ℤ)
h : H ≤ K
N : ℕ+
hN : Γ(↑N) ≤ H
⊢ IsCongruenceSubgroup K
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem Integrable.sub {f g : α → β} (hf : Integrable f μ) (hg : Integrable g μ) :
    Integrable (f - g) μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f g : α → β
hf : Integrable f μ
hg : Integrable g μ
⊢ Integrable (f - g) μ

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/Geometry/RingedSpace/OpenImmersion.lean
theorem pullback_snd_isIso_of_range_subset (H' : Set.range g.base ⊆ Set.range f.base) :
    IsIso (pullback.snd f g)

Proof state:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (pullback.snd f g)))

Tactic:
erw [← PreservesPullback.iso_hom_snd
    (LocallyRingedSpace.forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g]

Result:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso
    ((PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g).hom ≫
      pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))

Proof state:
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (pullback.snd f g)

Tactic:
apply (config := {allowSynthFailures := true}) Functor.ReflectsIsomorphisms.reflects
  (F := LocallyRingedSpace.forgetToSheafedSpace)

Result:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (forgetToSheafedSpace.map (pullback.snd f g))

Proof state:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (forgetToSheafedSpace.map (pullback.snd f g))

Tactic:
apply (config := {allowSynthFailures := true}) Functor.ReflectsIsomorphisms.reflects
  (F := SheafedSpace.forgetToPresheafedSpace)

Result:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso (SheafedSpace.forgetToPresheafedSpace.map (forgetToSheafedSpace.map (pullback.snd f g)))

Proof state:
case inst
X Y Z : LocallyRingedSpace
f : X ⟶ Z
g : Y ⟶ Z
H : IsOpenImmersion f
H' : Set.range ⇑(ConcreteCategory.hom g.base) ⊆ Set.range ⇑(ConcreteCategory.hom f.base)
⊢ IsIso
    ((PreservesPullback.iso (forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace) f g).hom ≫
      pullback.snd ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map f)
        ((forgetToSheafedSpace ⋙ SheafedSpace.forgetToPresheafedSpace).map g))

Tactic:
exact IsIso.comp_isIso' inferInstance <|
  PresheafedSpace.IsOpenImmersion.pullback_snd_isIso_of_range_subset _ _ H'

Result:
no goals
-- Mathlib/GroupTheory/SchurZassenhaus.lean
theorem step7 : IsCommutative N

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
this : Nontrivial ↥N
⊢ N.IsCommutative

Tactic:
haveI : Fact (Nat.card N).minFac.Prime := ⟨step4 h1 h3⟩

Result:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
this✝ : Nontrivial ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ N.IsCommutative

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
this✝ : Nontrivial ↥N
this : Fact (Nat.Prime (Nat.card ↥N).minFac)
⊢ N.IsCommutative

Tactic:
exact
  ⟨⟨fun g h => ((eq_top_iff.mp ((step3 h1 h2 h3 (center N)).resolve_left
    (step6 h1 h2 h3).bot_lt_center.ne') (mem_top h)).comm g).symm⟩⟩

Result:
no goals

Proof state:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
⊢ N.IsCommutative

Tactic:
haveI := N.bot_or_nontrivial.resolve_left (step0 h1 h3)

Result:
G : Type u
inst✝² : Group G
N : Subgroup G
inst✝¹ : N.Normal
h1 : (Nat.card ↥N).Coprime N.index
h2 :
  ∀ (G' : Type u) [inst : Group G'] [inst_1 : Finite G'],
    Nat.card G' < Nat.card G →
      ∀ {N' : Subgroup G'} [inst_2 : N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H'
h3 : ∀ (H : Subgroup G), ¬N.IsComplement' H
inst✝ : Finite G
this : Nontrivial ↥N
⊢ N.IsCommutative
-- Mathlib/Data/NNRat/Defs.lean
@[simp] lemma mul_den_eq_num (q : ℚ≥0) : q * q.den = q.num

Proof state:
q : ℚ≥0
⊢ q * ↑q.den = ↑q.num

Tactic:
ext

Result:
case a
q : ℚ≥0
⊢ ↑(q * ↑q.den) = ↑↑q.num

Proof state:
case a
q : ℚ≥0
⊢ ↑q * ↑q.den = ↑q.num

Tactic:
rw [← Int.cast_natCast, ← den_coe, ← Int.cast_natCast q.num, ← num_coe]

Result:
case a
q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑(↑q).num

Proof state:
case a
q : ℚ≥0
⊢ ↑(q * ↑q.den) = ↑↑q.num

Tactic:
push_cast

Result:
case a
q : ℚ≥0
⊢ ↑q * ↑q.den = ↑q.num

Proof state:
case a
q : ℚ≥0
⊢ ↑q * ↑↑(↑q).den = ↑(↑q).num

Tactic:
exact Rat.mul_den_eq_num _

Result:
no goals
-- Mathlib/Analysis/Fourier/FourierTransform.lean
lemma fourierIntegralInv_comm (f : V → E) :
    𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f)

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕 fun x => 𝓕 f (-x)

Tactic:
simp_rw [← fourierIntegralInv_eq_fourierIntegral_neg]

Result:
no goals

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕⁻ (𝓕 f)

Tactic:
conv_rhs => rw [fourierIntegralInv_eq_fourierIntegral_comp_neg]

Result:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
V : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MeasurableSpace V
inst✝¹ : BorelSpace V
inst✝ : FiniteDimensional ℝ V
f : V → E
⊢ 𝓕 (𝓕⁻ f) = 𝓕 fun x => 𝓕 f (-x)
-- Mathlib/Dynamics/Ergodic/Action/OfMinimal.lean
theorem aeconst_of_dense_aestabilizer_smul (hsm : NullMeasurableSet s μ)
    (hd : Dense (MulAction.aestabilizer G μ s : Set G)) : EventuallyConst s (ae μ) :=
  aeconst_of_dense_setOf_preimage_smul_ae hsm <| (hd.preimage (isOpenMap_inv _)).mono fun g hg ↦ by
    simpa only [preimage_smul] using hg

Proof state:
G : Type u_1
inst✝¹¹ : Group G
inst✝¹⁰ : TopologicalSpace G
inst✝⁹ : ContinuousInv G
X : Type u_2
inst✝⁸ : TopologicalSpace X
inst✝⁷ : R1Space X
inst✝⁶ : MeasurableSpace X
inst✝⁵ : BorelSpace X
inst✝⁴ : MulAction G X
inst✝³ : ContinuousSMul G X
μ : Measure X
inst✝² : IsFiniteMeasure μ
inst✝¹ : μ.InnerRegular
inst✝ : ErgodicSMul G X μ
s : Set X
hsm : NullMeasurableSet s μ
hd : Dense ↑(MulAction.aestabilizer G μ s)
g : G
hg : g ∈ Inv.inv ⁻¹' ↑(MulAction.aestabilizer G μ s)
⊢ g ∈ {g | (fun x => g • x) ⁻¹' s =ᶠ[ae μ] s}

Tactic:
simpa only [preimage_smul] using hg

Result:
no goals