harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isRat_mul {α} [Ring α] {f : α → α → α} {a b : α} {na nb nc : ℤ} {da db dc k : ℕ} :
    f = HMul.hMul → IsRat a na da → IsRat b nb db →
    Int.mul na nb = Int.mul k nc →
    Nat.mul da db = Nat.mul k dc →
    IsRat (f a b) nc dc

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁✝ : na * nb = ↑k * nc
h₂✝ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
H : ∀ (a : α), a * ⅟↑da * ⅟↑db = a * ⅟↑db * ⅟↑da
h₁ : ↑na * ↑nb = ↑k * ↑nc
h₂ : ↑nc * ⅟↑dc = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc
⊢ ↑nc * ↑k * ⅟↑da * ⅟↑db = ↑nc * ↑k * ↑dc * ⅟↑da * ⅟↑db * ⅟↑dc

Tactic:
simp only [mul_invOf_cancel_right,
  (Nat.cast_commute (α := α) da dc).invOf_left.invOf_right.right_comm,
  (Nat.cast_commute (α := α) db dc).invOf_left.invOf_right.right_comm]

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
refine ⟨this, ?_⟩

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this✝ : Invertible ↑(da * db)
this : Invertible ↑dc
⊢ ↑na * ⅟↑da * (↑nb * ⅟↑db) = ↑nc * ⅟↑dc

Proof state:
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc

Tactic:
have : Invertible (↑(da * db) : α) := by simpa using invertibleMul (da:α) db

Result:
case mk.mk
α : Type u_1
inst✝ : Ring α
na nb nc : ℤ
da db dc k : ℕ
inv✝¹ : Invertible ↑da
inv✝ : Invertible ↑db
h₁ : na * nb = ↑k * nc
h₂ : da * db = k * dc
this : Invertible ↑(da * db)
⊢ IsRat (↑na * ⅟↑da * (↑nb * ⅟↑db)) nc dc
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
@[to_additive (attr := simp)]
lemma prod_diag [DecidableEq α] (s : Finset α) (f : α × α → β) :
    ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s : Finset α
f : α × α → β
⊢ ∏ i ∈ s.diag, f i = ∏ i ∈ s, f (i, i)

Tactic:
apply prod_nbij' Prod.fst (fun i ↦ (i, i)) <;> simp

Result:
no goals
-- Mathlib/Topology/Clopen.lean
theorem continuousOn_boolIndicator_iff_isClopen (s U : Set X) :
    ContinuousOn U.boolIndicator s ↔ IsClopen (((↑) : s → X) ⁻¹' U)

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s U : Set X
⊢ ContinuousOn U.boolIndicator s ↔ IsClopen (Subtype.val ⁻¹' U)

Tactic:
rw [continuousOn_iff_continuous_restrict, ← continuous_boolIndicator_iff_isClopen]

Result:
X : Type u
inst✝ : TopologicalSpace X
s U : Set X
⊢ Continuous (s.restrict U.boolIndicator) ↔ Continuous (Subtype.val ⁻¹' U).boolIndicator

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s U : Set X
⊢ Continuous (s.restrict U.boolIndicator) ↔ Continuous (Subtype.val ⁻¹' U).boolIndicator

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/GaussEisensteinLemmas.lean
theorem sum_Ico_eq_card_lt {p q : ℕ} :
    ∑ a ∈ Ico 1 (p / 2).succ, a * q / p =
      #{x ∈ Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ | x.2 * p ≤ x.1 * q} :=
  if hp0 : p = 0 then by simp [hp0, Finset.ext_iff]
  else
    calc
      ∑ a ∈ Ico 1 (p / 2).succ, a * q / p =
          ∑ a ∈ Ico 1 (p / 2).succ, #{x ∈ Ico 1 (q / 2).succ | x * p ≤ a * q} :=
        Finset.sum_congr rfl fun x hx => div_eq_filter_card (Nat.pos_of_ne_zero hp0) <|
          calc
            x * q / p ≤ p / 2 * q / p

Proof state:
p q : ℕ
hp0 : ¬p = 0
⊢ ∀ a ∈ (Ico 1 (p / 2).succ).sigma fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ),
    (fun a => (a.fst, a.snd)) a ∈ filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ)

Tactic:
simp +contextual only [mem_filter, mem_sigma, and_self_iff,
forall_true_iff, mem_product]

Result:
no goals

Proof state:
p q : ℕ
hp0 : ¬p = 0
⊢ ∀ a ∈ filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ),
    (fun a => ⟨a.1, a.2⟩) a ∈ (Ico 1 (p / 2).succ).sigma fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)

