harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSpace/DomAct/Basic.lean
theorem smul_Lp_neg (c : Mᵈᵐᵃ) (f : Lp E p μ) : c • (-f) = -(c • f)

Proof state:
case mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • -⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩ = -(c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩)

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
f : ↥(Lp E p μ)
⊢ c • -f = -(c • f)

Tactic:
rcases f with ⟨⟨_⟩, _⟩

Result:
case mk.mk
M : Type u_1
α : Type u_3
E : Type u_4
inst✝⁵ : MeasurableSpace M
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
μ : Measure α
p : ℝ≥0∞
inst✝² : SMul M α
inst✝¹ : SMulInvariantMeasure M α μ
inst✝ : MeasurableSMul M α
c : Mᵈᵐᵃ
val✝ : α →ₘ[μ] E
a✝ : { f // AEStronglyMeasurable f μ }
property✝ : Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝ ∈ Lp E p μ
⊢ c • -⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩ = -(c • ⟨Quot.mk (⇑(Measure.aeEqSetoid E μ)) a✝, property✝⟩)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_eq_xor {a b : BitVec 1} : a - b = a ^^^ b

Proof state:
case inr
a b : BitVec 1
hb : b = 0 ∨ b = 1
h : a = 1
⊢ a - b = a ^^^ b

Tactic:
rcases hb with h' | h' <;> (simp [h, h'])

Result:
no goals

Proof state:
a b : BitVec 1
⊢ a - b = a ^^^ b

Tactic:
have ha : a = 0 ∨ a = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a - b = a ^^^ b

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a - b = a ^^^ b

Tactic:
rcases ha with h | h <;> (rcases hb with h' | h' <;> (simp [h, h']))

Result:
no goals

Proof state:
case inr.inr
a b : BitVec 1
h : a = 1
h' : b = 1
⊢ a - b = a ^^^ b

Tactic:
simp [h, h']

Result:
no goals

Proof state:
a b : BitVec 1
ha : a = 0 ∨ a = 1
⊢ a - b = a ^^^ b

Tactic:
have hb : b = 0 ∨ b = 1 := eq_zero_or_eq_one _

Result:
a b : BitVec 1
ha : a = 0 ∨ a = 1
hb : b = 0 ∨ b = 1
⊢ a - b = a ^^^ b
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem not_integrableOn_Ioi_rpow (s : ℝ) : ¬ IntegrableOn (fun x ↦ x ^ s) (Ioi (0 : ℝ))

Proof state:
case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
this : s < -1
⊢ False

Tactic:
exact hs.not_lt this

Result:
no goals

Proof state:
case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
this : IntegrableOn (fun x => x ^ s) (Ioi 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioi_rpow_iff zero_lt_one] at this

Result:
case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
this : s < -1
⊢ False

Proof state:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : IntegrableOn (fun x => x ^ s) (Ioo 0 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioo_rpow_iff zero_lt_one] at this

Result:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : -1 < s
⊢ False

Proof state:
s : ℝ
⊢ ¬IntegrableOn (fun x => x ^ s) (Ioi 0) volume

Tactic:
intro h

Result:
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
⊢ False

Proof state:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x ^ s) (Ioo (0 : ℝ) 1) := h.mono Ioo_subset_Ioi_self le_rfl

Result:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : IntegrableOn (fun x => x ^ s) (Ioo 0 1) volume
⊢ False

Proof state:
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
⊢ False

Tactic:
rcases le_or_lt s (-1) with hs|hs

Result:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
⊢ False

case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
⊢ False

Proof state:
case inl
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : s ≤ -1
this : -1 < s
⊢ False

Tactic:
exact hs.not_lt this

Result:
no goals

Proof state:
case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
⊢ False

Tactic:
have : IntegrableOn (fun x ↦ x ^ s) (Ioi (1 : ℝ)) := h.mono (Ioi_subset_Ioi zero_le_one) le_rfl

Result:
case inr
s : ℝ
h : IntegrableOn (fun x => x ^ s) (Ioi 0) volume
hs : -1 < s
this : IntegrableOn (fun x => x ^ s) (Ioi 1) volume
⊢ False
-- Mathlib/Algebra/MvPolynomial/Degrees.lean
theorem totalDegree_C (a : R) : (C a : MvPolynomial σ R).totalDegree = 0 :=
  (supDegree_single 0 a).trans <| by rw [sum_zero_index, bot_eq_zero', ite_self]

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
a : R
⊢ (if a = 0 then ⊥ else sum 0 fun x e => e) = 0

Tactic:
rw [sum_zero_index, bot_eq_zero', ite_self]

Result:
no goals
-- Mathlib/Order/SupClosed.lean
lemma SupClosed.iSup_mem [Finite ι] (hs : SupClosed s) (hbot : ⊥ ∈ s) (hf : ∀ i, f i ∈ s) :
    ⨆ i, f i ∈ s

Proof state:
case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s

Tactic:
exact hs.iSup_mem_of_nonempty hf

Result:
no goals

Proof state:
case inl
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : IsEmpty ι
⊢ ⨆ i, f i ∈ s

Tactic:
simpa [iSup_of_empty]

Result:
no goals

Proof state:
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : IsEmpty ι
⊢ ⨆ i, f i ∈ s

case inr
ι : Sort u_1
α : Type u_3
inst✝¹ : CompleteLattice α
f : ι → α
s : Set α
inst✝ : Finite ι
hs : SupClosed s
hbot : ⊥ ∈ s
hf : ∀ (i : ι), f i ∈ s
h✝ : Nonempty ι
⊢ ⨆ i, f i ∈ s
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `v` belongs to the interior of the interval `integrableExpSet X μ`,
then `X ^ n * exp (v * X)` is integrable for all `n : ℕ`. -/
lemma integrable_pow_mul_exp_of_mem_interior_integrableExpSet
    (hv : v ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ X ω ^ n * exp (v * X ω)) μ

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ 0 ≤ ↑n

Tactic:
positivity

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => X ω ^ n * rexp (v * X ω)) μ

Tactic:
convert integrable_rpow_mul_exp_of_mem_interior_integrableExpSet hv
  (by positivity : 0 ≤ (n : ℝ)) with ω

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
hv : v ∈ interior (integrableExpSet X μ)
n : ℕ
ω : Ω
⊢ X ω ^ n = X ω ^ ↑n
-- Mathlib/Probability/ProbabilityMassFunction/Binomial.lean
theorem binomial_apply (p : ℝ≥0∞) (h : p ≤ 1) (n : ℕ) (i : Fin (n + 1)) :
    binomial p h n i = p^(i : ℕ) * (1-p)^((Fin.last n - i) : ℕ) * (n.choose i : ℕ)

Proof state:
p : ℝ≥0∞
h : p ≤ 1
n : ℕ
i : Fin (n + 1)
⊢ (binomial p h n) i = p ^ ↑i * (1 - p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)

Tactic:
lift p to ℝ≥0 using ne_top_of_lt <| h.trans_lt one_lt_top

Result:
case intro
n : ℕ
i : Fin (n + 1)
p : ℝ≥0
h : ↑p ≤ 1
⊢ (binomial (↑p) h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)

Proof state:
case intro
n : ℕ
i : Fin (n + 1)
p : ℝ≥0
h : ↑p ≤ 1
⊢ (binomial (↑p) h n) i = ↑p ^ ↑i * (1 - ↑p) ^ (↑(Fin.last n) - ↑i) * ↑(n.choose ↑i)

Tactic:
simp [binomial]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
lemma divisorsAntidiag_neg_natCast (n : ℕ) :
    divisorsAntidiag (-n) =
      (n.divisorsAntidiagonal.map <| .prodMap natCast negNatCast).disjUnion
        (n.divisorsAntidiagonal.map <| .prodMap negNatCast natCast) (by
          simp +contextual [disjoint_left, eq_comm])

Proof state:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ Disjoint (map (Nat.castEmbedding.prodMap negNatCast) n.divisorsAntidiagonal)
    (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal)

Tactic:
simp +contextual [disjoint_left, eq_comm]

Result:
no goals

Proof state:
n : ℕ
⊢ (-↑n).divisorsAntidiag =
    (map (Nat.castEmbedding.prodMap negNatCast) n.divisorsAntidiagonal).disjUnion
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯

Tactic:
cases n <;> rfl

Result:
no goals
-- Mathlib/Algebra/Group/EvenFunction.lean
lemma Odd.mul_even [HasDistribNeg R] (hf : f.Odd) (hg : g.Even) : (f * g).Odd

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
⊢ Function.Odd (f * g)

Tactic:
intro a

Result:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = -(f * g) a

Proof state:
α : Type u_1
inst✝² : Neg α
R : Type u_3
inst✝¹ : Mul R
f g : α → R
inst✝ : HasDistribNeg R
hf : Function.Odd f
hg : Function.Even g
a : α
⊢ (f * g) (-a) = -(f * g) a

Tactic:
simp only [Pi.mul_apply, hf a, hg a, neg_mul]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem LiftRelO.swap (R : α → β → Prop) (C) :
    swap (LiftRelO R C) = LiftRelO (swap R) (swap C)

Proof state:
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
⊢ Function.swap (LiftRelO R C) = LiftRelO (Function.swap R) (Function.swap C)

Tactic:
funext x y

Result:
case h.h
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y

Proof state:
case h.h
α : Type u
β : Type v
R : α → β → Prop
C : WSeq α → WSeq β → Prop
x : Option (β × WSeq β)
y : Option (α × WSeq α)
⊢ Function.swap (LiftRelO R C) x y = LiftRelO (Function.swap R) (Function.swap C) x y

Tactic:
rcases x with ⟨⟩ | ⟨hx, jx⟩ <;> rcases y with ⟨⟩ | ⟨hy, jy⟩ <;> rfl

Result:
no goals
-- Mathlib/Analysis/Convex/Star.lean
theorem StarConvex.affine_image (f : E →ᵃ[𝕜] F) {s : Set E} (hs : StarConvex 𝕜 x s) :
    StarConvex 𝕜 (f x) (f '' s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
⊢ StarConvex 𝕜 (f x) (⇑f '' s)

Tactic:
rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • y ∈ ⇑f '' s

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y') = a • f x + b • y

Tactic:
rw [Convex.combo_affine_apply hab, hy'f]

Result:
no goals

Proof state:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • y ∈ ⇑f '' s

Tactic:
refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩

Result:
case intro.intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : OrderedRing 𝕜
inst✝³ : AddCommGroup E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
x : E
f : E →ᵃ[𝕜] F
s : Set E
hs : StarConvex 𝕜 x s
y : F
y' : E
hy' : y' ∈ s
hy'f : f y' = y
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ f (a • x + b • y') = a • f x + b • y
-- Mathlib/Algebra/Group/Graph.lean
/-- **Vertical line test** for group homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every "vertical line" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`. -/
@[to_additive "**Vertical line test** for group homomorphisms.

Let `f : G → H × I` be a homomorphism to a product of groups. Assume that `f` is surjective on the
first factor and that the image of `f` intersects every \"vertical line\" `{(h, i) | i : I}` at most
once. Then the image of `f` is the graph of some group homomorphism `f' : H → I`."]
lemma exists_range_eq_graph {f : G →* H × I} (hf₁ : Surjective (Prod.fst ∘ f))
    (hf : ∀ g₁ g₂, (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2) :
    ∃ f' : H →* I, range f = f'.graph

Proof state:
G : Type u_1
H : Type u_2
I : Type u_3
inst✝² : Group G
inst✝¹ : Group H
inst✝ : Group I
f : G →* H × I
hf₁ : Surjective (Prod.fst ∘ ⇑f)
hf : ∀ (g₁ g₂ : G), (f g₁).1 = (f g₂).1 → (f g₁).2 = (f g₂).2
⊢ ∃ f', f.range = f'.graph

Tactic:
simpa [SetLike.ext_iff] using exists_mrange_eq_mgraph hf₁ hf

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Metric.lean
theorem dist_comm : G.dist u v = G.dist v u

Proof state:
V : Type u_1
G : SimpleGraph V
u v : V
⊢ G.dist u v = G.dist v u

Tactic:
rw [dist, dist, edist_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/TensorProduct.lean
theorem associated_baseChange [Invertible (2 : A)] (Q : QuadraticForm R M₂) :
    associated (R := A) (Q.baseChange A) = BilinForm.baseChange A (associated (R := R) Q)

Proof state:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ BilinForm.tmul (LinearMap.mul A A) (associated Q) = BilinForm.baseChange A (associated Q)

Tactic:
exact rfl

Result:
no goals

Proof state:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ associated (QuadraticForm.baseChange A Q) = BilinForm.baseChange A (associated Q)

Tactic:
dsimp only [QuadraticForm.baseChange, LinearMap.baseChange]

Result:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ associated (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.baseChange A (associated Q)

Proof state:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ associated (QuadraticForm.tmul QuadraticMap.sq Q) = BilinForm.baseChange A (associated Q)

Tactic:
rw [associated_tmul (QuadraticMap.sq (R := A)) Q, associated_sq]

Result:
R : Type uR
A : Type uA
M₂ : Type uM₂
inst✝⁶ : CommRing R
inst✝⁵ : CommRing A
inst✝⁴ : AddCommGroup M₂
inst✝³ : Algebra R A
inst✝² : Module R M₂
inst✝¹ : Invertible 2
inst✝ : Invertible 2
Q : QuadraticForm R M₂
⊢ BilinForm.tmul (LinearMap.mul A A) (associated Q) = BilinForm.baseChange A (associated Q)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_true : (countP fun (_ : α) => true) = size

Proof state:
α : Type u_1
⊢ (countP fun x => true) = size

Tactic:
funext l

Result:
case h
α : Type u_1
l : Array α
⊢ countP (fun x => true) l = l.size

Proof state:
case h
α : Type u_1
l : Array α
⊢ countP (fun x => true) l = l.size

Tactic:
simp

Result:
no goals
-- Mathlib/Data/ENat/Basic.lean
lemma WithBot.lt_add_one_iff {n : WithBot ℕ∞} {m : ℕ} : n < m + 1 ↔ n ≤ m

Proof state:
case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Tactic:
rw [WithBot.coe_lt_coe, Nat.cast_add, ENat.coe_one, ENat.lt_add_one_iff (ENat.coe_ne_top _),
  ← WithBot.coe_le_coe, WithBot.coe_natCast]

Result:
no goals

Proof state:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑↑(m + 1) ↔ n ≤ ↑m

Tactic:
cases n

Result:
case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m

case coe
m : ℕ
a✝ : ℕ∞
⊢ ↑a✝ < ↑↑(m + 1) ↔ ↑a✝ ≤ ↑m

Proof state:
case bot
m : ℕ
⊢ ⊥ < ↑↑(m + 1) ↔ ⊥ ≤ ↑m

Tactic:
simp only [bot_le, iff_true, WithBot.bot_lt_coe]

Result:
no goals

Proof state:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑m + 1 ↔ n ≤ ↑m

Tactic:
rw [← WithBot.coe_one, ← ENat.coe_one, WithBot.coe_natCast, ← Nat.cast_add, ← WithBot.coe_natCast]

Result:
n : WithBot ℕ∞
m : ℕ
⊢ n < ↑↑(m + 1) ↔ n ≤ ↑m
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem ext_of_singleton [Countable α] {μ ν : Measure α} (h : ∀ a, μ {a} = ν {a}) : μ = ν :=
  ext_of_sUnion_eq_univ (countable_range singleton) (by aesop) (by aesop)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (a : α), μ {a} = ν {a}
⊢ ∀ s ∈ range singleton, μ.restrict s = ν.restrict s

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
inst✝ : Countable α
μ ν : Measure α
h : ∀ (a : α), μ {a} = ν {a}
⊢ ⋃₀ range singleton = univ

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem volume_pi_Ioo_toReal {a b : ι → ℝ} (h : a ≤ b) :
    (volume (pi univ fun i => Ioo (a i) (b i))).toReal = ∏ i, (b i - a i)

Proof state:
ι : Type u_1
inst✝ : Fintype ι
a b : ι → ℝ
h : a ≤ b
⊢ (volume (univ.pi fun i => Ioo (a i) (b i))).toReal = ∏ i : ι, (b i - a i)

Tactic:
simp only [volume_pi_Ioo, ENNReal.toReal_prod, ENNReal.toReal_ofReal (sub_nonneg.2 (h _))]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
lemma eLpNormEssSup_lt_top_iff_isBoundedUnder :
    eLpNormEssSup f μ < ⊤ ↔ IsBoundedUnder (· ≤ ·) (ae μ) fun x ↦ ‖f x‖₊ where
  mp h := ⟨(eLpNormEssSup f μ).toNNReal, by
    simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]; exact ae_le_eLpNormEssSup⟩
  mpr

Proof state:
case intro
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun x => ‖f x‖₊) (ae μ), (fun x1 x2 => x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ⊤

Tactic:
exact eLpNormEssSup_lt_top_of_ae_nnnorm_bound (C := C) hC

Result:
no goals

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ (IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (ae μ) fun x => ‖f x‖₊) → eLpNormEssSup f μ < ⊤

Tactic:
rintro ⟨C, hC⟩

Result:
case intro
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ≥0
hC : ∀ᶠ (x : ℝ≥0) in map (fun x => ‖f x‖₊) (ae μ), (fun x1 x2 => x1 ≤ x2) x C
⊢ eLpNormEssSup f μ < ⊤

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ⊤
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x => ‖f x‖₊) (ae μ), (fun x1 x2 => x1 ≤ x2) x (eLpNormEssSup f μ).toNNReal

Tactic:
simp_rw [← ENNReal.coe_le_coe, ENNReal.coe_toNNReal h.ne]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ⊤
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x => ‖f x‖₊) (ae μ), ↑x ≤ eLpNormEssSup f μ

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
h : eLpNormEssSup f μ < ⊤
⊢ ∀ᶠ (x : ℝ≥0) in map (fun x => ‖f x‖₊) (ae μ), ↑x ≤ eLpNormEssSup f μ

Tactic:
exact ae_le_eLpNormEssSup

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem equivFunOnFintype_single [Fintype ι] (i : ι) (m : β i) :
    (@DFinsupp.equivFunOnFintype ι β _ _) (DFinsupp.single i m) = Pi.single i m

Proof state:
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
⊢ equivFunOnFintype (single i m) = Pi.single i m

Tactic:
ext x

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ equivFunOnFintype (single i m) x = Pi.single i m x

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ equivFunOnFintype (single i m) x = Pi.single i m x

Tactic:
dsimp [Pi.single, Function.update]

Result:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ (single i m) x = if h : x = i then ⋯ ▸ m else 0

Proof state:
case h
ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
i : ι
m : β i
x : ι
⊢ (single i m) x = if h : x = i then ⋯ ▸ m else 0

Tactic:
simp [DFinsupp.single_eq_pi_single, @eq_comm _ i]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem subsingleton_iff_le_one : Subsingleton (Fin n) ↔ n ≤ 1

Proof state:
case refine_2
n : Nat
⊢ Subsingleton (Fin 1) ↔ 1 ≤ 1

Tactic:
simp

Result:
case refine_2
n : Nat
⊢ Subsingleton (Fin 1)

Proof state:
case refine_1
n : Nat
⊢ Subsingleton (Fin 0)

Tactic:
exact ⟨nofun⟩

Result:
no goals

Proof state:
case refine_2
n : Nat
⊢ Subsingleton (Fin 1)

Tactic:
exact ⟨fun ⟨0, _⟩ ⟨0, _⟩ => rfl⟩

Result:
no goals

Proof state:
n : Nat
⊢ Subsingleton (Fin n) ↔ n ≤ 1

Tactic:
(match n with | 0 | 1 | n+2 => ?_) <;> try simp

Result:
case refine_1
n : Nat
⊢ Subsingleton (Fin 0)

case refine_2
n : Nat
⊢ Subsingleton (Fin 1)

case refine_3
n✝ n : Nat
⊢ Subsingleton (Fin (n + 2)) ↔ n + 2 ≤ 1

Proof state:
n : Nat
⊢ Subsingleton (Fin n) ↔ n ≤ 1

Tactic:
match n with | 0 | 1 | n+2 => ?_

Result:
case refine_1
n : Nat
⊢ Subsingleton (Fin 0) ↔ 0 ≤ 1

case refine_2
n : Nat
⊢ Subsingleton (Fin 1) ↔ 1 ≤ 1

case refine_3
n✝ n : Nat
⊢ Subsingleton (Fin (n + 2)) ↔ n + 2 ≤ 1

Proof state:
case refine_3
n✝ n : Nat
⊢ Subsingleton (Fin (n + 2)) ↔ n + 2 ≤ 1

Tactic:
exact iff_of_false (fun h => Fin.ne_of_lt zero_lt_one (h.elim ..)) (of_decide_eq_false rfl)

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Ker.lean
theorem map_comap_eq_self {f : G →* N} {H : Subgroup N} (h : H ≤ f.range) :
    map f (comap f H) = H

Proof state:
G : Type u_1
inst✝¹ : Group G
N : Type u_5
inst✝ : Group N
f : G →* N
H : Subgroup N
h : H ≤ f.range
⊢ map f (comap f H) = H

Tactic:
rwa [map_comap_eq, inf_eq_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_eq_zero_iff {θ : Angle} : (2 : ℕ) • θ = 0 ↔ θ = 0 ∨ θ = π

Proof state:
θ : Angle
⊢ 2 • θ = 0 ↔ θ = 0 ∨ θ = ↑π

Tactic:
convert two_nsmul_eq_iff <;> simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/Equal.lean
theorem BitVec.xor_beq_zero_iff (a b : BitVec w) : (a ^^^ b == 0#w) = (a == b)

Proof state:
w : Nat
a b : BitVec w
⊢ (a ^^^ b == 0#w) = (a == b)

Tactic:
rw [Bool.eq_iff_iff]

Result:
w : Nat
a b : BitVec w
⊢ (a ^^^ b == 0#w) = true ↔ (a == b) = true

Proof state:
w : Nat
a b : BitVec w
⊢ (a ^^^ b == 0#w) = true ↔ (a == b) = true

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/Birthday.lean
theorem birthday_one : birthday 1 = 1

Proof state:
⊢ ((lsub fun i => (moveLeft 1 i).birthday) ⊔ lsub fun i => (moveRight 1 i).birthday) = 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ birthday 1 = 1

Tactic:
rw [birthday_def]

Result:
⊢ ((lsub fun i => (moveLeft 1 i).birthday) ⊔ lsub fun i => (moveRight 1 i).birthday) = 1