harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/NAry.lean
theorem image_image₂_distrib_left {g : γ → δ} {f' : α' → β → δ} {g' : α → α'}
    (h_distrib : ∀ a b, g (f a b) = f' (g' a) b) :
    (image₂ f s t).image g = image₂ f' (s.image g') t :=
  coe_injective <| by
    push_cast
    exact image_image2_distrib_left h_distrib

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ ↑(image g (image₂ f s t)) = ↑(image₂ f' (image g' s) t)

Tactic:
push_cast

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ g '' image2 f ↑s ↑t = image2 f' (g' '' ↑s) ↑t

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
γ : Type u_5
δ : Type u_7
inst✝² : DecidableEq α'
inst✝¹ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
g : γ → δ
f' : α' → β → δ
g' : α → α'
h_distrib : ∀ (a : α) (b : β), g (f a b) = f' (g' a) b
⊢ g '' image2 f ↑s ↑t = image2 f' (g' '' ↑s) ↑t

Tactic:
exact image_image2_distrib_left h_distrib

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem eq_self_sub_one {n : Nat} : n = n - 1 ↔ n = 0

Proof state:
n : Nat
⊢ n = n - 1 ↔ n = 0

Tactic:
cases n <;> simp [add_one_ne]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem properDivisors_one : properDivisors 1 = ∅

Proof state:
⊢ properDivisors 1 = ∅

Tactic:
rw [properDivisors, Ico_self, filter_empty]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem sum_apply {ι : Type*} (s : Finset ι) (f : ι → α →ᵇ β) (a : α) :
    (∑ i ∈ s, f i) a = ∑ i ∈ s, f i a

Proof state:
α : Type u
β : Type v
inst✝⁴ : TopologicalSpace α
inst✝³ : PseudoMetricSpace β
inst✝² : AddCommMonoid β
inst✝¹ : BoundedAdd β
inst✝ : ContinuousAdd β
ι : Type u_2
s : Finset ι
f : ι → α →ᵇ β
a : α
⊢ (∑ i ∈ s, f i) a = ∑ i ∈ s, (f i) a

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coxeterWeight_swap : coxeterWeight P i j = coxeterWeight P j i

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
i j : ι
⊢ P.coxeterWeight i j = P.coxeterWeight j i

Tactic:
simp only [coxeterWeight, mul_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean
theorem invOf_ι (m : M) [Invertible (Q m)] [Invertible (ι Q m)] :
    ⅟ (ι Q m) = ι Q (⅟ (Q m) • m)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
m : M
inst✝¹ : Invertible (Q m)
inst✝ : Invertible ((ι Q) m)
this : Invertible ((ι Q) m) := invertibleιOfInvertible Q m
⊢ ⅟((ι Q) m) = (ι Q) (⅟(Q m) • m)

Tactic:
convert (rfl : ⅟ (ι Q m) = _)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
m : M
inst✝¹ : Invertible (Q m)
inst✝ : Invertible ((ι Q) m)
⊢ ⅟((ι Q) m) = (ι Q) (⅟(Q m) • m)

Tactic:
letI := invertibleιOfInvertible Q m

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : QuadraticForm R M
m : M
inst✝¹ : Invertible (Q m)
inst✝ : Invertible ((ι Q) m)
this : Invertible ((ι Q) m) := invertibleιOfInvertible Q m
⊢ ⅟((ι Q) m) = (ι Q) (⅟(Q m) • m)
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem L1.integral_of_fun_eq_integral {f : α → G} (hf : Integrable f μ) :
    ∫ a, (hf.toL1 f) a ∂μ = ∫ a, f a ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ

Tactic:
simp [MeasureTheory.integral, hG]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
⊢ ∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : CompleteSpace G
⊢ ∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : CompleteSpace G
⊢ ∫ (a : α), ↑↑(Integrable.toL1 f hf) a ∂μ = ∫ (a : α), f a ∂μ

Tactic:
simp only [MeasureTheory.integral, hG, L1.integral]

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf_1 : Integrable (fun a => ↑↑(Integrable.toL1 f hf) a) μ then
        integralCLM (Integrable.toL1 (fun a => ↑↑(Integrable.toL1 f hf) a) hf_1)
      else 0
    else 0) =
    if h : True then if hf : Integrable (fun a => f a) μ then integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hf : Integrable f μ
