harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_neg {x} : ∀ y : HomogeneousLocalization 𝒜 x, (-y).val = -y.val :=
  Quotient.ind' fun y ↦ by rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]; rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ (-Quotient.mk'' y).val = -val (Quotient.mk'' y)

Tactic:
rw [← mk_neg, val_mk, val_mk, Localization.neg_mk]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
y : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(-y).num ⟨↑(-y).den, ⋯⟩ = Localization.mk (-↑y.num) ⟨↑y.den, ⋯⟩
-- Mathlib/Order/Filter/SmallSets.lean
theorem eventually_smallSets_forall {p : α → Prop} :
    (∀ᶠ s in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ x in l, p x

Proof state:
α : Type u_1
l : Filter α
p : α → Prop
⊢ (∀ᶠ (s : Set α) in l.smallSets, ∀ x ∈ s, p x) ↔ ∀ᶠ (x : α) in l, p x

Tactic:
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_comm' [DecidableEq m] [DecidableEq n] {M : Matrix n m A} {N : Matrix m n A}
    {M' : Matrix m n A} (hMM' : M * M' = 1) (hM'M : M' * M = 1) : det (M * N) = det (N * M)

Proof state:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = (N * M).det

Tactic:
rw [← det_submatrix_equiv_self e, ← submatrix_mul_equiv _ _ _ (Equiv.refl n) _, det_comm,
  submatrix_mul_equiv, Equiv.coe_refl, submatrix_id_id]

Result:
no goals

Proof state:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
⊢ (M * N).det = (N * M).det

Tactic:
let e := indexEquivOfInv hMM' hM'M

Result:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
e : n ≃ m := indexEquivOfInv hMM' hM'M
⊢ (M * N).det = (N * M).det

Proof state:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
⊢ (M * N).det = (N * M).det

Tactic:
nontriviality A

Result:
A : Type u_5
inst✝⁴ : CommRing A
m : Type u_6
n : Type u_7
inst✝³ : Fintype m
inst✝² : Fintype n
inst✝¹ : DecidableEq m
inst✝ : DecidableEq n
M : Matrix n m A
N M' : Matrix m n A
hMM' : M * M' = 1
hM'M : M' * M = 1
a✝ : Nontrivial A
⊢ (M * N).det = (N * M).det
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pullbackIsoUnopPushout_inv_snd {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] :
    (pullbackIsoUnopPushout f g).inv ≫ pullback.snd f g =
      (pushout.inr _ _ : _ ⟶ pushout f.op g.op).unop :=
  (IsLimit.conePointUniqueUpToIso_inv_comp _ _ _).trans (by simp [unop_id (X := { unop := Y })])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (PushoutCocone.unop (colimit.cocone (span f.op g.op))).π.app WalkingCospan.right = (pushout.inr f.op g.op).unop

Tactic:
simp [unop_id (X := { unop := Y })]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
/-- Embedding `i : Fin n` into `Fin (n + 1)` using a pivot `p` that is lesser
results in a value that is greater than `p`. -/
lemma lt_succAbove_iff_le_castSucc (p : Fin (n + 1)) (i : Fin n) :
    p < p.succAbove i ↔ p ≤ castSucc i

Proof state:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Result:
no goals

Proof state:
case inr
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]

Result:
no goals

Proof state:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]

Result:
case inl
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem right_ne_of_oangle_sign_eq_neg_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = -1) : p₃ ≠ p₂ :=
  right_ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : (∡ p₁ p₂ p₃).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Rel.lean
theorem inter_dom_subset_preimage_image (s : Set α) : s ∩ r.dom ⊆ r.preimage (r.image s)

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s ∧ x ∈ {x | ∃ y, r x y}
⊢ x ∈ r.preimage (r.image s)

Tactic:
rcases hx with ⟨hx, ⟨y, rxy⟩⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ x ∈ r.preimage (r.image s)

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s ∩ r.dom
⊢ x ∈ r.preimage (r.image s)

Tactic:
simp only [Set.mem_inter_iff, dom] at hx

Result:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s ∧ x ∈ {x | ∃ y, r x y}
⊢ x ∈ r.preimage (r.image s)

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ (∃ x ∈ s, r x y) ∧ r.inv y x

Tactic:
exact ⟨⟨x, hx, rxy⟩, rxy⟩

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ x ∈ r.preimage (r.image s)

Tactic:
use y

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ y ∈ r.image s ∧ r.inv y x

Proof state:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
⊢ s ∩ r.dom ⊆ r.preimage (r.image s)

Tactic:
intro x hx

Result:
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s ∩ r.dom
⊢ x ∈ r.preimage (r.image s)

Proof state:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ y ∈ r.image s ∧ r.inv y x

Tactic:
simp only [image, Set.mem_setOf_eq]

