harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_modify [EquivBEq α] [LawfulHashable α] {k k' : α} {f : β → β}
    (h : m.WF) {hc : k' ∈ Const.modify m k f} :
    Const.get (Const.modify m k f) k' hc =
      if heq : k == k' then
        haveI h' : k ∈ m := mem_congr h heq |>.mpr <| mem_modify h |>.mp hc
        f (Const.get m k h')
      else
        haveI h' : k' ∈ m := mem_modify h |>.mp hc
        Const.get m k' h'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ (modify m k f).contains k' = true →
    get (modify m k f) k' hc = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_modify

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
hc✝ : k' ∈ modify m k f
hc : (modify m k f).contains k' = true
⊢ get (modify m k f) k' hc✝ = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

Tactic:
revert hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ (modify m k f).contains k' = true →
    get (modify m k f) k' hc = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
hc : k' ∈ modify m k f
⊢ get (modify m k f) k' hc = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : β → β
h : m.WF
hc✝ : k' ∈ modify m k f
hc : (modify m k f).contains k' = true
⊢ get (modify m k f) k' hc✝ = if heq : (k == k') = true then f (get m k ⋯) else get m k' ⋯
-- Mathlib/FieldTheory/Galois/Basic.lean
theorem of_separable_splitting_field_aux [hFE : FiniteDimensional F E] [sp : p.IsSplittingField F E]
    (hp : p.Separable) (K : Type*) [Field K] [Algebra F K] [Algebra K E] [IsScalarTower F K E]
    {x : E} (hx : x ∈ p.aroots E)
    -- these are both implied by `hFE`, but as they carry data this makes the lemma more general
    [Fintype (K →ₐ[F] E)]
    [Fintype (K⟮x⟯.restrictScalars F →ₐ[F] E)] :
    Fintype.card (K⟮x⟯.restrictScalars F →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯

Proof state:
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯

Tactic:
have h2 : minpoly K x ∣ p.map (algebraMap F K) := by
  apply minpoly.dvd
  rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
    IsScalarTower.algebraMap_eq]
  exact (Polynomial.mem_roots (Polynomial.map_ne_zero h1)).mp hx

Result:
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
h2 : minpoly K x ∣ Polynomial.map (algebraMap F K) p
⊢ Fintype.card (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E) = Fintype.card (K →ₐ[F] E) * finrank K ↥K⟮x⟯

Proof state:
case hp
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ (Polynomial.aeval x) (Polynomial.map (algebraMap F K) p) = 0

Tactic:
rw [Polynomial.aeval_def, Polynomial.eval₂_map, ← Polynomial.eval_map, ←
  IsScalarTower.algebraMap_eq]

Result:
case hp
F : Type u_1
inst✝⁸ : Field F
E : Type u_2
inst✝⁷ : Field E
inst✝⁶ : Algebra F E
p : F[X]
hFE : FiniteDimensional F E
sp : Polynomial.IsSplittingField F E p
hp : p.Separable
K : Type u_3
inst✝⁵ : Field K
inst✝⁴ : Algebra F K
inst✝³ : Algebra K E
inst✝² : IsScalarTower F K E
x : E
hx : x ∈ p.aroots E
inst✝¹ : Fintype (K →ₐ[F] E)
inst✝ : Fintype (↥(IntermediateField.restrictScalars F K⟮x⟯) →ₐ[F] E)
h : IsIntegral K x
h1 : p ≠ 0
⊢ Polynomial.eval x (Polynomial.map (algebraMap F E) p) = 0
-- Mathlib/Geometry/Euclidean/Inversion/Calculus.lean
theorem hasFDerivAt_inversion (hx : x ≠ c) :
    HasFDerivAt (inversion c R)
      ((R / dist x c) ^ 2 • (reflection (ℝ ∙ (x - c))ᗮ : F →L[ℝ] F)) x

Proof state:
case intro.refine_2.refine_1
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
this :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
        (_root_.id (c + x) - c))
    (c + x)
⊢ EqOn
    ⇑((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
        (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
          (_root_.id (c + x) - c))
    ⇑((R / dist ((fun x => c + x) x) c) ^ 2 •
        ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
            continuous_toFun := ⋯, continuous_invFun := ⋯ })
    {x}

Tactic:
have : ((‖x‖ ^ 2) ^ 2)⁻¹ * (‖x‖ ^ 2) = (‖x‖ ^ 2)⁻¹ := by
  rw [← div_eq_inv_mul, sq (‖x‖ ^ 2), div_self_mul_self']

Result:
case intro.refine_2.refine_1
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
c : F
R : ℝ
x : F
hx : (fun x => c + x) x ≠ c
this✝ :
  HasFDerivAt (inversion c R)
    ((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
      (R ^ 2 •
            -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
              2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
        (_root_.id (c + x) - c))
    (c + x)
this : ((‖x‖ ^ 2) ^ 2)⁻¹ * ‖x‖ ^ 2 = (‖x‖ ^ 2)⁻¹
⊢ EqOn
    ⇑((R ^ 2 * ((fun y => y⁻¹) ∘ fun x => ‖_root_.id x - c‖ ^ 2) (c + x)) • ContinuousLinearMap.id ℝ F +
        (R ^ 2 •
              -((‖_root_.id (c + x) - c‖ ^ 2) ^ 2)⁻¹ •
                2 • ((innerSL ℝ) (_root_.id (c + x) - c)).comp (ContinuousLinearMap.id ℝ F)).smulRight
          (_root_.id (c + x) - c))
    ⇑((R / dist ((fun x => c + x) x) c) ^ 2 •
        ↑{ toLinearEquiv := (reflection (Submodule.span ℝ {(fun x => c + x) x - c})ᗮ).toLinearEquiv,
            continuous_toFun := ⋯, continuous_invFun := ⋯ })
    {x}
-- Mathlib/RingTheory/Algebraic/Basic.lean
theorem IsAlgebraic.nontrivial {a : A} (h : IsAlgebraic R a) : Nontrivial R

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : IsAlgebraic R a
⊢ Nontrivial R

Tactic:
contrapose! h

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : ¬Nontrivial R
⊢ ¬IsAlgebraic R a

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : Subsingleton R
⊢ ¬IsAlgebraic R a

Tactic:
apply is_transcendental_of_subsingleton

Result:
no goals

Proof state:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : ¬Nontrivial R
⊢ ¬IsAlgebraic R a

Tactic:
rw [not_nontrivial_iff_subsingleton] at h

Result:
R : Type u
A : Type v
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
h : Subsingleton R
⊢ ¬IsAlgebraic R a
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
/-- Second derivative of q-ary entropy. -/
lemma deriv2_qaryEntropy :
    deriv^[2] (qaryEntropy q) p = -1 / (p * (1 - p))

Proof state:
case hf
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (↑q - 1)) p

case hg
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (1 - y)) p

Tactic:
simp only [ne_eq, differentiableAt_const]

Result:
case hg
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
⊢ DifferentiableAt ℝ (fun y => log (1 - y)) p

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
⊢ False

Tactic:
cases this <;> simp_all [
  not_continuousAt_deriv_qaryEntropy_zero, not_continuousAt_deriv_qaryEntropy_one, contAt]

Result:
no goals

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
d_oneminus : ∀ (p : ℝ), deriv (fun y => 1 - y) p = -1
⊢ deriv (fun x => log (↑q - 1) + log (1 - x)) p - p⁻¹ = -1 / (p * (1 - p))

Tactic:
field_simp [sub_ne_zero_of_ne xne1.symm, this, d_oneminus]

Result:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
d_oneminus : ∀ (p : ℝ), deriv (fun y => 1 - y) p = -1
⊢ (-p - (1 - p)) * (p * (1 - p)) = -((1 - p) * p)

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ False

Tactic:
have contAt := h.continuousAt

Result:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
contAt : ContinuousAt (deriv (qaryEntropy q)) p
⊢ False

Proof state:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
⊢ ¬DifferentiableAt ℝ (deriv (qaryEntropy q)) p

Tactic:
intro h

Result:
case neg
q : ℕ
p : ℝ
is_x_where_nondiff : ¬(p ≠ 0 ∧ p ≠ 1)
this : p = 0 ∨ p = 1
h : DifferentiableAt ℝ (deriv (qaryEntropy q)) p
⊢ False

Proof state:
q✝ : ℕ
p✝ : ℝ
xne0 : p✝ ≠ 0
xne1 : p✝ ≠ 1
this : ∀ᶠ (y : ℝ) in 𝓝 p✝, deriv (fun p => qaryEntropy q✝ p) y = log (↑q✝ - 1) + log (1 - y) - log y
q p : ℝ
⊢ DifferentiableAt ℝ (fun p => q - p) p

Tactic:
fun_prop

Result:
no goals

Proof state:
q : ℕ
p : ℝ
xne0 : p ≠ 0
xne1 : p ≠ 1
this✝ : ∀ᶠ (y : ℝ) in 𝓝 p, deriv (fun p => qaryEntropy q p) y = log (↑q - 1) + log (1 - y) - log y
this : ∀ {q : ℝ} (p : ℝ), DifferentiableAt ℝ (fun p => q - p) p
d_oneminus : ∀ (p : ℝ), deriv (fun y => 1 - y) p = -1
⊢ (-p - (1 - p)) * (p * (1 - p)) = -((1 - p) * p)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/List.lean
theorem foldl_toList (o : Option β) (a : α) (f : α → β → α) :
    o.toList.foldl f a = o.elim a (fun b => f a b)

Proof state:
β : Type u_1
α : Type u_2
o : Option β
a : α
f : α → β → α
⊢ List.foldl f a o.toList = o.elim a fun b => f a b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem sup_eq_sup {ι ι' : Type u} (r : ι → ι → Prop) (r' : ι' → ι' → Prop) [IsWellOrder ι r]
    [IsWellOrder ι' r'] {o : Ordinal.{u}} (ho : type r = o) (ho' : type r' = o)
    (f : ∀ a < o, Ordinal.{max u v}) :
    sup.{_, v} (familyOfBFamily' r ho f) = sup.{_, v} (familyOfBFamily' r' ho' f) :=
  sup_eq_of_range_eq.{u, u, v} (by simp)

Proof state:
ι ι' : Type u
r : ι → ι → Prop
r' : ι' → ι' → Prop
inst✝¹ : IsWellOrder ι r
inst✝ : IsWellOrder ι' r'
o : Ordinal.{u}
ho : type r = o
ho' : type r' = o
f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}
⊢ range (familyOfBFamily' r ho f) = range (familyOfBFamily' r' ho' f)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Logic.lean
theorem heq_eqRec_iff_heq {α : Sort _} {a : α} {motive : (a' : α) → a = a' → Sort _}
    {x : motive a rfl} {a' : α} {e : a = a'} {β : Sort _} {y : β} :
    HEq y (@Eq.rec α a motive x a' e) ↔ HEq y x

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
β : Sort u_2
y : β
⊢ HEq y (⋯ ▸ x) ↔ HEq y x

Tactic:
rfl

Result:
no goals

Proof state:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
a' : α
e : a = a'
β : Sort u_2
y : β
⊢ HEq y (e ▸ x) ↔ HEq y x

Tactic:
subst e

Result:
α : Sort u_1
a : α
motive : (a' : α) → a = a' → Sort u_2
x : motive a ⋯
β : Sort u_2
y : β
⊢ HEq y (⋯ ▸ x) ↔ HEq y x
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
theorem le_emultiplicity_iff_replicate_le_normalizedFactors {a b : R} {n : ℕ} (ha : Irreducible a)
    (hb : b ≠ 0) :
    ↑n ≤ emultiplicity a b ↔ replicate n (normalize a) ≤ normalizedFactors b

Proof state:
case succ.mpr.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ b

Tactic:
rw [← (prod_normalizedFactors hb).dvd_iff_dvd_right, hu, prod_add, prod_replicate]

Result:
case succ.mpr.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ normalize a ^ (n + 1) * u.prod

Proof state:
case succ.mpr
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
⊢ (∃ u, normalizedFactors b = replicate (n + 1) (normalize a) + u) → a ^ (n + 1) ∣ b

Tactic:
rintro ⟨u, hu⟩

Result:
case succ.mpr.intro
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
b : R
hb : b ≠ 0
u : Multiset R
hu : normalizedFactors b = replicate (n + 1) (normalize a) + u
⊢ a ^ (n + 1) ∣ b

Proof state:
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
n : ℕ
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)

Tactic:
induction' n with n ih

Result:
case zero
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
⊢ ∀ {b : R}, b ≠ 0 → (a ^ 0 ∣ b ↔ replicate 0 (normalize a) ≤ normalizedFactors b)

case succ
R : Type u_2
inst✝² : CancelCommMonoidWithZero R
inst✝¹ : UniqueFactorizationMonoid R
inst✝ : NormalizationMonoid R
a : R
ha : Irreducible a
n : ℕ
ih : ∀ {b : R}, b ≠ 0 → (a ^ n ∣ b ↔ replicate n (normalize a) ≤ normalizedFactors b)
⊢ ∀ {b : R}, b ≠ 0 → (a ^ (n + 1) ∣ b ↔ replicate (n + 1) (normalize a) ≤ normalizedFactors b)
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_congr {p q : α → Prop} [DecidablePred p] [DecidablePred q] {s : Multiset α} :
    (∀ x ∈ s, p x ↔ q x) → filter p s = filter q s :=
  Quot.inductionOn s fun _l h => congr_arg ofList <| List.filter_congr <| by simpa using h

Proof state:
α : Type u_1
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
s : Multiset α
_l : List α
h : ∀ x ∈ Quot.mk (⇑(isSetoid α)) _l, p x ↔ q x
⊢ ∀ x ∈ _l, decide (p x) = decide (q x)

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Data/Semiquot.lean
theorem liftOn_ofMem (q : Semiquot α) (f : α → β)
    (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b) (a : α) (aq : a ∈ q) : liftOn q f h = f a

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
h : ∀ a ∈ q, ∀ b ∈ q, f a = f b
a : α
aq : a ∈ q
⊢ q.liftOn f h = f a

Tactic:
revert h

Result:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a

Tactic:
intro

Result:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
h✝ : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b
⊢ (mk aq).liftOn f h✝ = f a

Proof state:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a ∈ q, ∀ b ∈ q, f a = f b), q.liftOn f h = f a

Tactic:
rw [eq_mk_of_mem aq]

Result:
α : Type u_1
β : Type u_2
q : Semiquot α
f : α → β
a : α
aq : a ∈ q
⊢ ∀ (h : ∀ a_1 ∈ mk aq, ∀ b ∈ mk aq, f a_1 = f b), (mk aq).liftOn f h = f a
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem isIntegral_trans [Algebra.IsIntegral R A] (x : B) (hx : IsIntegral A x) :
    IsIntegral R x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
hx : IsIntegral A x
⊢ IsIntegral R x

Tactic:
rcases hx with ⟨p, pmonic, hp⟩

Result:
case intro.intro
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
⊢ IsIntegral R x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap (↥S) B) x p' = 0

Tactic:
rw [IsScalarTower.algebraMap_eq S A B, ← eval₂_map]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : CommRing A
inst✝⁵ : Ring B
inst✝⁴ : Algebra A B
inst✝³ : Algebra R B
inst✝² : Algebra R A
inst✝¹ : IsScalarTower R A B
inst✝ : Algebra.IsIntegral R A
x : B
p : A[X]
pmonic : p.Monic
hp : eval₂ (algebraMap A B) x p = 0
S : Subalgebra R A := adjoin R ↑p.coeffs
this : Module.Finite R ↥S
p' : (↥S)[X] := p.toSubring S.toSubring ⋯
⊢ eval₂ (algebraMap A B) x (Polynomial.map (algebraMap (↥S) A) p') = 0
-- Mathlib/Data/List/Chain.lean
theorem chain'_append :
    ∀ {l₁ l₂ : List α},
      Chain' R (l₁ ++ l₂) ↔ Chain' R l₁ ∧ Chain' R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
  | [], l => by simp
  | [a], l => by simp [chain'_cons', and_comm]
  | a :: b :: l₁, l₂ => by
    rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, and_assoc]
    simp

Proof state:
α : Type u
R : α → α → Prop
a : α
l : List α
⊢ Chain' R ([a] ++ l) ↔ Chain' R [a] ∧ Chain' R l ∧ ∀ (x : α), x ∈ [a].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
simp [chain'_cons', and_comm]

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ Chain' R (a :: b :: l₁ ++ l₂) ↔
    Chain' R (a :: b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
rw [cons_append, cons_append, chain'_cons, chain'_cons, ← cons_append, chain'_append, and_assoc]

Result:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Proof state:
α : Type u
R : α → α → Prop
l : List α
⊢ Chain' R ([] ++ l) ↔ Chain' R [] ∧ Chain' R l ∧ ∀ (x : α), x ∈ [].getLast? → ∀ (y : α), y ∈ l.head? → R x y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
R : α → α → Prop
a b : α
l₁ l₂ : List α
⊢ (R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y) ↔
    R a b ∧ Chain' R (b :: l₁) ∧ Chain' R l₂ ∧ ∀ (x : α), x ∈ (a :: b :: l₁).getLast? → ∀ (y : α), y ∈ l₂.head? → R x y

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_succAbove
    {f : ℂⁿ⁺¹ → E} {c : ℂⁿ⁺¹} {R : ℝⁿ⁺¹} (hf : TorusIntegrable f c R)
    (i : Fin (n + 1)) :
    (∯ x in T(c, R), f x) =
      ∮ x in C(c i, R i), ∯ y in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Tactic:
have heπ : (e ⁻¹' Icc 0 fun _ => 2 * π) = Icc 0 (2 * π) ×ˢ Icc (0 : ℝⁿ) fun _ => 2 * π :=
  ((Fin.insertNthOrderIso (fun _ => ℝ) i).preimage_Icc _ _).trans (Icc_prod_eq _ _)

Result:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
⊢ (∯ (x : Fin (n + 1) → ℂ) in T(c, R), f x) =
    ∮ (x : ℂ) in C(c i, R i), ∯ (y : Fin n → ℂ) in T(c ∘ i.succAbove, R ∘ i.succAbove), f (i.insertNth x y)

Proof state:
case e_a.e_a
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : (Fin (n + 1) → ℂ) → E
c : Fin (n + 1) → ℂ
R : Fin (n + 1) → ℝ
hf : TorusIntegrable f c R
i : Fin (n + 1)
e : ℝ × (Fin n → ℝ) ≃ᵐ (Fin (n + 1) → ℝ) := (MeasurableEquiv.piFinSuccAbove (fun x => ℝ) i).symm
hem : MeasurePreserving (⇑e) volume volume
heπ : (⇑e ⁻¹' Icc 0 fun x => 2 * π) = Icc 0 (2 * π) ×ˢ Icc 0 fun x => 2 * π
θ : ℝ
x✝¹ : θ ∈ Icc 0 (2 * π)
Θ : Fin n → ℝ
x✝ : Θ ∈ Icc 0 fun x => 2 * π
⊢ (fun i_1 => c i_1 + ↑(R i_1) * cexp (↑(i.insertNth θ Θ i_1) * I)) =
    i.insertNth (circleMap (c i) (R i) θ) fun i_1 => c (i.succAbove i_1) + ↑(R (i.succAbove i_1)) * cexp (↑(Θ i_1) * I)

Tactic:
simp only [funext_iff, i.forall_iff_succAbove, circleMap, Fin.insertNth_apply_same,
  eq_self_iff_true, Fin.insertNth_apply_succAbove, imp_true_iff, and_self_iff]

Result:
no goals