hG : CompleteSpace G
⊢ (if h : True then
      if hf_1 : Integrable (fun a => ↑↑(Integrable.toL1 f hf) a) μ then
        integralCLM (Integrable.toL1 (fun a => ↑↑(Integrable.toL1 f hf) a) hf_1)
      else 0
    else 0) =
    if h : True then if hf : Integrable (fun a => f a) μ then integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
    else 0

Tactic:
exact setToFun_toL1 (dominatedFinMeasAdditive_weightedSMul μ) hf

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem ite_compl (t s s' : Set α) : tᶜ.ite s s' = t.ite s' s

Proof state:
α : Type u
t s s' : Set α
⊢ tᶜ.ite s s' = t.ite s' s

Tactic:
rw [Set.ite, Set.ite, diff_compl, union_comm, diff_eq]

Result:
no goals
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
@[simp]
lemma cauchyBound_X : cauchyBound (X : K[X]) = 1

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
⊢ X.cauchyBound = 1

Tactic:
simp [cauchyBound]

Result:
no goals
-- Mathlib/Algebra/BrauerGroup/Defs.lean
@[trans]
lemma trans {A B C : CSA K} (hAB : IsBrauerEquivalent A B) (hBC : IsBrauerEquivalent B C) :
    IsBrauerEquivalent A C

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgebraCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgebraCat
⊢ IsBrauerEquivalent A C

Tactic:
exact ⟨p * n, m * q, by simp_all, by simp_all,
  ⟨reindexAlgEquiv _ _ finProdFinEquiv |>.symm.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
  iso1.mapMatrix (m := Fin p)|>.trans <| compAlgEquiv _ _ _ _|>.trans <|
  reindexAlgEquiv K B (.prodComm (Fin p) (Fin m))|>.trans <| compAlgEquiv _ _ _ _|>.symm.trans <|
  iso2.mapMatrix.trans <| compAlgEquiv _ _ _ _|>.trans <| reindexAlgEquiv _ _ finProdFinEquiv⟩⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hBC : IsBrauerEquivalent B C
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨p, q, hp, hq, ⟨iso2⟩⟩ := hBC

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgebraCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgebraCat
⊢ IsBrauerEquivalent A C

Proof state:
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgebraCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgebraCat
⊢ p * n ≠ 0

Tactic:
simp_all

Result:
no goals

Proof state:
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hAB : IsBrauerEquivalent A B
hBC : IsBrauerEquivalent B C
⊢ IsBrauerEquivalent A C

Tactic:
obtain ⟨n, m, hn, hm, ⟨iso1⟩⟩ := hAB

Result:
case intro.intro.intro.intro.intro
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
hBC : IsBrauerEquivalent B C
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
⊢ IsBrauerEquivalent A C

Proof state:
K : Type u
inst✝ : Field K
A : CSA K
B : CSA K
C : CSA K
n m : ℕ
hn : n ≠ 0
hm : m ≠ 0
iso1 : Matrix (Fin n) (Fin n) ↑A.toAlgebraCat ≃ₐ[K] Matrix (Fin m) (Fin m) ↑B.toAlgebraCat
p q : ℕ
hp : p ≠ 0
hq : q ≠ 0
iso2 : Matrix (Fin p) (Fin p) ↑B.toAlgebraCat ≃ₐ[K] Matrix (Fin q) (Fin q) ↑C.toAlgebraCat
⊢ m * q ≠ 0

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem transpose_sub [Sub α] (M : Matrix m n α) (N : Matrix m n α) : (M - N)ᵀ = Mᵀ - Nᵀ

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M - N)ᵀ i✝ j✝ = (Mᵀ - Nᵀ) i✝ j✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
⊢ (M - N)ᵀ = Mᵀ - Nᵀ

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
α : Type v
inst✝ : Sub α
M N : Matrix m n α
i✝ : n
j✝ : m
⊢ (M - N)ᵀ i✝ j✝ = (Mᵀ - Nᵀ) i✝ j✝
-- Mathlib/Analysis/LocallyConvex/WithSeminorms.lean
theorem WithSeminorms.continuous_seminorm {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p)
    (i : ι) : Continuous (p i)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
⊢ Continuous ⇑(p i)

Tactic:
have := hp.topologicalAddGroup

Result:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous ⇑(p i)

