harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem leftInvOn_piecewise {e' : PartialEquiv α β} [∀ i, Decidable (i ∈ s)]
    [∀ i, Decidable (i ∈ t)] (h : e.IsImage s t) (h' : e'.IsImage s t) :
    LeftInvOn (t.piecewise e.symm e'.symm) (s.piecewise e e') (s.ite e.source e'.source)

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
⊢ LeftInvOn (t.piecewise ↑e.symm ↑e'.symm) (s.piecewise ↑e ↑e') (s.ite e.source e'.source)

Tactic:
rintro x (⟨he, hs⟩ | ⟨he, hs : x ∉ s⟩)

Result:
case inl.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

case inr.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : x ∉ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Proof state:
case inl.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e.source
hs : x ∈ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Tactic:
rw [piecewise_eq_of_mem _ _ _ hs, piecewise_eq_of_mem _ _ _ ((h he).2 hs), e.left_inv he]

Result:
no goals

Proof state:
case inr.intro
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
e' : PartialEquiv α β
inst✝¹ : (i : α) → Decidable (i ∈ s)
inst✝ : (i : β) → Decidable (i ∈ t)
h : e.IsImage s t
h' : e'.IsImage s t
x : α
he : x ∈ e'.source
hs : x ∉ s
⊢ t.piecewise (↑e.symm) (↑e'.symm) (s.piecewise (↑e) (↑e') x) = x

Tactic:
rw [piecewise_eq_of_not_mem _ _ _ hs, piecewise_eq_of_not_mem _ _ _ ((h'.compl he).2 hs),
  e'.left_inv he]

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem Int.finiteMultiplicity_iff {a b : ℤ} : FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Proof state:
a b : ℤ
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
  pos_iff_ne_zero, Int.natAbs_ne_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_neg_one (a : Int) : a * -1 = -a

Proof state:
a : Int
⊢ a * -1 = -a

Tactic:
rw [Int.mul_neg, Int.mul_one]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
lemma filter_attach' (l : List α) (p : {a // a ∈ l} → Bool) [DecidableEq α] :
    l.attach.filter p =
      (l.filter fun x => ∃ h, p ⟨x, h⟩).attach.map (Subtype.map id fun _ => mem_of_mem_filter)

Proof state:
α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x => decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
refine map_injective_iff.2 Subtype.coe_injective ?_

Result:
α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ map (fun a => ↑a) (filter p l.attach) =
    map (fun a => ↑a) (map (Subtype.map id ⋯) (filter (fun x => decide (∃ h, p ⟨x, h⟩ = true)) l).attach)

Proof state:
α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ map (fun a => ↑a) (filter p l.attach) =
    map (fun a => ↑a) (map (Subtype.map id ⋯) (filter (fun x => decide (∃ h, p ⟨x, h⟩ = true)) l).attach)

Tactic:
simp [comp_def, map_filter _ Subtype.coe_injective]

Result:
no goals

Proof state:
α : Type u
l : List α
p : { a // a ∈ l } → Bool
inst✝ : DecidableEq α
⊢ filter p l.attach = map (Subtype.map id ⋯) (filter (fun x => decide (∃ h, p ⟨x, h⟩ = true)) l).attach

Tactic:
classical
refine map_injective_iff.2 Subtype.coe_injective ?_
simp [comp_def, map_filter _ Subtype.coe_injective]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
theorem condCDF_ae_eq (ρ : Measure (α × ℝ)) [IsFiniteMeasure ρ] (r : ℚ) :
    (fun a ↦ condCDF ρ a r) =ᵐ[ρ.fst] fun a ↦ (preCDF ρ r a).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a => ↑(condCDF ρ a) ↑r) =ᶠ[ae ρ.fst] fun a => (preCDF ρ r a).toReal

Tactic:
simp_rw [condCDF_eq_stieltjesOfMeasurableRat_unit_prod ρ]

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a => ↑(stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)) ↑r) =ᶠ[ae ρ.fst] fun a =>
    (preCDF ρ r a).toReal

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝ : IsFiniteMeasure ρ
r : ℚ
⊢ (fun a => ↑(stieltjesOfMeasurableRat (fun p r => (preCDF ρ r p.2).toReal) ⋯ ((), a)) ↑r) =ᶠ[ae ρ.fst] fun a =>
    (preCDF ρ r a).toReal

Tactic:
exact stieltjesOfMeasurableRat_ae_eq (isRatCondKernelCDF_preCDF ρ) () r

Result:
no goals
-- Mathlib/Order/Interval/Set/WithBotTop.lean
theorem image_coe_Iic : (some : α → WithBot α) '' Iic a = Ioc (⊥ : WithBot α) a

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
⊢ some '' Iic a = Ioc ⊥ ↑a

Tactic:
rw [← preimage_coe_Iic, image_preimage_eq_inter_range, range_coe, inter_comm, Ioi_inter_Iic]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Pointwise.lean
theorem mem_inv_pointwise_smul_iff {a : M} {S : Ideal R} {x : R} : x ∈ a⁻¹ • S ↔ a • x ∈ S

Proof state:
M : Type u_1
R : Type u_2
inst✝² : Group M
inst✝¹ : Semiring R
inst✝ : MulSemiringAction M R
a : M
S : Ideal R
x : R
⊢ x ∈ a⁻¹ • S ↔ a • x ∈ S

Tactic:
rw [mem_pointwise_smul_iff_inv_smul_mem, inv_inv]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
theorem whiskerLeft_comp (Q : LocalizedMonoidal L W ε) {X Y Z : LocalizedMonoidal L W ε}
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    Q ◁ (f ≫ g) = Q ◁ f ≫ Q ◁ g

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Q X Y Z : LocalizedMonoidal L W ε
f : X ⟶ Y
g : Y ⟶ Z
⊢ Q ◁ (f ≫ g) = Q ◁ f ≫ Q ◁ g

Tactic:
simp only [← id_tensorHom, ← tensor_comp, comp_id]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem tail_cons : tail (cons x p) = p

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
⊢ tail (cons x p) = p

Tactic:
simp (config := { unfoldPartialApp := true }) [tail, cons]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Fin/Fold.lean
theorem dfoldlM_loop_eq [Monad m] (f : ∀ (i : Fin n), α i.castSucc → m (α i.succ)) (x) :
    dfoldlM.loop n α f n (Nat.le_refl _) x = pure x

Proof state:
m : Type u_1 → Type u_2
n : Nat
α : Fin (n + 1) → Type u_1
inst✝ : Monad m
f : (i : Fin n) → α i.castSucc → m (α i.succ)
x : α ⟨n, ⋯⟩
⊢ dfoldlM.loop n α f n ⋯ x = pure x

Tactic:
rw [dfoldlM.loop, dif_neg (Nat.lt_irrefl _), cast_eq]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem div_eq_div_iff (ha : a ≠ 0) (ha' : a ≠ ∞) (hb : b ≠ 0) (hb' : b ≠ ∞) :
    c / b = d / a ↔ a * c = b * d

Proof state:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ b * d = a * c

Tactic:
rw [← eq_div_iff hb hb', mul_div_assoc, eq_comm]

Result:
no goals

Proof state:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ c / b = d / a ↔ a * c = b * d

Tactic:
rw [eq_div_iff ha ha']

Result:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ a * c = b * d

Proof state:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ a * c = b * d

Tactic:
conv_rhs => rw [eq_comm]

Result:
a b c d : ℝ≥0∞
ha : a ≠ 0
ha' : a ≠ ⊤
hb : b ≠ 0
hb' : b ≠ ⊤
⊢ a * (c / b) = d ↔ b * d = a * c
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem degree_cyclotomic' {ζ : R} {n : ℕ} (h : IsPrimitiveRoot ζ n) :
    (cyclotomic' n R).degree = Nat.totient n

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
ζ : R
n : ℕ
h : IsPrimitiveRoot ζ n
⊢ (cyclotomic' n R).degree = ↑n.totient

Tactic:
simp only [degree_eq_natDegree (cyclotomic'_ne_zero n R), natDegree_cyclotomic' h]

Result:
no goals
-- Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean
theorem mem_box : x ∈ box n d ↔ ∀ i, x i < d

Proof state:
n d : ℕ
x : Fin n → ℕ
⊢ x ∈ box n d ↔ ∀ (i : Fin n), x i < d

Tactic:
simp only [box, Fintype.mem_piFinset, mem_range]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Dimension.lean
lemma Limits.IsZero.hasProjectiveDimensionLT_zero (hX : IsZero X) :
    HasProjectiveDimensionLT X 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X 0

Tactic:
rw [hasProjectiveDimensionLT_iff]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Tactic:
rw [← e.mk₀_id_comp, hX.eq_of_src (𝟙 X) 0, Ext.mk₀_zero, Ext.zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ ∀ (i : ℕ), 0 ≤ i → ∀ ⦃Y : C⦄ (e : Ext X Y i), e = 0

Tactic:
intro i hi Y e

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
i : ℕ
hi : 0 ≤ i
Y : C
e : Ext X Y i
⊢ e = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
⊢ HasProjectiveDimensionLT X 0

Tactic:
letI := HasExt.standard C

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
hX : IsZero X
this : HasExt C := HasExt.standard C
⊢ HasProjectiveDimensionLT X 0
-- Mathlib/Order/SuccPred/Basic.lean
lemma isMin_of_not_pred_mem [PredOrder α] {a : s} (h : pred ↑a ∉ s) : IsMin a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ pred a = a

Tactic:
change dite .. = _

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ (if h : pred ↑a ∈ s then ⟨pred ↑a, h⟩ else a) = a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ IsMin a

Tactic:
rw [← pred_eq_iff_isMin]

Result:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ pred a = a

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ (if h : pred ↑a ∈ s then ⟨pred ↑a, h⟩ else a) = a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_3
inst✝² : PartialOrder α
s : Set α
inst✝¹ : s.OrdConnected
inst✝ : PredOrder α
a : ↑s
h : pred ↑a ∉ s
⊢ IsMin a

Tactic:
classical
rw [← pred_eq_iff_isMin]
change dite .. = _
simp [h]

Result:
no goals
-- Mathlib/RingTheory/Flat/EquationalCriterion.lean
theorem isTrivialRelation_iff_vanishesTrivially :
    IsTrivialRelation f x ↔ VanishesTrivially R f x

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_3
inst✝ : Fintype ι
f : ι → R
x : ι → M
⊢ IsTrivialRelation f x ↔ VanishesTrivially R f x

Tactic:
simp only [IsTrivialRelation, VanishesTrivially, smul_eq_mul, mul_comm]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rtakeWhile_concat (x : α) :
    rtakeWhile p (l ++ [x]) = if p x then rtakeWhile p l ++ [x] else []

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ rtakeWhile p (l ++ [x]) = if p x = true then rtakeWhile p l ++ [x] else []

Tactic:
simp only [rtakeWhile, takeWhile, reverse_append, reverse_singleton, singleton_append]

Result:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []

Proof state:
α : Type u_1
p : α → Bool
l : List α
x : α
⊢ (match p x with
      | true => x :: takeWhile p l.reverse
      | false => []).reverse =
    if p x = true then (takeWhile p l.reverse).reverse ++ [x] else []

Tactic:
split_ifs with h <;> simp [h]

Result:
no goals
-- Mathlib/RingTheory/Coalgebra/Basic.lean
@[simp]
lemma sum_counit_tmul_eq {a : A} (repr : Coalgebra.Repr R a) :
    ∑ i ∈ repr.index, counit (R := R) (repr.left i) ⊗ₜ (repr.right i) = 1 ⊗ₜ[R] a

Proof state:
R : Type u
A : Type v
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid A
inst✝¹ : Module R A
inst✝ : Coalgebra R A
a : A
repr : Repr R a
⊢ ∑ i ∈ repr.index, counit (repr.left i) ⊗ₜ[R] repr.right i = 1 ⊗ₜ[R] a

Tactic:
simpa [← repr.eq, map_sum] using congr($(rTensor_counit_comp_comul (R := R) (A := A)) a)

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem finrank_bot : finrank F (⊥ : IntermediateField F E) = 1

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ finrank F ↥⊥ = 1

Tactic:
rw [finrank_eq_one_iff]

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
@[simp]
lemma centralMoment_zero_measure : centralMoment X p (0 : Measure Ω) = 0

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
p : ℕ
⊢ centralMoment X p 0 = 0

Tactic:
simp [centralMoment]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
@[simp, norm_cast]
lemma ofReal_nonneg {x : ℝ} : 0 ≤ (x : K) ↔ 0 ≤ x

Proof state:
K : Type u_1
inst✝ : RCLike K
x : ℝ
⊢ 0 ≤ ↑x ↔ 0 ≤ x

Tactic:
rw [← ofReal_zero, ofReal_le_ofReal]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
theorem Sphere.ne_iff {s₁ s₂ : Sphere P} :
    s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius

Proof state:
P : Type u_2
inst✝ : MetricSpace P
s₁ s₂ : Sphere P
⊢ s₁ ≠ s₂ ↔ s₁.center ≠ s₂.center ∨ s₁.radius ≠ s₂.radius

Tactic:
rw [← not_and_or, ← Sphere.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/Discriminant.lean
theorem discr_not_zero_of_basis [Algebra.IsSeparable K L] (b : Basis ι K L) :
    discr K b ≠ 0

Proof state:
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ discr K ⇑b ≠ 0

Tactic:
rw [discr_def, traceMatrix_of_basis, ← LinearMap.BilinForm.nondegenerate_iff_det_ne_zero]

Result:
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ (traceForm K L).Nondegenerate

Proof state:
ι : Type w
inst✝⁶ : DecidableEq ι
inst✝⁵ : Fintype ι
K : Type u
L : Type v
inst✝⁴ : Field K
inst✝³ : Field L
inst✝² : Algebra K L
inst✝¹ : Module.Finite K L
inst✝ : Algebra.IsSeparable K L
b : Basis ι K L
⊢ (traceForm K L).Nondegenerate

Tactic:
exact traceForm_nondegenerate _ _

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_pointReflection (x y : P) : Wbtw R y x (pointReflection R x y)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 0 ≤ 2⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (lineMap y ((pointReflection R x) y)) 2⁻¹ = x

Tactic:
rw [lineMap_apply, pointReflection_apply, vadd_vsub_assoc, ← two_smul R (x -ᵥ y)]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ • 2 • (x -ᵥ y) +ᵥ y = x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ • 2 • (x -ᵥ y) +ᵥ y = x

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ 2⁻¹ ≤ 1

Tactic:
norm_num

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ Wbtw R y x ((pointReflection R x) y)

Tactic:
refine ⟨2⁻¹, ⟨by norm_num, by norm_num⟩, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x y : P
⊢ (lineMap y ((pointReflection R x) y)) 2⁻¹ = x
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem inner_add_right (x y z : E) : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ ⟪x, y + z⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

Tactic:
rw [← inner_conj_symm, inner_add_left, RingHom.map_add]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y z : E
⊢ (starRingEnd 𝕜) ⟪y, x⟫_𝕜 + (starRingEnd 𝕜) ⟪z, x⟫_𝕜 = ⟪x, y⟫_𝕜 + ⟪x, z⟫_𝕜

Tactic:
simp only [inner_conj_symm]

Result:
no goals
-- Mathlib/CategoryTheory/Idempotents/Karoubi.lean
theorem decomp_p (P : Karoubi C) : (toKaroubi C).map P.p = decompId_p P ≫ decompId_i P

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ (toKaroubi C).map P.p = P.decompId_p ≫ P.decompId_i

Tactic:
ext

Result:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (P.decompId_p ≫ P.decompId_i).f

Proof state:
case h
C : Type u_1
inst✝ : Category.{u_2, u_1} C
P : Karoubi C
⊢ ((toKaroubi C).map P.p).f = (P.decompId_p ≫ P.decompId_i).f

Tactic:
simp only [comp_f, decompId_p_f, decompId_i_f, P.idem, toKaroubi_map_f]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem sup_ind (a b : α) {p : α → Prop} (ha : p a) (hb : p b) : p (a ⊔ b) :=
  (IsTotal.total a b).elim (fun h : a ≤ b => by rwa [sup_eq_right.2 h]) fun h => by
  rwa [sup_eq_left.2 h]

Proof state:
α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : a ≤ b
⊢ p (a ⊔ b)

Tactic:
rwa [sup_eq_right.2 h]

Result:
no goals

Proof state:
α : Type u
inst✝ : LinearOrder α
a b : α
p : α → Prop
ha : p a
hb : p b
h : b ≤ a
⊢ p (a ⊔ b)

Tactic:
rwa [sup_eq_left.2 h]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_add_eq_iff_add_mul_eq_mul {x} {y : M} {z₁ z₂} :
    mk' S x y + z₁ = z₂ ↔ algebraMap R S x + z₁ * algebraMap R S y = z₂ * algebraMap R S y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
z₁ z₂ : S
⊢ mk' S x y + z₁ = z₂ ↔ (algebraMap R S) x + z₁ * (algebraMap R S) ↑y = z₂ * (algebraMap R S) ↑y

Tactic:
rw [← mk'_spec S x y, ← IsUnit.mul_left_inj (IsLocalization.map_units S y), right_distrib]

Result:
no goals
-- Mathlib/Topology/Order/OrderClosed.lean
theorem PredOrder.nhdsLT [PredOrder α] : 𝓝[<] a = ⊥

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
h : IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
simp [h.Iio_eq]

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
h : ¬IsMin a
⊢ 𝓝[<] a = ⊥

Tactic:
exact (Order.pred_covBy_of_not_isMin h).nhdsLT

Result:
no goals

Proof state:
α : Type u
inst✝³ : TopologicalSpace α
inst✝² : LinearOrder α
inst✝¹ : ClosedIicTopology α
a : α
inst✝ : PredOrder α
⊢ 𝓝[<] a = ⊥

Tactic:
if h : IsMin a then simp [h.Iio_eq]
else exact (Order.pred_covBy_of_not_isMin h).nhdsLT

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/Contraction.lean
theorem contractLeftAux_contractLeftAux (v : M) (x : CliffordAlgebra Q) (fx : CliffordAlgebra Q) :
    contractLeftAux Q d v (ι Q v * x, contractLeftAux Q d v (x, fx)) = Q v • fx

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ ((contractLeftAux Q d) v) ((ι Q) v * x, ((contractLeftAux Q d) v) (x, fx)) = Q v • fx

Tactic:
simp only [contractLeftAux_apply_apply]

Result:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - (ι Q) v * (d v • x - (ι Q) v * fx) = Q v • fx

Proof state:
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
d : Module.Dual R M
v : M
x fx : CliffordAlgebra Q
⊢ d v • ((ι Q) v * x) - (ι Q) v * (d v • x - (ι Q) v * fx) = Q v • fx

Tactic:
rw [mul_sub, ← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, ← sub_add, mul_smul_comm, sub_self,
  zero_add]

Result:
no goals
-- Mathlib/RingTheory/Finiteness/Cardinality.lean
/-- A finite module admits a surjective linear map from a finite free module. -/
lemma exists_fin' [Module.Finite R M] : ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), Surjective f

Proof state:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
⊢ ∃ n f, Surjective ⇑f

Tactic:
have ⟨n, s, hs⟩ := exists_fin (R := R) (M := M)

Result:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
hs : span R (Set.range s) = ⊤
⊢ ∃ n f, Surjective ⇑f

Proof state:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
hs : span R (Set.range s) = ⊤
⊢ ∃ n f, Surjective ⇑f

Tactic:
refine ⟨n, Basis.constr (Pi.basisFun R _) ℕ s, ?_⟩

Result:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
hs : span R (Set.range s) = ⊤
⊢ Surjective ⇑(((Pi.basisFun R (Fin n)).constr ℕ) s)

Proof state:
R : Type u
M : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Module.Finite R M
n : ℕ
s : Fin n → M
hs : span R (Set.range s) = ⊤
⊢ Surjective ⇑(((Pi.basisFun R (Fin n)).constr ℕ) s)

Tactic:
rw [← LinearMap.range_eq_top, Basis.constr_range, hs]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem bot_lt_affineSpan : ⊥ < affineSpan k s ↔ s.Nonempty

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅

Tactic:
exact (affineSpan_eq_bot _).not

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ ⊥ < affineSpan k s ↔ s.Nonempty

Tactic:
rw [bot_lt_iff_ne_bot, nonempty_iff_ne_empty]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
⊢ affineSpan k s ≠ ⊥ ↔ s ≠ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem rotateLeft_def {x : BitVec w} {r : Nat} :
    x.rotateLeft r = (x <<< (r % w)) ||| (x >>> (w - r % w))

Proof state:
w : Nat
x : BitVec w
r : Nat
⊢ x.rotateLeft r = x <<< (r % w) ||| x >>> (w - r % w)

Tactic:
simp only [rotateLeft, rotateLeftAux]

Result:
no goals