harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Energy.lean
theorem coe_energy {𝕜 : Type*} [LinearOrderedField 𝕜] : (P.energy G : 𝕜) =
    (∑ uv ∈ P.parts.offDiag, (G.edgeDensity uv.1 uv.2 : 𝕜) ^ 2) / (#P.parts : 𝕜) ^ 2

Proof state:
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑(#P.parts) ^ 2) =
    (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2

Tactic:
norm_cast

Result:
no goals

Proof state:
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑(P.energy G) = (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2

Tactic:
rw [energy]

Result:
α : Type u_1
inst✝² : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝ : LinearOrderedField 𝕜
⊢ ↑((∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑(#P.parts) ^ 2) =
    (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2
-- Mathlib/RingTheory/WittVector/Basic.lean
theorem mul : mapFun f (x * y) = mapFun f x * mapFun f y

Proof state:
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x y : 𝕎 R
⊢ mapFun (⇑f) (x * y) = mapFun (⇑f) x * mapFun (⇑f) y

Tactic:
map_fun_tac

Result:
no goals
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem smul_eval [MulSemiringAction G S] (g : G) (f : S[X]) (x : S) :
    (g • f).eval x = g • f.eval (g⁻¹ • x)

Proof state:
S : Type u_3
inst✝² : CommSemiring S
G : Type u_4
inst✝¹ : Group G
inst✝ : MulSemiringAction G S
g : G
f : S[X]
x : S
⊢ eval x (g • f) = g • eval (g⁻¹ • x) f

Tactic:
rw [← smul_eval_smul, smul_inv_smul]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
lemma dist_top_of_ne (h : u ≠ v) : (⊤ : SimpleGraph V).dist u v = 1

Proof state:
V : Type u_1
u v : V
h : u ≠ v
⊢ ⊤.dist u v = 1

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b)

Proof state:
b : Bool
⊢ ~~~ofBool b = ofBool !b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Logic/Function/DependsOn.lean
/-- A constant function does not depend on any variable. -/
lemma dependsOn_const (b : β) : DependsOn (fun _ : Π i, α i ↦ b) ∅

Proof state:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
b : β
⊢ DependsOn (fun x => b) ∅

Tactic:
simp [DependsOn]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
@[simp]
lemma monovaryOn_inv_right₀ (hg : ∀ i ∈ s, 0 < g i) : MonovaryOn f g⁻¹ s ↔ AntivaryOn f g s :=
  forall₂_swap.trans <| forall₄_congr fun i hi j hj ↦ by simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrderedSemifield α
inst✝ : LinearOrderedSemifield β
s : Set ι
f : ι → α
g : ι → β
hg : ∀ i ∈ s, 0 < g i
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
⊢ g⁻¹ j < g⁻¹ i → f j ≤ f i ↔ g i < g j → f j ≤ f i

Tactic:
simp [inv_lt_inv₀ (hg _ hj) (hg _ hi)]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Basic.lean
theorem val_le_one_or_val_inv_le_one (v : Valuation K Γ₀) (x : K) : v x ≤ 1 ∨ v x⁻¹ ≤ 1

Proof state:
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
by_cases h : x = 0

Result:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Proof state:
case neg
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : ¬x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
simp only [← one_le_val_iff v h, le_total]

Result:
no goals

Proof state:
case pos
K : Type u_1
inst✝¹ : DivisionRing K
Γ₀ : Type u_4
inst✝ : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
x : K
h : x = 0
⊢ v x ≤ 1 ∨ v x⁻¹ ≤ 1

Tactic:
simp only [h, _root_.map_zero, zero_le', inv_zero, or_self]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_iff_not_affineIndependent {p : Fin 3 → P} :
    Collinear k (Set.range p) ↔ ¬AffineIndependent k p

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
p : Fin 3 → P
⊢ Collinear k (Set.range p) ↔ ¬AffineIndependent k p

Tactic:
rw [collinear_iff_finrank_le_one,
  finrank_vectorSpan_le_iff_not_affineIndependent k p (Fintype.card_fin 3)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem bne_self_eq_false [BEq α] [LawfulBEq α] (a : α) : (a != a) = false

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
⊢ (a != a) = false

Tactic:
simp [bne]

Result:
no goals
-- Mathlib/Algebra/Ring/Centralizer.lean
theorem add_mem_centralizer [Distrib M] (ha : a ∈ centralizer S) (hb : b ∈ centralizer S) :
    a + b ∈ centralizer S := fun c hc => by rw [add_mul, mul_add, ha c hc, hb c hc]

Proof state:
M : Type u_1
S : Set M
a b : M
inst✝ : Distrib M
ha : a ∈ S.centralizer
hb : b ∈ S.centralizer
c : M
hc : c ∈ S
⊢ c * (a + b) = (a + b) * c

Tactic:
rw [add_mul, mul_add, ha c hc, hb c hc]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Ultra.lean
theorem IsUltrametricDist.of_normedAlgebra' [SeminormedRing L] [NormOneClass L] [NormedAlgebra K L]
    [h : IsUltrametricDist L] : IsUltrametricDist K :=
  ⟨fun x y z => by
    simpa using h.dist_triangle_max (algebraMap K L x) (algebraMap K L y) (algebraMap K L z)⟩

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : NormedField K
inst✝² : SeminormedRing L
inst✝¹ : NormOneClass L
inst✝ : NormedAlgebra K L
h : IsUltrametricDist L
x y z : K
⊢ dist x z ≤ dist x y ⊔ dist y z

Tactic:
simpa using h.dist_triangle_max (algebraMap K L x) (algebraMap K L y) (algebraMap K L z)

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_affine_Ico {a : α} (h : 0 < a) (b c d : α) :
    (a * · + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
⊢ (fun x => x + b) '' ((fun x => a * x) '' Ico c d) = Ico (a * c + b) (a * d + b)

Tactic:
rw [image_mul_left_Ico h, image_add_const_Ico]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
h : 0 < a
b c d : α
this : (fun x => x + b) '' ((fun x => a * x) '' Ico c d) = Ico (a * c + b) (a * d + b)
⊢ (fun x => a * x + b) '' Ico c d = Ico (a * c + b) (a * d + b)

Tactic:
rwa [Set.image_image] at this

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_eq_ncard_iff_ncard_diff_eq_ncard_diff (hs : s.Finite

Proof state:
α : Type u_1
s t : Set α
hs : autoParam s.Finite _auto✝
ht : autoParam t.Finite _auto✝
⊢ s.ncard = t.ncard ↔ (s \ t).ncard = (t \ s).ncard

Tactic:
rw [← ncard_inter_add_ncard_diff_eq_ncard s t hs, ← ncard_inter_add_ncard_diff_eq_ncard t s ht,
  inter_comm, add_right_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.le_of_eq_2 (u v : Nat) : u = v → v ≤ u

Proof state:
u v : Nat
⊢ u = v → v ≤ u

Tactic:
omega

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
private lemma mu'_eq_sum_Ioc_of_ne (h : a ≠ b) : mu' 𝕜 a b = -∑ x ∈ Ioc a b, mu' 𝕜 x b

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
h : a ≠ b
⊢ (IncidenceAlgebra.mu' 𝕜) a b = -∑ x ∈ Ioc a b, (IncidenceAlgebra.mu' 𝕜) x b

Tactic:
rw [mu'_apply, if_neg h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Linear.lean
@[simp]
lemma opcyclesMap'_smul :
    opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Tactic:
have γ : RightHomologyMapData φ h₁ h₂ := default

Result:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Proof state:
R : Type u_1
C : Type u_2
inst✝³ : Semiring R
inst✝² : Category.{u_3, u_2} C
inst✝¹ : Preadditive C
inst✝ : Linear R C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
a : R
γ : RightHomologyMapData φ h₁ h₂
⊢ opcyclesMap' (a • φ) h₁ h₂ = a • opcyclesMap' φ h₁ h₂

Tactic:
simp only [(γ.smul a).opcyclesMap'_eq, RightHomologyMapData.smul_φQ, γ.opcyclesMap'_eq]

Result:
no goals
-- Mathlib/Logic/Basic.lean
theorem ite_prop_iff_and : (if P then Q else R) ↔ ((P → Q) ∧ (¬ P → R))

Proof state:
P Q R : Prop
inst✝ : Decidable P
⊢ (if P then Q else R) ↔ (P → Q) ∧ (¬P → R)

Tactic:
by_cases p : P <;> simp [p]

Result:
no goals
-- Mathlib/Computability/Partrec.lean
theorem comp {f : β →. σ} {g : α → β} (hf : Partrec f) (hg : Computable g) :
    Partrec fun a => f (g a) :=
  (hf.comp hg).of_eq fun n => by simp; rcases e : decode (α := α) n with - | a <;> simp [e, encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (((↑(decode n)).bind fun a => Part.some (encode (g a))).bind fun n =>
      (↑(decode n)).bind fun a => Part.map encode (f a)) =
    (↑(decode n)).bind fun a => Part.map encode (f (g a))

Tactic:
rcases e : decode (α := α) n with - | a <;> simp [e, encodek]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (do
      let n ← (↑(decode n)).bind fun a => Part.map encode (↑g a)
      (↑(decode n)).bind fun a => Part.map encode (f a)) =
    (↑(decode n)).bind fun a => Part.map encode ((fun a => f (g a)) a)

Tactic:
simp

Result:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
f : β →. σ
g : α → β
hf : Partrec f
hg : Computable g
n : ℕ
⊢ (((↑(decode n)).bind fun a => Part.some (encode (g a))).bind fun n =>
      (↑(decode n)).bind fun a => Part.map encode (f a)) =
    (↑(decode n)).bind fun a => Part.map encode (f (g a))
-- Mathlib/Algebra/Homology/TotalComplex.lean
lemma d₂_eq (i₁ : I₁) {i₂ i₂' : I₂} (h : c₂.Rel i₂ i₂') (i₁₂ : I₁₂)
    (h' : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂'⟩ = i₁₂) :
    K.d₂ c₁₂ i₁ i₂ i₁₂ = ComplexShape.ε₂ c₁ c₂ c₁₂ ⟨i₁, i₂⟩ • ((K.X i₁).d i₂ i₂' ≫
    K.toGradedObject.ιMapObj (ComplexShape.π c₁ c₂ c₁₂) ⟨i₁, i₂'⟩ i₁₂ h')

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ i₂' : I₂
h : c₂.Rel i₂ i₂'
i₁₂ : I₁₂
h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) • (K.X i₁).d i₂ i₂' ≫ K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h'

Tactic:
rw [d₂_eq' K c₁₂ i₁ h i₁₂, K.toGradedObject.ιMapObjOrZero_eq]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem add_top_iff_ne_bot {x : EReal} : x + ⊤ = ⊤ ↔ x ≠ ⊥

Proof state:
x : EReal
⊢ x + ⊤ = ⊤ ↔ x ≠ ⊥

Tactic:
rw [add_comm, top_add_iff_ne_bot]

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem RegularSpace.t3Space_iff_t0Space [RegularSpace X] : T3Space X ↔ T0Space X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
⊢ T3Space X ↔ T0Space X

Tactic:
constructor <;> intro <;> infer_instance

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem Filter.Tendsto.atTop_mul {C : 𝕜} (hC : 0 < C) (hf : Tendsto f l atTop)
    (hg : Tendsto g l (𝓝 C)) : Tendsto (fun x => f x * g x) l atTop

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atTop

Tactic:
refine tendsto_atTop_mono' _ ?_ (hf.atTop_mul_const (half_pos hC))

Result:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ (fun x => f x * (C / 2)) ≤ᶠ[l] fun x => f x * g x

Proof state:
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ (fun x => f x * (C / 2)) ≤ᶠ[l] fun x => f x * g x

Tactic:
filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0]
  with x hg hf using mul_le_mul_of_nonneg_left hg.le hf

Result:
no goals
-- Mathlib/LinearAlgebra/Projectivization/Constructions.lean
lemma cross_mk_of_cross_eq_zero {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0)
    (h : crossProduct v w = 0) :
    cross (mk F v hv) (mk F w hw) = mk F v hv

Proof state:
F : Type u_1
inst✝¹ : Field F
inst✝ : DecidableEq F
v w : Fin 3 → F
hv : v ≠ 0
hw : w ≠ 0
h : (crossProduct v) w = 0
⊢ (mk F v hv).cross (mk F w hw) = mk F v hv

Tactic:
rw [cross_mk, dif_pos h]

Result:
no goals
-- Mathlib/NumberTheory/Bernoulli.lean
theorem bernoulli'_two : bernoulli' 2 = 1 / 6

Proof state:
⊢ 1 - ∑ k ∈ range 2, ↑(Nat.choose 2 k) / (↑2 - ↑k + 1) * bernoulli' k = 1 / 6

Tactic:
norm_num [sum_range_succ, sum_range_succ, sum_range_zero]

Result:
no goals

Proof state:
⊢ bernoulli' 2 = 1 / 6

Tactic:
rw [bernoulli'_def]

Result:
⊢ 1 - ∑ k ∈ range 2, ↑(Nat.choose 2 k) / (↑2 - ↑k + 1) * bernoulli' k = 1 / 6
-- Mathlib/Data/Nat/Fib/Basic.lean
theorem fib_dvd (m n : ℕ) (h : m ∣ n) : fib m ∣ fib n

Proof state:
m n : ℕ
h : m ∣ n
⊢ fib m ∣ fib n

Tactic:
rwa [gcd_eq_left_iff_dvd, ← fib_gcd, gcd_eq_left_iff_dvd.mp]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem IsCompl.prod_mul_prod {s t : Finset α} (h : IsCompl s t) (f : α → β) :
    (∏ i ∈ s, f i) * ∏ i ∈ t, f i = ∏ i, f i :=
  (Finset.prod_disjUnion h.disjoint).symm.trans <| by
    classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x ∈ s.disjUnion t ⋯, f x = ∏ i : α, f i

Tactic:
classical rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]; rfl

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x ∈ ⊤, f x = ∏ i : α, f i

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x ∈ s.disjUnion t ⋯, f x = ∏ i : α, f i

Tactic:
rw [Finset.disjUnion_eq_union, ← Finset.sup_eq_union, h.sup_eq_top]

Result:
α : Type u_3
β : Type u_4
inst✝¹ : Fintype α
inst✝ : CommMonoid β
s t : Finset α
h : IsCompl s t
f : α → β
⊢ ∏ x ∈ ⊤, f x = ∏ i : α, f i
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.upperBound?_least [@TransCmp α cmp] [IsCut cmp cut] (ht : Ordered cmp t)
    (H : t.upperBound? cut = some x) (hy : y ∈ t)
    (xy : cmp y x = .lt) (hx : cut x = .lt) : cut y = .gt :=
  ht.upperBound?_least_ub (by nofun) H hy hx xy

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsCut cmp cut
ht : Ordered cmp t
H : upperBound? cut t = some x
hy : y ∈ t
xy : cmp y x = Ordering.lt
hx : cut x = Ordering.lt
⊢ ∀ {x : α}, none = some x → All (fun x_1 => cmpLT cmp x_1 x) t

Tactic:
nofun

Result:
no goals
-- Mathlib/Algebra/Lie/Abelian.lean
theorem maxTrivEquiv_of_refl_eq_refl :
    maxTrivEquiv (LieModuleEquiv.refl : M ≃ₗ⁅R,L⁆ M) = LieModuleEquiv.refl

Proof state:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
m✝ : ↥(maxTrivSubmodule R L M)
⊢ ↑((maxTrivEquiv LieModuleEquiv.refl) m✝) = ↑(LieModuleEquiv.refl m✝)

Tactic:
simp only [coe_maxTrivEquiv_apply, LieModuleEquiv.refl_apply]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
⊢ maxTrivEquiv LieModuleEquiv.refl = LieModuleEquiv.refl

Tactic:
ext

Result:
case h.a
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
inst✝ : LieModule R L M
m✝ : ↥(maxTrivSubmodule R L M)
⊢ ↑((maxTrivEquiv LieModuleEquiv.refl) m✝) = ↑(LieModuleEquiv.refl m✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
    (cons a x) ||| (cons b y) = cons (a || b) (x ||| y)

Proof state:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x ||| cons b y).getLsbD i = (cons (a || b) (x ||| y)).getLsbD i

Tactic:
simp [cons]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
a b : Bool
⊢ cons a x ||| cons b y = cons (a || b) (x ||| y)

Tactic:
ext i

Result:
case pred
w : Nat
x y : BitVec w
a b : Bool
i : Nat
a✝ : i < w + 1
⊢ (cons a x ||| cons b y).getLsbD i = (cons (a || b) (x ||| y)).getLsbD i
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap (f : L →ₐ[F] E) (B : IntermediateField F L) :
    relfinrank (A.comap f) B = relfinrank A (B.map f)

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
L : Type w
inst✝¹ : Field L
inst✝ : Algebra F L
A : IntermediateField F E
f : L →ₐ[F] E
B : IntermediateField F L
⊢ (comap f A).relfinrank B = A.relfinrank (map f B)

Tactic:
simpa using congr(toNat $(lift_relrank_comap A f B))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem?_insertIdx_of_lt {l : List α} {x : α} {n k : Nat} (h : k < n) :
    (insertIdx n x l)[k]? = l[k]?

Proof state:
α : Type u
l : List α
x : α
n k : Nat
h : k < n
⊢ (insertIdx n x l)[k]? = l[k]?

Tactic:
rw [getElem?_insertIdx, if_pos h]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/NonUnital.lean
lemma cfcₙ_nonpos_iff (f : R → R) (a : A) (hf : ContinuousOn f (σₙ R a)

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.1103482) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ cfcₙ f a ≤ 0 ↔ ∀ x ∈ σₙ R a, f x ≤ 0

Tactic:
simp_rw [← neg_nonneg, ← cfcₙ_neg]

Result:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.1103482) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfcₙ (fun x => -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹⁶ : OrderedCommRing R
inst✝¹⁵ : Nontrivial R
inst✝¹⁴ : StarRing R
inst✝¹³ : MetricSpace R
inst✝¹² : IsTopologicalRing R
inst✝¹¹ : ContinuousStar R
inst✝¹⁰ : ∀ (α : Type ?u.1103482) [inst : Zero α] [inst_1 : TopologicalSpace α], StarOrderedRing C(α, R)₀
inst✝⁹ : TopologicalSpace A
inst✝⁸ : NonUnitalRing A
inst✝⁷ : StarRing A
inst✝⁶ : PartialOrder A
inst✝⁵ : StarOrderedRing A
inst✝⁴ : Module R A
inst✝³ : IsScalarTower R A A
inst✝² : SMulCommClass R A A
inst✝¹ : NonUnitalContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
f : R → R
a : A
hf : autoParam (ContinuousOn f (σₙ R a)) _auto✝
h0 : autoParam (f 0 = 0) _auto✝
ha : autoParam (p a) _auto✝
⊢ 0 ≤ cfcₙ (fun x => -f x) a ↔ ∀ x ∈ σₙ R a, 0 ≤ -f x

Tactic:
exact cfcₙ_nonneg_iff (fun x ↦ -f x) a

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem option_casesOn {o : α → Option β} {f : α → σ} {g : α → β → σ} (ho : Primrec o)
    (hf : Primrec f) (hg : Primrec₂ g) :
    @Primrec _ σ _ _ fun a => Option.casesOn (o a) (f a) (g a) :=
  encode_iff.1 <|
    (nat_casesOn (encode_iff.2 ho) (encode_iff.2 hf) <|
          pred.comp₂ <|
            Primrec₂.encode_iff.2 <|
              (Primrec₂.nat_iff'.1 hg).comp₂ ((@Primrec.encode α _).comp fst).to₂
                Primrec₂.right).of_eq
      fun a => by rcases o a with - | b <;> simp [encodek]

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
inst✝² : Primcodable α
inst✝¹ : Primcodable β
inst✝ : Primcodable σ
o : α → Option β
f : α → σ
g : α → β → σ
ho : Primrec o
hf : Primrec f
hg : Primrec₂ g
a : α
⊢ (Nat.casesOn (encode (o a)) (encode (f a)) fun b =>
      (encode ((decode (encode (a, b).1)).bind fun a => Option.map (g a) (decode b))).pred) =
    encode (Option.casesOn (o a) (f a) (g a))

Tactic:
rcases o a with - | b <;> simp [encodek]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem measure_diff (h : s₂ ⊆ s₁) (h₂ : NullMeasurableSet s₂ μ) (h_fin : μ s₂ ≠ ∞) :
    μ (s₁ \ s₂) = μ s₁ - μ s₂

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s₁ s₂ : Set α
h : s₂ ⊆ s₁
h₂ : NullMeasurableSet s₂ μ
h_fin : μ s₂ ≠ ⊤
⊢ μ (s₁ \ s₂) = μ s₁ - μ s₂

Tactic:
rw [measure_diff' _ h₂ h_fin, union_eq_self_of_subset_right h]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem sSup_inf_sSup : sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, (p : α × α).1 ⊓ p.2

Proof state:
α : Type u
inst✝ : Frame α
s t : Set α
⊢ sSup s ⊓ sSup t = ⨆ p ∈ s ×ˢ t, p.1 ⊓ p.2

Tactic:
simp only [sSup_eq_iSup, biSup_inf_biSup]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Reduced.lean
lemma linearIndependent_iff_coxeterWeightIn_ne_four :
    LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeightIn S i j ≠ 4

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹¹ : CommRing R
inst✝¹⁰ : AddCommGroup M
inst✝⁹ : Module R M
inst✝⁸ : AddCommGroup N
inst✝⁷ : Module R N
P : RootPairing ι R M N
S : Type u_5
i j : ι
inst✝⁶ : Finite ι
inst✝⁵ : CharZero R
inst✝⁴ : NoZeroSMulDivisors R M
inst✝³ : LinearOrderedCommRing S
inst✝² : Algebra S R
inst✝¹ : FaithfulSMul S R
inst✝ : P.IsValuedIn S
⊢ LinearIndependent R ![P.root i, P.root j] ↔ P.coxeterWeightIn S i j ≠ 4

Tactic:
rw [linearIndependent_iff_coxeterWeight_ne_four, ← P.algebraMap_coxeterWeightIn S,
  ← map_ofNat (algebraMap S R), (algebraMap_injective S R).ne_iff]

Result:
no goals