Proof state:
𝕜 : Type u_1
E : Type u_5
ι : Type u_8
inst✝³ : NormedField 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Nonempty ι
t : TopologicalSpace E
p : SeminormFamily 𝕜 E ι
hp : WithSeminorms p
i : ι
this : IsTopologicalAddGroup E
⊢ Continuous ⇑(p i)

Tactic:
exact continuous_iInf_dom (@continuous_norm _ (p i).toSeminormedAddGroup)

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- The function `completedLFunction₀ Φ` is differentiable. -/
lemma differentiable_completedLFunction₀ (Φ : ZMod N → ℂ) :
    Differentiable ℂ (completedLFunction₀ Φ)

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ fun y => ↑N ^ (-y)

Tactic:
fun_prop

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
⊢ Differentiable ℂ (completedLFunction₀ Φ)

Tactic:
refine .add ?_ ?_ <;>
refine .mul (by fun_prop) (.sum fun i _ ↦ .const_mul ?_ _)

Result:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
i : ZMod N
x✝ : i ∈ Finset.univ
⊢ Differentiable ℂ (completedHurwitzZetaEven₀ (toAddCircle i))

case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
i : ZMod N
x✝ : i ∈ Finset.univ
⊢ Differentiable ℂ (completedHurwitzZetaOdd (toAddCircle i))

Proof state:
case refine_1
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
i : ZMod N
x✝ : i ∈ Finset.univ
⊢ Differentiable ℂ (completedHurwitzZetaEven₀ (toAddCircle i))

case refine_2
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
i : ZMod N
x✝ : i ∈ Finset.univ
⊢ Differentiable ℂ (completedHurwitzZetaOdd (toAddCircle i))

Tactic:
exacts [differentiable_completedHurwitzZetaEven₀ _, differentiable_completedHurwitzZetaOdd _]

Result:
no goals
-- Mathlib/Algebra/Order/Monovary.lean
/-- Two functions antivary iff the rearrangement inequality holds. -/
lemma antivaryOn_iff_smul_rearrangement :
    AntivaryOn f g s ↔
      ∀ ⦃i⦄, i ∈ s → ∀ ⦃j⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i :=
  monovaryOn_toDual_right.symm.trans <| by rw [monovaryOn_iff_smul_rearrangement]; rfl

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄,
      i ∈ s →
        ∀ ⦃j : ι⦄,
          j ∈ s →
            f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤
              f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f (⇑OrderDual.toDual ∘ g) s ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i

Tactic:
rw [monovaryOn_iff_smul_rearrangement]

