harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Equiv/TransferInstance.lean
/-- Any finite group in universe `u` is equivalent to some finite group in universe `v`. -/
lemma exists_type_univ_nonempty_mulEquiv (G : Type u) [Group G] [Finite G] :
    ∃ (G' : Type v) (_ : Group G') (_ : Fintype G'), Nonempty (G ≃* G')

Proof state:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
let f : Fin n ≃ ULift (Fin n) := Equiv.ulift.symm

Result:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Proof state:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.101936, 0} (Fin n) := e✝.trans f
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
letI groupH : Group (ULift (Fin n)) := e.symm.group

Result:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.101936, 0} (Fin n) := e✝.trans f
groupH : Group (ULift.{?u.101936, 0} (Fin n)) := e.symm.group
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Proof state:
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin G

Result:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Proof state:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
let e : G ≃ ULift (Fin n) := e.trans f

Result:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.101936, 0} (Fin n) := e✝.trans f
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Proof state:
case intro.intro
G : Type u
inst✝¹ : Group G
inst✝ : Finite G
n : ℕ
e✝ : G ≃ Fin n
f : Fin n ≃ ULift.{?u.101936, 0} (Fin n) := Equiv.ulift.symm
e : G ≃ ULift.{?u.101936, 0} (Fin n) := e✝.trans f
groupH : Group (ULift.{?u.101936, 0} (Fin n)) := e.symm.group
⊢ ∃ G' x x_1, Nonempty (G ≃* G')

Tactic:
exact ⟨ULift (Fin n), groupH, inferInstance, ⟨MulEquiv.symm <| e.symm.mulEquiv⟩⟩

Result:
no goals
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem isLocallySurjective_iff_range_sheafify_eq_top {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
    IsLocallySurjective J f ↔ (Subpresheaf.range (whiskerRight f (forget A))).sheafify J = ⊤

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight f (forget A))) = ⊤

Tactic:
simp only [Subpresheaf.ext_iff, funext_iff, Set.ext_iff, Subpresheaf.top_obj,
  Set.top_eq_univ, Set.mem_univ, iff_true]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔
    ∀ (x : Cᵒᵖ) (x_1 : (G ⋙ forget A).obj x),
      x_1 ∈ (Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight f (forget A)))).obj x

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔
    ∀ (x : Cᵒᵖ) (x_1 : (G ⋙ forget A).obj x),
      x_1 ∈ (Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight f (forget A)))).obj x

Tactic:
exact ⟨fun H _ => H.imageSieve_mem, fun H => ⟨H _⟩⟩

Result:
no goals
-- Mathlib/Data/Nat/Factors.lean
theorem prod_primeFactorsList : ∀ {n}, n ≠ 0 → List.prod (primeFactorsList n) = n
  | 0 => by simp
  | 1 => by simp
  | k + 2 => fun _ =>
    let m := minFac (k + 2)
    have : (k + 2) / m < (k + 2) := factors_lemma
    show (primeFactorsList (k + 2)).prod = (k + 2) by
      have h₁ : (k + 2) / m ≠ 0 := fun h => by
        have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
        rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this
      rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
        Nat.mul_div_cancel' (minFac_dvd _)]

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).primeFactorsList.prod = k + 2