Result:
case h
α : Type u_1
β : Type u_2
r : Rel α β
s : Set α
x : α
hx : x ∈ s
y : β
rxy : r x y
⊢ (∃ x ∈ s, r x y) ∧ r.inv y x
-- Mathlib/RingTheory/WittVector/Identities.lean
theorem verschiebung_zmod (x : 𝕎 (ZMod p)) : verschiebung x = x * p

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ verschiebung x = x * ↑p

Tactic:
rw [← frobenius_verschiebung, frobenius_zmodp]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma dblXYZ_smul (P : Fin 3 → R) (u : R) : W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.dblXYZ (u • P) = u ^ 4 • W'.dblXYZ P

Tactic:
rw [dblXYZ, dblX_smul, dblY_smul, dblZ_smul, smul_fin3, dblXYZ_X, dblXYZ_Y, dblXYZ_Z]

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
@[to_additive (attr := simp)]
lemma subgroupClosure_mul (hs : s.Nonempty) : closure s * s = closure s

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ↑(closure s) * s = ↑(closure s)

Tactic:
rw [← Set.iUnion_op_smul_set]

Result:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)

Tactic:
have h a (ha : a ∈ s) :  (closure s : Set G) <• a = closure s :=
  op_smul_coe_set <| subset_closure ha

Result:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, ↑(closure s) <• a = ↑(closure s)
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)

Proof state:
G : Type u_2
inst✝ : Group G
s : Set G
hs : s.Nonempty
h : ∀ a ∈ s, ↑(closure s) <• a = ↑(closure s)
⊢ ⋃ a ∈ s, ↑(closure s) <• a = ↑(closure s)

Tactic:
simp +contextual [h, hs]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
theorem leadingCoeff_add_eq_right {Γ} [LinearOrder Γ] {x y : HahnSeries Γ R}
    (hxy : y.orderTop < x.orderTop) : (x + y).leadingCoeff = y.leadingCoeff

Proof state:
R : Type u_3
inst✝¹ : AddMonoid R
Γ : Type u_8
inst✝ : LinearOrder Γ
x y : HahnSeries Γ R
hxy : y.orderTop < x.orderTop
⊢ (x + y).leadingCoeff = y.leadingCoeff

Tactic:
simpa [← map_add, ← AddOpposite.op_add, hxy] using leadingCoeff_add_eq_left
  (x := addOppositeEquiv.symm (.op y))
  (y := addOppositeEquiv.symm (.op x))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem isPrefixOf_toList [BEq α] {as bs : Array α} :
    as.toList.isPrefixOf bs.toList = as.isPrefixOf bs

Proof state:
case mk.mk
α : Type u_1
inst✝ : BEq α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.toList.isPrefixOf { toList := toList✝ }.toList =
    { toList := toList✝¹ }.isPrefixOf { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
as bs : Array α
⊢ as.toList.isPrefixOf bs.toList = as.isPrefixOf bs

Tactic:
cases as

Result:
case mk
α : Type u_1
inst✝ : BEq α
bs : Array α
toList✝ : List α
⊢ { toList := toList✝ }.toList.isPrefixOf bs.toList = { toList := toList✝ }.isPrefixOf bs

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
bs : Array α
toList✝ : List α
⊢ { toList := toList✝ }.toList.isPrefixOf bs.toList = { toList := toList✝ }.isPrefixOf bs

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
inst✝ : BEq α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ }.toList.isPrefixOf { toList := toList✝ }.toList =
    { toList := toList✝¹ }.isPrefixOf { toList := toList✝ }
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
/-- The measure `μ.restrict μ.sigmaFiniteSetᶜ` takes only two values: 0 and ∞ . -/
lemma restrict_compl_sigmaFiniteSet_eq_zero_or_top (μ : Measure α) [SFinite μ] (s : Set α) :
    μ.restrict μ.sigmaFiniteSetᶜ s = 0 ∨ μ.restrict μ.sigmaFiniteSetᶜ s = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ (μ.restrict μ.sigmaFiniteSetᶜ) s = 0 ∨ (μ.restrict μ.sigmaFiniteSetᶜ) s = ⊤