Result:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : LinearOrderedRing α
inst✝² : LinearOrderedAddCommGroup β
inst✝¹ : Module α β
inst✝ : OrderedSMul α β
f : ι → α
g : ι → β
s : Set ι
⊢ (∀ ⦃i : ι⦄,
      i ∈ s →
        ∀ ⦃j : ι⦄,
          j ∈ s →
            f i • (⇑OrderDual.toDual ∘ g) j + f j • (⇑OrderDual.toDual ∘ g) i ≤
              f i • (⇑OrderDual.toDual ∘ g) i + f j • (⇑OrderDual.toDual ∘ g) j) ↔
    ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i • g i + f j • g j ≤ f i • g j + f j • g i
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem connectedComponentEquiv_symm (φ : G ≃g G') :
    φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm

Proof state:
case H.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
x✝ : G'.ConnectedComponent
a✝ : V'
⊢ φ.symm.connectedComponentEquiv (Quot.mk G'.Reachable a✝) = φ.connectedComponentEquiv.symm (Quot.mk G'.Reachable a✝)

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
⊢ φ.symm.connectedComponentEquiv = φ.connectedComponentEquiv.symm

Tactic:
ext ⟨_⟩

Result:
case H.mk
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
φ : G ≃g G'
x✝ : G'.ConnectedComponent
a✝ : V'
⊢ φ.symm.connectedComponentEquiv (Quot.mk G'.Reachable a✝) = φ.connectedComponentEquiv.symm (Quot.mk G'.Reachable a✝)
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem piecewise_ae_eq_of_ae_eq_set [DecidablePred (· ∈ s)] [DecidablePred (· ∈ t)]
    (hst : s =ᵐ[μ] t) : s.piecewise f g =ᵐ[μ] t.piecewise f g :=
  hst.mem_iff.mono fun x hx => by simp [piecewise, hx]

Proof state:
α : Type u_2
β : Type u_3
inst✝² : MeasurableSpace α
μ : Measure α
s t : Set α
f g : α → β
inst✝¹ : DecidablePred fun x => x ∈ s
inst✝ : DecidablePred fun x => x ∈ t
hst : s =ᶠ[ae μ] t
x : α
hx : x ∈ s ↔ x ∈ t
⊢ s.piecewise f g x = t.piecewise f g x

Tactic:
simp [piecewise, hx]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/Basic.lean
theorem map_comap_eq_self_of_surjective
    {f : R →+* S} (hf : Function.Surjective f) (t : Subsemiring S) : (t.comap f).map f = t :=
  map_comap_eq_self <| by simp [hf]

Proof state:
R : Type u
S : Type v
inst✝¹ : NonAssocSemiring R
inst✝ : NonAssocSemiring S
f : R →+* S
hf : Function.Surjective ⇑f
t : Subsemiring S
⊢ t ≤ f.rangeS

Tactic:
simp [hf]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
lemma degree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : degree p ≤ degree q

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
rw [mul_ne_zero_iff] at h2

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h1 : p ∣ q
h2 : q ≠ 0
⊢ p.degree ≤ q.degree

Tactic:
rcases h1 with ⟨q, rfl⟩

Result:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p * q ≠ 0
⊢ p.degree ≤ (p * q).degree

Proof state:
case intro
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p q : R[X]
h2 : p ≠ 0 ∧ q ≠ 0
⊢ p.degree ≤ (p * q).degree

Tactic:
exact degree_le_mul_left p h2.2

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_le_one₀ (ha₀ : 0 < a) (ha₁ : a ≤ 1) (hn : 0 ≤ n) : a ^ n ≤ 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
n : ℤ
ha₀ : 0 < a
ha₁ : a ≤ 1
hn : 0 ≤ n
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_anti₀ ha₀ ha₁ hn

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/HasPullback.lean
theorem pushoutComparison_map_desc (f : X ⟶ Y) (g : X ⟶ Z) [HasPushout f g]
    [HasPushout (G.map f) (G.map g)] {W : C} {h : Y ⟶ W} {k : Z ⟶ W} (w : f ≫ h = g ≫ k) :
    pushoutComparison G f g ≫ G.map (pushout.desc _ _ w) =
      pushout.desc (G.map h) (G.map k) (by simp only [← G.map_comp, w])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ pushoutComparison G f g ≫ G.map (pushout.desc h k w) = pushout.desc (G.map h) (G.map k) ⋯

Tactic:
ext <;> simp [← G.map_comp]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
W✝ X Y Z : C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
G : C ⥤ D
f : X ⟶ Y
g : X ⟶ Z
inst✝¹ : HasPushout f g
inst✝ : HasPushout (G.map f) (G.map g)
W : C
h : Y ⟶ W
k : Z ⟶ W
w : f ≫ h = g ≫ k
⊢ G.map f ≫ G.map h = G.map g ≫ G.map k

Tactic:
simp only [← G.map_comp, w]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Group.lean
theorem pairwise_disjoint_Ico_add_intCast :
    Pairwise (Disjoint on fun n : ℤ => Ico (a + n) (a + n + 1))

Proof state:
α : Type u_1
inst✝ : OrderedRing α
a : α
⊢ Pairwise (Disjoint on fun n => Ico (a + ↑n) (a + ↑n + 1))

Tactic:
simpa only [zsmul_one, Int.cast_add, Int.cast_one, ← add_assoc] using
  pairwise_disjoint_Ico_add_zsmul a (1 : α)

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem discrete_isNormal : (@discrete C _).IsNormal :=
  { wide := fun c => by constructor
    conj := fun f γ hγ => by
      cases hγ
      simp only [inv_eq_inv, Category.id_comp, IsIso.inv_hom_id]; constructor }

Proof state:
case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ 𝟙 d✝ ∈ discrete.arrows d✝ d✝

Tactic:
constructor

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
c : C
⊢ 𝟙 c ∈ discrete.arrows c c

Tactic:
constructor

Result:
no goals

Proof state:
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
γ : c✝ ⟶ c✝
hγ : γ ∈ discrete.arrows c✝ c✝
⊢ Groupoid.inv f ≫ γ ≫ f ∈ discrete.arrows d✝ d✝

Tactic:
cases hγ

Result:
case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ Groupoid.inv f ≫ 𝟙 c✝ ≫ f ∈ discrete.arrows d✝ d✝

Proof state:
case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ Groupoid.inv f ≫ 𝟙 c✝ ≫ f ∈ discrete.arrows d✝ d✝

Tactic:
simp only [inv_eq_inv, Category.id_comp, IsIso.inv_hom_id]

Result:
case id
C : Type u
inst✝ : Groupoid C
c✝ d✝ : C
f : c✝ ⟶ d✝
⊢ 𝟙 d✝ ∈ discrete.arrows d✝ d✝
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma toAffine_slope_of_ne {P Q : Fin 3 → F} (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hx : P x * Q z ≠ Q x * P z) :
    W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) =
      (P y * Q z - Q y * P z) / (P x * Q z - Q x * P z)

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ (P y * Q z - P z * Q y) / (P x * Q z - P z * Q x) = (P y * Q z - Q y * P z) / (P x * Q z - Q x * P z)