Tactic:
rw [primeFactorsList, List.prod_cons, prod_primeFactorsList h₁,
  Nat.mul_div_cancel' (minFac_dvd _)]

Result:
no goals

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ k + 2 ≠ 0

Tactic:
simp

Result:
no goals

Proof state:
⊢ 1 ≠ 0 → (primeFactorsList 1).prod = 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ 0 ≠ 0 → (primeFactorsList 0).prod = 0

Tactic:
simp

Result:
no goals

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h : (k + 2) / m = 0
⊢ False

Tactic:
have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h

Result:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False

Tactic:
exact (show k + 2 ≠ 0 by simp) this

Result:
no goals

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0 * m
⊢ False

Tactic:
rw [zero_mul] at this

Result:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this✝ : (k + 2) / m < k + 2
h : (k + 2) / m = 0
this : k + 2 = 0
⊢ False

Proof state:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
⊢ (k + 2).primeFactorsList.prod = k + 2

Tactic:
have h₁ : (k + 2) / m ≠ 0 := fun h => by
  have : (k + 2) = 0 * m := (Nat.div_eq_iff_eq_mul_left (minFac_pos _) (minFac_dvd _)).1 h
  rw [zero_mul] at this; exact (show k + 2 ≠ 0 by simp) this

Result:
k : ℕ
x✝ : k + 2 ≠ 0
m : ℕ := (k + 2).minFac
this : (k + 2) / m < k + 2
h₁ : (k + 2) / m ≠ 0
⊢ (k + 2).primeFactorsList.prod = k + 2
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
/-- Auxiliary lemma for `setIntegral_density`. -/
lemma setIntegral_density_of_measurableSet (hκν : fst κ ≤ ν)
    [IsFiniteKernel ν] (n : ℕ) (a : α) {s : Set β} (hs : MeasurableSet s) {A : Set γ}
    (hA : MeasurableSet[countableFiltration γ n] A) :
    ∫ x in A, density κ ν a x s ∂(ν a) = (κ a (A ×ˢ s)).toReal

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ ∀ᶠ (a_1 : ℕ) in atTop,
    ∫ (x : γ) in A, κ.densityProcess ν a_1 a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a

Tactic:
simp only [eventually_atTop]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
inst✝ : IsFiniteKernel ν
n : ℕ
a : α
s : Set β
hs : MeasurableSet s
A : Set γ
hA : MeasurableSet A
this : ∫ (x : γ) in A, κ.density ν a x s ∂ν a = limsup (fun i => ∫ (x : γ) in A, κ.densityProcess ν i a x s ∂ν a) atTop
⊢ ∃ a_1, ∀ b ≥ a_1, ∫ (x : γ) in A, κ.densityProcess ν b a x s ∂ν a = ∫ (x : γ) in A, κ.densityProcess ν n a x s ∂ν a
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem SatisfiesM_foldlM [Monad m] [LawfulMonad m]
    {as : Array α} (motive : Nat → β → Prop) {init : β} (h0 : motive 0 init) {f : β → α → m β}
    (hf : ∀ i : Fin as.size, ∀ b, motive i.1 b → SatisfiesM (motive (i.1 + 1)) (f b as[i])) :
    SatisfiesM (motive as.size) (as.foldlM f init)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
i j : Nat
b : β
h₁ : j ≤ as.size
h₂ : as.size ≤ i + j
H : motive j b
hj : j < as.size
⊢ SatisfiesM (motive as.size)
    (match i with
    | 0 => pure b
    | i'.succ =>
      let_fun this := ⋯;
      do
      let __do_lift ← f b as[j]
      foldlM.loop f as as.size ⋯ i' (j + 1) __do_lift)

Tactic:
split

Result:
case h_1
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ : Nat
h₂ : as.size ≤ 0 + j
⊢ SatisfiesM (motive as.size) (pure b)

case h_2
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
as : Array α
motive : Nat → β → Prop
init : β
h0 : motive 0 init
f : β → α → m β
hf : ∀ (i : Fin as.size) (b : β), motive (↑i) b → SatisfiesM (motive (↑i + 1)) (f b as[i])
j : Nat
b : β
h₁ : j ≤ as.size
H : motive j b
hj : j < as.size
i✝ i'✝ : Nat
h₂ : as.size ≤ i'✝.succ + j
⊢ SatisfiesM (motive as.size)
    (let_fun this := ⋯;
    do
    let __do_lift ← f b as[j]
    foldlM.loop f as as.size ⋯ i'✝ (j + 1) __do_lift)
-- Mathlib/Topology/Algebra/Support.lean
theorem exists_compact_iff_hasCompactMulSupport [R1Space α] :
    (∃ K : Set α, IsCompact K ∧ ∀ x, x ∉ K → f x = 1) ↔ HasCompactMulSupport f

Proof state:
α : Type u_2
β : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : One β
f : α → β
inst✝ : R1Space α
⊢ (∃ K, IsCompact K ∧ ∀ x ∉ K, f x = 1) ↔ HasCompactMulSupport f

Tactic:
simp_rw [← nmem_mulSupport, ← mem_compl_iff, ← subset_def, compl_subset_compl,
  hasCompactMulSupport_def, exists_isCompact_superset_iff]

Result:
no goals
-- Mathlib/Data/Nat/Log.lean
lemma log2_eq_log_two {n : ℕ} : Nat.log2 n = Nat.log 2 n

Proof state:
case inr.H
n : ℕ
hn : n ≠ 0
⊢ ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n

Tactic:
intro m

Result:
case inr.H
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ m ≤ n.log2 ↔ m ≤ log 2 n

Proof state:
case inr.H
n : ℕ
hn : n ≠ 0
m : ℕ
⊢ m ≤ n.log2 ↔ m ≤ log 2 n

Tactic:
rw [Nat.le_log2 hn, ← Nat.pow_le_iff_le_log Nat.one_lt_two hn]

Result:
no goals

Proof state:
n : ℕ
⊢ n.log2 = log 2 n

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl

⊢ log2 0 = log 2 0

case inr
n : ℕ
hn : n ≠ 0
⊢ n.log2 = log 2 n

Proof state:
case inl

⊢ log2 0 = log 2 0

Tactic:
rw [log2_zero, log_zero_right]

Result:
no goals

Proof state:
case inr
n : ℕ
hn : n ≠ 0
⊢ n.log2 = log 2 n

Tactic:
apply eq_of_forall_le_iff

Result:
case inr.H
n : ℕ
hn : n ≠ 0
⊢ ∀ (c : ℕ), c ≤ n.log2 ↔ c ≤ log 2 n
-- Mathlib/Analysis/Fourier/AddCircle.lean
theorem fourier_coe_apply {n : ℤ} {x : ℝ} :
    fourier n (x : AddCircle T) = Complex.exp (2 * π * Complex.I * n * x / T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
norm_num

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ (fourier n) ↑x = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
rw [fourier_apply, ← QuotientAddGroup.mk_zsmul, toCircle, Function.Periodic.lift_coe,
  Circle.coe_exp, Complex.ofReal_mul, Complex.ofReal_div, Complex.ofReal_mul, zsmul_eq_mul,
  Complex.ofReal_mul, Complex.ofReal_intCast]

Result:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (↑2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Proof state:
case e_z
T : ℝ
n : ℤ
x : ℝ
⊢ 2 * ↑π / ↑T * (↑n * ↑x) * Complex.I = 2 * ↑π * Complex.I * ↑n * ↑x / ↑T

Tactic:
ring

Result:
no goals

Proof state:
T : ℝ
n : ℤ
x : ℝ
⊢ Complex.exp (2 * ↑π / ↑T * (↑n * ↑x) * Complex.I) = Complex.exp (2 * ↑π * Complex.I * ↑n * ↑x / ↑T)

Tactic:
congr 1

Result:
case e_z
T : ℝ
n : ℤ
x : ℝ
⊢ 2 * ↑π / ↑T * (↑n * ↑x) * Complex.I = 2 * ↑π * Complex.I * ↑n * ↑x / ↑T
-- Mathlib/Algebra/Lie/Submodule.lean
@[simp]
lemma map_incl_lt_iff_lt_top {N' : LieSubmodule R L N} :
    N'.map (LieSubmodule.incl N) < N ↔ N' < ⊤

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ map N.incl N' < N ↔ N' < ⊤

Tactic:
convert (LieSubmodule.mapOrderEmbedding (f := N.incl) Subtype.coe_injective).lt_iff_lt

Result:
case h.e'_1.h.e'_4
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ N = (mapOrderEmbedding ⋯) ⊤

Proof state:
case h.e'_1.h.e'_4
R : Type u
L : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : LieRing L
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : LieRingModule L M
N : LieSubmodule R L M
N' : LieSubmodule R L ↥N
⊢ N = (mapOrderEmbedding ⋯) ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem comp_C_integral_of_surjective_of_isJacobsonRing {R : Type*} [CommRing R] [IsJacobsonRing R]
    {σ : Type*} [Finite σ] {S : Type*} [Field S] (f : MvPolynomial σ R →+* S)
    (hf : Function.Surjective ↑f) : (f.comp C).IsIntegral

Proof state:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
⊢ (f.comp C).IsIntegral

Tactic:
have e := (Fintype.equivFin σ).symm

Result:
case intro
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
⊢ (f.comp C).IsIntegral

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective ⇑(g.comp (Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Tactic:
norm_num at hf'

Result:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsJacobsonRing R
σ : Type u_2
inst✝¹ : _root_.Finite σ
S : Type u_3
inst✝ : Field S
f : MvPolynomial σ R →+* S
hf : Function.Surjective ⇑f
val✝ : Fintype σ
e : Fin (Fintype.card σ) ≃ σ
f' : MvPolynomial (Fin (Fintype.card σ)) R →+* S := f.comp (renameEquiv R e).toRingEquiv.toRingHom
this : (ker f').IsMaximal
g : MvPolynomial (Fin (Fintype.card σ)) R ⧸ ker f' →+* S := Ideal.Quotient.lift (ker f') f' ⋯
hf' : Function.Surjective (⇑g ∘ ⇑(Ideal.Quotient.mk (ker f')))
hfg : g.comp (Ideal.Quotient.mk (ker f')) = f'
⊢ Function.Surjective ⇑g

Tactic:
exact Function.Surjective.of_comp hf'

Result:
no goals
-- Mathlib/Topology/Category/Compactum.lean
theorem lim_eq_str {X : Compactum} (F : Ultrafilter X) : F.lim = X.str F

Proof state:
X : Compactum
F : Ultrafilter X.A
⊢ F.lim = X.str F

Tactic:
rw [Ultrafilter.lim_eq_iff_le_nhds, le_nhds_iff]

Result:
X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F

Proof state:
X : Compactum
F : Ultrafilter X.A
⊢ ∀ (s : Set X.A), X.str F ∈ s → IsOpen s → s ∈ ↑F

Tactic:
tauto

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_max {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) (s : Set α) :
    ∫⁻ x in s, max (f x) (g x) ∂μ =
      ∫⁻ x in s ∩ { x | f x ≤ g x }, g x ∂μ + ∫⁻ x in s ∩ { x | g x < f x }, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}

Tactic:
exacts [measurableSet_lt hg hf, measurableSet_le hf hg]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ ∫⁻ (x : α) in s, f x ⊔ g x ∂μ = ∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ

Tactic:
rw [lintegral_max hf hg, restrict_restrict, restrict_restrict, inter_comm s, inter_comm s]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | g x < f x}

α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
s : Set α
⊢ MeasurableSet {x | f x ≤ g x}
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem derivWithin_sub_const_fun (c : F) : derivWithin (f · - c) = derivWithin f

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
⊢ (derivWithin fun x => f x - c) = derivWithin f

Tactic:
ext

Result:
case h.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝¹ : Set 𝕜
x✝ : 𝕜
⊢ derivWithin (fun x => f x - c) x✝¹ x✝ = derivWithin f x✝¹ x✝

Proof state:
case h.h
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
c : F
x✝¹ : Set 𝕜
x✝ : 𝕜
⊢ derivWithin (fun x => f x - c) x✝¹ x✝ = derivWithin f x✝¹ x✝

Tactic:
apply derivWithin_sub_const

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem le_of_mem_A {r ε : ℝ} {L : E →L[𝕜] F} {x : E} (hx : x ∈ A f L r ε) {y z : E}
    (hy : y ∈ closedBall x (r / 2)) (hz : z ∈ closedBall x (r / 2)) :
    ‖f z - f y - L (z - y)‖ ≤ ε * r

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x : E
hx : x ∈ A f L r ε
y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
⊢ ‖f z - f y - L (z - y)‖ ≤ ε * r

Tactic:
rcases hx with ⟨r', r'mem, hr'⟩

Result:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ ≤ ε * r

Proof state:
case intro.intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ ≤ ε * r

Tactic:
apply le_of_lt

Result:
case intro.intro.hab
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ < ε * r

Proof state:
case intro.intro.hab
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
r ε : ℝ
L : E →L[𝕜] F
x y z : E
hy : y ∈ closedBall x (r / 2)
hz : z ∈ closedBall x (r / 2)
r' : ℝ
r'mem : r' ∈ Ioc (r / 2) r
hr' : ∀ y ∈ ball x r', ∀ z ∈ ball x r', ‖f z - f y - L (z - y)‖ < ε * r
⊢ ‖f z - f y - L (z - y)‖ < ε * r

Tactic:
exact hr' _ ((mem_closedBall.1 hy).trans_lt r'mem.1) _ ((mem_closedBall.1 hz).trans_lt r'mem.1)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem eq_zero_or_eq_one (a : BitVec 1) : a = 0#1 ∨ a = 1#1

Proof state:
a : Nat
ha : a < 2 ^ 1
⊢ a = 0 ∨ a = 1

Tactic:
omega

Result:
no goals

Proof state:
case ofFin.mk.inl.refl
ha : 0 < 2 ^ 1
⊢ { toFin := ⟨0, ha⟩ } = 0#1 ∨ { toFin := ⟨0, ha⟩ } = 1#1

Tactic:
simp

Result:
no goals

Proof state:
case ofFin.mk
a : Nat
ha : a < 2 ^ 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Tactic:
have acases : a = 0 ∨ a = 1 := by omega

Result:
case ofFin.mk
a : Nat
ha : a < 2 ^ 1
acases : a = 0 ∨ a = 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Proof state:
a : BitVec 1
⊢ a = 0#1 ∨ a = 1#1

Tactic:
obtain ⟨a, ha⟩ := a

Result:
case ofFin.mk
a : Nat
ha : a < 2 ^ 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Proof state:
ha : 1 < 2 ^ 1
⊢ { toFin := ⟨1, ha⟩ } = 0#1 ∨ { toFin := ⟨1, ha⟩ } = 1#1

Tactic:
simp

Result:
no goals

Proof state:
case ofFin.mk.inr
a : Nat
ha : a < 2 ^ 1
h✝ : a = 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Tactic:
case inr h =>
subst h
simp

Result:
no goals

Proof state:
a : Nat
ha : a < 2 ^ 1
h : a = 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Tactic:
subst h

Result:
ha : 1 < 2 ^ 1
⊢ { toFin := ⟨1, ha⟩ } = 0#1 ∨ { toFin := ⟨1, ha⟩ } = 1#1

Proof state:
case ofFin.mk
a : Nat
ha : a < 2 ^ 1
acases : a = 0 ∨ a = 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1

Tactic:
rcases acases with ⟨rfl | rfl⟩

Result:
case ofFin.mk.inl.refl
ha : 0 < 2 ^ 1
⊢ { toFin := ⟨0, ha⟩ } = 0#1 ∨ { toFin := ⟨0, ha⟩ } = 1#1

case ofFin.mk.inr
a : Nat
ha : a < 2 ^ 1
h✝ : a = 1
⊢ { toFin := ⟨a, ha⟩ } = 0#1 ∨ { toFin := ⟨a, ha⟩ } = 1#1