Tactic:
simp +contextual only [mem_filter, mem_sigma, and_self_iff,
forall_true_iff, mem_product]

Result:
no goals

Proof state:
p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
⊢ x * q / p ≤ p / 2 * q / p

Tactic:
have := le_of_lt_succ (mem_Ico.mp hx).2

Result:
p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
this : x ≤ p / 2
⊢ x * q / p ≤ p / 2 * q / p

Proof state:
p q : ℕ
hp0 : p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, a * q / p =
    #(filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))

Tactic:
simp [hp0, Finset.ext_iff]

Result:
no goals

Proof state:
p q : ℕ
hp0 : ¬p = 0
x : ℕ
hx : x ∈ Ico 1 (p / 2).succ
this : x ≤ p / 2
⊢ x * q / p ≤ p / 2 * q / p

Tactic:
gcongr

Result:
no goals

Proof state:
p q : ℕ
hp0 : ¬p = 0
⊢ #((Ico 1 (p / 2).succ).sigma fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)) =
    #(filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))

Tactic:
exact card_nbij' (fun a ↦ ⟨a.1, a.2⟩) (fun a ↦ ⟨a.1, a.2⟩)
  (by simp +contextual only [mem_filter, mem_sigma, and_self_iff,
    forall_true_iff, mem_product])
  (by simp +contextual only [mem_filter, mem_sigma, and_self_iff,
    forall_true_iff, mem_product]) (fun _ _ ↦ rfl) (fun _ _ ↦ rfl)

Result:
no goals

Proof state:
p q : ℕ
hp0 : ¬p = 0
⊢ ∑ a ∈ Ico 1 (p / 2).succ, #(filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)) =
    #(filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))

Tactic:
rw [← card_sigma]

Result:
p q : ℕ
hp0 : ¬p = 0
⊢ #((Ico 1 (p / 2).succ).sigma fun a => filter (fun x => x * p ≤ a * q) (Ico 1 (q / 2).succ)) =
    #(filter (fun x => x.2 * p ≤ x.1 * q) (Ico 1 (p / 2).succ ×ˢ Ico 1 (q / 2).succ))
-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem frobeniusRotation_nonzero {a₁ a₂ : 𝕎 k} (ha₁ : a₁.coeff 0 ≠ 0) (ha₂ : a₂.coeff 0 ≠ 0) :
    frobeniusRotation p ha₁ ha₂ ≠ 0

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0

Tactic:
simpa [← h, frobeniusRotation, frobeniusRotationCoeff] using WittVector.zero_coeff p k 0

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ frobeniusRotation p ha₁ ha₂ ≠ 0

Tactic:
intro h

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ False

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ False

Tactic:
apply solution_nonzero p ha₁ ha₂

Result:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
a₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : frobeniusRotation p ha₁ ha₂ = 0
⊢ solution p a₁ a₂ = 0
-- Mathlib/Data/List/Sigma.lean
theorem kerase_comm (a₁ a₂) (l : List (Sigma β)) :
    kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l) :=
  if h : a₁ = a₂ then by simp [h]
  else
    if ha₁ : a₁ ∈ l.keys then
      if ha₂ : a₂ ∈ l.keys then
        match l, kerase a₁ l, exists_of_kerase ha₁, ha₂ with
        | _, _, ⟨b₁, l₁, l₂, a₁_nin_l₁, rfl, rfl⟩, _ =>
          if h' : a₂ ∈ l₁.keys then by
            simp [kerase_append_left h',
              kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]
          else by
            simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
              @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (Ne.symm h)]
      else by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
    else by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : a₁ ∉ l₁.keys
x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
h' : a₂ ∉ l₁.keys
⊢ kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))

Tactic:
simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
  @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (Ne.symm h)]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₁ : a₁ ∈ l.keys
ha₂ : a₂ ∉ l.keys
⊢ kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)

Tactic:
simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₁ : a₁ ∉ l.keys
⊢ kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)

Tactic:
simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : ¬a₁ = a₂
ha₂ : a₂ ∈ l.keys
b₁ : β a₁
l₁ l₂ : List (Sigma β)
a₁_nin_l₁ : a₁ ∉ l₁.keys
x✝ : a₂ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
ha₁ : a₁ ∈ (l₁ ++ ⟨a₁, b₁⟩ :: l₂).keys
h' : a₂ ∈ l₁.keys
⊢ kerase a₂ (l₁ ++ l₂) = kerase a₁ (kerase a₂ (l₁ ++ ⟨a₁, b₁⟩ :: l₂))