Tactic:
ring1

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ ?m.1582090 ≠ ?m.1582091

Tactic:
rwa [ne_eq, ← X_eq_iff hPz hQz]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ (toAffine W).slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z) = (P y * Q z - Q y * P z) / (P x * Q z - Q x * P z)

Tactic:
field_simp [Affine.slope_of_X_ne <| by rwa [ne_eq, ← X_eq_iff hPz hQz]]

Result:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z ≠ Q x * P z
⊢ (P y * Q z - P z * Q y) / (P x * Q z - P z * Q x) = (P y * Q z - Q y * P z) / (P x * Q z - Q x * P z)
-- Mathlib/Algebra/Homology/Opposite.lean
@[simp]
lemma quasiIso_unopFunctor_map_iff
    {K L : HomologicalComplex Vᵒᵖ c} (φ : K ⟶ L)
    [∀ i, K.HasHomology i] [∀ i, L.HasHomology i] :
    QuasiIso ((unopFunctor _ _).map φ.op) ↔ QuasiIso φ

Proof state:
ι : Type u_1
V : Type u_2
inst✝³ : Category.{u_3, u_2} V
c : ComplexShape ι
inst✝² : HasZeroMorphisms V
K L : HomologicalComplex Vᵒᵖ c
φ : K ⟶ L
inst✝¹ : ∀ (i : ι), K.HasHomology i
inst✝ : ∀ (i : ι), L.HasHomology i
⊢ QuasiIso ((unopFunctor V c).map φ.op) ↔ QuasiIso φ

Tactic:
simp only [quasiIso_iff, quasiIsoAt_unopFunctor_map_iff]

Result:
no goals
-- Mathlib/Data/List/Permutation.lean
theorem length_foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
    length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) =
      (map length L).sum + length r

Proof state:
α : Type u_1
t : α
ts : List α
r L : List (List α)
⊢ (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L).length = (map length L).sum + r.length

Tactic:
simp [foldr_permutationsAux2, Function.comp_def, length_permutationsAux2, length_flatMap]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Basic.lean
theorem monic_geom_sum_X {n : ℕ} (hn : n ≠ 0) : (∑ i ∈ range n, (X : R[X]) ^ i).Monic

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ 0 < X.natDegree

Tactic:
simp only [natDegree_X, zero_lt_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
⊢ (∑ i ∈ range n, X ^ i).Monic

Tactic:
nontriviality R

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ (∑ i ∈ range n, X ^ i).Monic

Proof state:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ (∑ i ∈ range n, X ^ i).Monic

Tactic:
apply monic_X.geom_sum _ hn

Result:
R : Type u
inst✝ : Semiring R
n : ℕ
hn : n ≠ 0
a✝ : Nontrivial R
⊢ 0 < X.natDegree
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_apply_zero (n : ℕ) :
    (ofScalars E c n fun _ => 0) = Pi.single (f := fun _ => E) 0 (c 0 • 1) n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
⊢ ((ofScalars E c n) fun x => 0) = Pi.single 0 (c 0 • 1) n

Tactic:
rw [ofScalars]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
⊢ ((c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 0) = Pi.single 0 (c 0 • 1) n

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : Ring E
inst✝² : Algebra 𝕜 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalRing E
c : ℕ → 𝕜
n : ℕ
⊢ ((c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E) fun x => 0) = Pi.single 0 (c 0 • 1) n

Tactic:
cases n <;> simp

Result:
no goals