Tactic:
rw [Measure.restrict_apply' measurableSet_sigmaFiniteSet.compl]

Result:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
s : Set α
⊢ μ (s ∩ μ.sigmaFiniteSetᶜ) = 0 ∨ μ (s ∩ μ.sigmaFiniteSetᶜ) = ⊤

Tactic:
exact measure_eq_zero_or_top_of_subset_compl_sigmaFiniteSet Set.inter_subset_right

Result:
no goals
-- Mathlib/RingTheory/WittVector/DiscreteValuationRing.lean
theorem exists_eq_pow_p_mul' (a : 𝕎 k) (ha : a ≠ 0) :
    ∃ (m : ℕ) (b : Units (𝕎 k)), a = (p : 𝕎 k) ^ m * b

Proof state:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
⊢ ∃ m b, a = ↑p ^ m * ↑b

Tactic:
have hb₀ : b.coeff 0 = b₀ := rfl

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
hb₀ : b.coeff 0 = ↑b₀
⊢ ∃ m b, a = ↑p ^ m * ↑b

Proof state:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
⊢ ∃ m b, a = ↑p ^ m * ↑b

Tactic:
let b₀ := Units.mk0 (b.coeff 0) h₁

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
⊢ ∃ m b, a = ↑p ^ m * ↑b

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
⊢ ∃ m b, a = ↑p ^ m * ↑b

Tactic:
obtain ⟨m, b, h₁, h₂⟩ := exists_eq_pow_p_mul a ha

Result:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
⊢ ∃ m b, a = ↑p ^ m * ↑b

Proof state:
case intro.intro.intro
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
h₁ : b.coeff 0 ≠ 0
h₂ : a = ↑p ^ m * b
b₀ : kˣ := Units.mk0 (b.coeff 0) h₁
hb₀ : b.coeff 0 = ↑b₀
⊢ ∃ m b, a = ↑p ^ m * ↑b

Tactic:
exact ⟨m, mkUnit hb₀, h₂⟩

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem Wbtw.trans_right_ne [NoZeroSMulDivisors R V] {w x y z : P} (h₁ : Wbtw R w x z)
    (h₂ : Wbtw R x y z) (h : w ≠ x) : w ≠ y

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x z : P
h₁ : Wbtw R w x z
h : w ≠ x
h₂ : Wbtw R x w z
⊢ False

Tactic:
exact h (h₁.swap_left_iff.1 h₂)

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x y z : P
h₁ : Wbtw R w x z
h₂ : Wbtw R x y z
h : w ≠ x
⊢ w ≠ y

Tactic:
rintro rfl

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝⁴ : OrderedRing R
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddTorsor V P
inst✝ : NoZeroSMulDivisors R V
w x z : P
h₁ : Wbtw R w x z
h : w ≠ x
h₂ : Wbtw R x w z
⊢ False
-- Mathlib/Order/Basic.lean
theorem Pi.lt_def [∀ i, Preorder (π i)] {x y : ∀ i, π i} :
    x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝ : (i : ι) → Preorder (π i)
x y : (i : ι) → π i
⊢ x < y ↔ x ≤ y ∧ ∃ i, x i < y i

Tactic:
simp +contextual [lt_iff_le_not_le, Pi.le_def]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma sub_add_sub_cancel (hab : b ≤ a) (hcb : c ≤ b) : a - b + (b - c) = a - c

Proof state:
a b c : ℕ
hab : b ≤ a
hcb : c ≤ b
⊢ a - b + (b - c) = a - c

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem ne_iff_lt_or_gt {i j : Fin n} : i ≠ j ↔ i < j ∨ i > j

Proof state:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩ ≠ j ↔ ⟨val✝, isLt✝⟩ < j ∨ ⟨val✝, isLt✝⟩ > j

Tactic:
cases j

Result:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩ ↔ ⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ∨ ⟨val✝¹, isLt✝¹⟩ > ⟨val✝, isLt✝⟩

Proof state:
n : Nat
i j : Fin n
⊢ i ≠ j ↔ i < j ∨ i > j

Tactic:
cases i

Result:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝, isLt✝⟩ ≠ j ↔ ⟨val✝, isLt✝⟩ < j ∨ ⟨val✝, isLt✝⟩ > j

Proof state:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ⟨val✝¹, isLt✝¹⟩ ≠ ⟨val✝, isLt✝⟩ ↔ ⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ∨ ⟨val✝¹, isLt✝¹⟩ > ⟨val✝, isLt✝⟩

Tactic:
simp only [ne_eq, Fin.mk.injEq, Nat.ne_iff_lt_or_gt, gt_iff_lt]

Result:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ val✝¹ < val✝ ∨ val✝ < val✝¹ ↔ ⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ∨ ⟨val✝, isLt✝⟩ < ⟨val✝¹, isLt✝¹⟩

Proof state:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ val✝¹ < val✝ ∨ val✝ < val✝¹ ↔ ⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ∨ ⟨val✝, isLt✝⟩ < ⟨val✝¹, isLt✝¹⟩

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem toFilteriUnion_congr (I : Box ι) (l : IntegrationParams) {π₁ π₂ : Prepartition I}
    (h : π₁.iUnion = π₂.iUnion) : l.toFilteriUnion I π₁ = l.toFilteriUnion I π₂

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
l : IntegrationParams
π₁ π₂ : Prepartition I
h : π₁.iUnion = π₂.iUnion
⊢ toFilteriUnion I π₁ = toFilteriUnion I π₂

Tactic:
simp only [toFilteriUnion, toFilterDistortioniUnion, h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two (x y : V) :
    ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2

Tactic:
exact inner_eq_zero_iff_angle_eq_pi_div_two x y

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ ↔ angle x y = π / 2

Tactic:
rw [norm_sub_sq_eq_norm_sq_add_norm_sq_iff_real_inner_eq_zero]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ inner x y = 0 ↔ angle x y = π / 2
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem finprod_heightOneSpectrum_factorization_coe {I : Ideal R} (hI : I ≠ 0) :
    (∏ᶠ v : HeightOneSpectrum R, (v.asIdeal : FractionalIdeal R⁰ K) ^
      ((Associates.mk v.asIdeal).count (Associates.mk I).factors : ℤ)) = I

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) = ↑I

Tactic:
conv_rhs => rw [← Ideal.finprod_heightOneSpectrum_factorization hI]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ↑(∏ᶠ (v : HeightOneSpectrum R), v.maxPowDividing I)

Tactic:
rw [FractionalIdeal.coeIdeal_finprod R⁰ K (le_refl _)]

Result:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(a.maxPowDividing I)

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
I : Ideal R
hI : I ≠ 0
⊢ ∏ᶠ (v : HeightOneSpectrum R), ↑v.asIdeal ^ ↑((Associates.mk v.asIdeal).count (Associates.mk I).factors) =
    ∏ᶠ (a : HeightOneSpectrum R), ↑(a.maxPowDividing I)

Tactic:
simp_rw [IsDedekindDomain.HeightOneSpectrum.maxPowDividing, FractionalIdeal.coeIdeal_pow,
  zpow_natCast]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma continuous_iff (hg : IsInducing g) :
    Continuous f ↔ Continuous (g ∘ f)

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Z
hg : IsInducing g
⊢ Continuous f ↔ Continuous (g ∘ f)

Tactic:
simp_rw [continuous_iff_continuousAt, hg.continuousAt_iff]

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
theorem ChartedSpace.secondCountable_of_sigmaCompact [SecondCountableTopology H]
    [SigmaCompactSpace M] : SecondCountableTopology M

Proof state:
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
⊢ SecondCountableTopology M

Tactic:
obtain ⟨s, hsc, hsU⟩ : ∃ s, Set.Countable s ∧ ⋃ (x) (_ : x ∈ s), (chartAt H x).source = univ :=
  countable_cover_nhds_of_sigmaCompact fun x : M ↦ chart_source_mem_nhds H x

Result:
case intro.intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
s : Set M
hsc : s.Countable
hsU : ⋃ x ∈ s, (chartAt H x).source = univ
⊢ SecondCountableTopology M

Proof state:
case intro.intro
H : Type u
M : Type u_2
inst✝⁴ : TopologicalSpace H
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : SecondCountableTopology H
inst✝ : SigmaCompactSpace M
s : Set M
hsc : s.Countable
hsU : ⋃ x ∈ s, (chartAt H x).source = univ
⊢ SecondCountableTopology M

Tactic:
exact ChartedSpace.secondCountable_of_countable_cover H hsU hsc

Result:
no goals
-- Mathlib/Probability/Process/Stopping.lean
theorem stoppedValue_piecewise_const' {ι' : Type*} {i j : ι'} {f : ι' → Ω → ℝ} :
    stoppedValue f (s.piecewise (fun _ => i) fun _ => j) =
    s.indicator (f i) + sᶜ.indicator (f j)

Proof state:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ f (s.piecewise (fun x => i) (fun x => j) ω) ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
by_cases hx : ω ∈ s <;> simp [hx]

Result:
no goals

Proof state:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω

Tactic:
rw [stoppedValue]

Result:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ f (s.piecewise (fun x => i) (fun x => j) ω) ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω

Proof state:
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) = s.indicator (f i) + sᶜ.indicator (f j)

Tactic:
ext ω

Result:
case h
Ω : Type u_1
s : Set Ω
inst✝ : DecidablePred fun x => x ∈ s
ι' : Type u_4
i j : ι'
f : ι' → Ω → ℝ
ω : Ω
⊢ stoppedValue f (s.piecewise (fun x => i) fun x => j) ω = (s.indicator (f i) + sᶜ.indicator (f j)) ω
-- Mathlib/Data/Nat/Factorial/DoubleFactorial.lean
theorem doubleFactorial_add_one (n : ℕ) : (n + 1)‼ = (n + 1) * (n - 1)‼

Proof state:
n : ℕ
⊢ (n + 1)‼ = (n + 1) * (n - 1)‼

Tactic:
cases n <;> rfl

Result:
no goals