Tactic:
simp [kerase_append_left h',
  kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
a₁ a₂ : α
l : List (Sigma β)
h : a₁ = a₂
⊢ kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem induction_on_prime {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ x : α, IsUnit x → P x)
    (h₃ : ∀ a p : α, a ≠ 0 → Prime p → P a → P (p * a)) : P a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Prime p → P a → P (p * a)
⊢ P a

Tactic:
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime] at h₃

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
P : α → Prop
a : α
h₁ : P 0
h₂ : ∀ (x : α), IsUnit x → P x
h₃ : ∀ (a p : α), a ≠ 0 → Irreducible p → P a → P (p * a)
⊢ P a

Tactic:
exact WfDvdMonoid.induction_on_irreducible a h₁ h₂ h₃

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Module/Defs.lean
@[simp] lemma inner_sub_right {x y z : E} : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫

Proof state:
A : Type u_1
E : Type u_2
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : StarRing A
inst✝⁸ : AddCommGroup E
inst✝⁷ : Module ℂ A
inst✝⁶ : Module ℂ E
inst✝⁵ : PartialOrder A
inst✝⁴ : SMul Aᵐᵒᵖ E
inst✝³ : Norm A
inst✝² : Norm E
inst✝¹ : CStarModule A E
inst✝ : StarModule ℂ A
x y z : E
⊢ inner x (y - z) = inner x y - inner x z

Tactic:
simp [← innerₛₗ_apply]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma nonsingularLift_negMap {P : PointClass F} (hP : W.NonsingularLift P) :
    W.NonsingularLift <| W.negMap P

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P : PointClass F
hP : W.NonsingularLift P
⊢ W.NonsingularLift (W.negMap P)

Tactic:
rcases P with ⟨_⟩

Result:
case mk
F : Type u
inst✝ : Field F
W : Projective F
P : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Proof state:
case mk
F : Type u
inst✝ : Field F
W : Projective F
P : PointClass F
a✝ : Fin 3 → F
hP : W.NonsingularLift (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝)
⊢ W.NonsingularLift (W.negMap (Quot.mk (⇑(MulAction.orbitRel Fˣ (Fin 3 → F))) a✝))

Tactic:
exact nonsingular_neg hP

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem bind_powerset_len {α : Type*} (S : Multiset α) :
    (bind (Multiset.range (card S + 1)) fun k => S.powersetCard k) = S.powerset

Proof state:
case h
α : Type u_2
a✝ : List α
⊢ ↑(List.map ofList (flatMap (fun a => sublistsLen a a✝) (List.range (a✝.length + 1)))) =
    ↑(List.map ofList a✝.sublists')

Tactic:
exact coe_eq_coe.mpr ((List.range_bind_sublistsLen_perm _).map _)

Result:
no goals

Proof state:
case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k => powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧

Tactic:
simp_rw [quot_mk_to_coe, powerset_coe', powersetCard_coe, ← coe_range, coe_bind,
  ← List.map_flatMap, coe_card]

Result:
case h
α : Type u_2
a✝ : List α
⊢ ↑(List.map ofList (flatMap (fun a => sublistsLen a a✝) (List.range (a✝.length + 1)))) =
    ↑(List.map ofList a✝.sublists')

Proof state:
α : Type u_2
S : Multiset α
⊢ ((range (S.card + 1)).bind fun k => powersetCard k S) = S.powerset

Tactic:
induction S using Quotient.inductionOn

Result:
case h
α : Type u_2
a✝ : List α
⊢ ((range (card ⟦a✝⟧ + 1)).bind fun k => powersetCard k ⟦a✝⟧) = powerset ⟦a✝⟧
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_inv {u : ℕ → ℝ≥0∞} :
    expGrowthSup u⁻¹ = - expGrowthInf u

Proof state:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n => (u n).log / ↑n) n

Tactic:
rw [Pi.neg_apply, Pi.inv_apply, div_eq_mul_inv, div_eq_mul_inv, ← EReal.neg_mul, log_inv]

Result:
no goals

Proof state:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = limsup (-fun n => (u n).log / ↑n) atTop

Tactic:
refine limsup_congr (Eventually.of_forall fun n ↦ ?_)

Result:
u : ℕ → ℝ≥0∞
n : ℕ
⊢ (u⁻¹ n).log / ↑n = (-fun n => (u n).log / ↑n) n

Proof state:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = -expGrowthInf u

Tactic:
rw [expGrowthInf, ← limsup_neg]

Result:
u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = limsup (-fun n => (u n).log / ↑n) atTop
-- Mathlib/RingTheory/Polynomial/SeparableDegree.lean
theorem HasSeparableContraction.eq_degree {f : F[X]} (hf : HasSeparableContraction 1 f) :
    hf.degree = f.natDegree

Proof state:
F : Type u_1
inst✝ : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
a : ℕ
ha : hf.degree * 1 ^ a = f.natDegree
⊢ hf.degree = f.natDegree

Tactic:
rw [← ha, one_pow a, mul_one]

Result:
no goals

Proof state:
F : Type u_1
inst✝ : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
⊢ hf.degree = f.natDegree

Tactic:
let ⟨a, ha⟩ := hf.dvd_degree'

Result:
F : Type u_1
inst✝ : CommSemiring F
f : F[X]
hf : HasSeparableContraction 1 f
a : ℕ
ha : hf.degree * 1 ^ a = f.natDegree
⊢ hf.degree = f.natDegree
-- Mathlib/GroupTheory/CosetCover.lean
theorem index_le_of_leftCoset_cover_const : H.index ≤ s.card

Proof state:
case inl
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
h : H.index = 0
⊢ H.index ≤ s.card

Tactic:
exact h ▸ s.card.zero_le

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
⊢ H.index ≤ s.card

Tactic:
cases H.index.eq_zero_or_pos with
| inl h => exact h ▸ s.card.zero_le
| inr h =>
  rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers
  exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Function.Surjective ((↑s).restrict fun x => ↑(g x))
h : H.index > 0
⊢ H.index ≤ s.card

Tactic:
exact (Nat.card_le_card_of_surjective _ hcovers).trans_eq (Nat.card_eq_finsetCard _)

Result:
no goals

Proof state:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : ⋃ i ∈ s, g i • ↑H = Set.univ
h : H.index > 0
⊢ H.index ≤ s.card

Tactic:
rw [leftCoset_cover_const_iff_surjOn, Set.surjOn_iff_surjective] at hcovers

Result:
case inr
G : Type u_1
inst✝ : Group G
ι : Type u_2
s : Finset ι
H : Subgroup G
g : ι → G
hcovers : Function.Surjective ((↑s).restrict fun x => ↑(g x))
h : H.index > 0
⊢ H.index ≤ s.card
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toBasicOpen_injective (f : R) : Function.Injective (toBasicOpen R f)

Proof state:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
this : ∃ c_1, ↑c_1 * (↑⟨d, ⋯⟩ * a) = ↑c_1 * (↑⟨b, ⋯⟩ * c)
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Tactic:
obtain ⟨r, hr⟩ := this

Result:
case intro.intro.mk.intro.intro.mk.intro
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
I : Ideal R := { carrier := {r | r * (d * a) = r * (b * c)}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }
p : PrimeSpectrum R
hfp : f ∉ p.asIdeal
r : ↥p.asIdeal.primeCompl
hr : ↑r * (↑⟨d, ⋯⟩ * a) = ↑r * (↑⟨b, ⋯⟩ * c)
⊢ ∃ a ∈ ↑I, a ∉ ↑p.asIdeal

Proof state:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
⊢ IsLocalization.mk' (Localization.Away f) a ⟨b, hb⟩ = IsLocalization.mk' (Localization.Away f) c ⟨d, hd⟩

Tactic:
rw [IsLocalization.eq]

Result:
case intro.intro.mk.intro.intro.mk
R : Type u
inst✝ : CommRing R
f a b : R
hb : b ∈ Submonoid.powers f
c d : R
hd : d ∈ Submonoid.powers f
h_eq : const R a b (PrimeSpectrum.basicOpen f) ⋯ = const R c d (PrimeSpectrum.basicOpen f) ⋯
⊢ ∃ c_1, ↑c_1 * (↑⟨d, hd⟩ * a) = ↑c_1 * (↑⟨b, hb⟩ * c)
-- Mathlib/RingTheory/Frobenius.lean
lemma mk_apply (x) : Ideal.Quotient.mk Q (φ x) = x ^ Nat.card (R ⧸ Q.under R)

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ (Ideal.Quotient.mk Q) (φ x) = (Ideal.Quotient.mk Q) x ^ Nat.card (R ⧸ Ideal.under R Q)

Tactic:
rw [← map_pow, Ideal.Quotient.eq]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ φ x - x ^ Nat.card (R ⧸ Ideal.under R Q) ∈ Q

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
φ : S →ₐ[R] S
Q : Ideal S
H : φ.IsArithFrobAt Q
x : S
⊢ φ x - x ^ Nat.card (R ⧸ Ideal.under R Q) ∈ Q

Tactic:
exact H x

Result:
no goals
-- Mathlib/RingTheory/SimpleModule/Basic.lean
lemma isSemisimpleModule_biSup_of_isSemisimpleModule_submodule {s : Set ι} {p : ι → Submodule R M}
    (hp : ∀ i ∈ s, IsSemisimpleModule R (p i)) :
    IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
have hp₂ : ⨆ i ∈ s, p' i = ⊤ := by
  apply Submodule.map_injective_of_injective q.injective_subtype
  simp_rw [Submodule.map_top, Submodule.range_subtype, Submodule.map_iSup]
  exact biSup_congr fun i hi ↦ Submodule.map_comap_eq_of_le (hp₀ i hi)

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
hp₁ : ∀ i ∈ s, IsSemisimpleModule R ↥(p' i)
hp₂ : ⨆ i ∈ s, p' i = ⊤
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Proof state:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)

Tactic:
have hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype := fun i hi ↦ by
  simpa only [Submodule.range_subtype] using le_biSup _ hi

Result:
ι : Type u_1
R : Type u_2
inst✝² : Ring R
M : Type u_4
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s : Set ι
p : ι → Submodule R M
hp : ∀ i ∈ s, IsSemisimpleModule R ↥(p i)
q : Submodule R M := ⨆ i ∈ s, p i
p' : ι → Submodule R ↥q := fun i => Submodule.comap q.subtype (p i)
hp₀ : ∀ i ∈ s, p i ≤ LinearMap.range q.subtype
⊢ IsSemisimpleModule R ↥(⨆ i ∈ s, p i)
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem FiniteDimensional.of_locallyCompact_manifold
    [CompleteSpace 𝕜] (I : ModelWithCorners 𝕜 E H) [Nonempty M] [LocallyCompactSpace M] :
    FiniteDimensional 𝕜 E

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁵ : TopologicalSpace H
M : Type u_11
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst✝¹ : Nonempty M
inst✝ : LocallyCompactSpace M
⊢ FiniteDimensional 𝕜 E

Tactic:
have := LocallyCompactSpace.of_locallyCompact_manifold M I

Result:
E : Type u_8
𝕜 : Type u_9
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁵ : TopologicalSpace H
M : Type u_11
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst✝¹ : Nonempty M
inst✝ : LocallyCompactSpace M
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Proof state:
E : Type u_8
𝕜 : Type u_9
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
H : Type u_10
inst✝⁵ : TopologicalSpace H
M : Type u_11
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : CompleteSpace 𝕜
I : ModelWithCorners 𝕜 E H
inst✝¹ : Nonempty M
inst✝ : LocallyCompactSpace M
this : LocallyCompactSpace E
⊢ FiniteDimensional 𝕜 E

Tactic:
exact FiniteDimensional.of_locallyCompactSpace 𝕜

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Tilted.lean
lemma setIntegral_tilted' (f : α → ℝ) (g : α → E) {s : Set α} (hs : MeasurableSet s) :
    ∫ x in s, g x ∂(μ.tilted f) = ∫ x in s, (exp (f x) / ∫ x, exp (f x) ∂μ) • (g x) ∂μ

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : AEMeasurable f μ
this : AEMeasurable (fun x => rexp (f x) / ∫ (x : α), rexp (f x) ∂μ) μ
⊢ AEMeasurable (fun x => ↑⟨rexp (f x) / ∫ (x : α), rexp (f x) ∂μ, ⋯⟩) μ

Tactic:
simpa only [NNReal.coe_mk]

Result:
no goals

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ
g : α → E
s : Set α
hs : MeasurableSet s
hf : ¬AEMeasurable f μ
hf' : ¬Integrable (fun x => rexp (f x)) μ
⊢ 0 = ∫ (x : α) in s, (rexp (f x) / 0) • g x ∂μ

Tactic:
simp

Result:
no goals