harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_left_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle (r • x) x = 0

Proof state:
case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle (r • x) x = 0

Tactic:
simp [h.symm]

Result:
no goals

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
⊢ o.oangle (r • x) x = 0

Tactic:
rcases hr.lt_or_eq with (h | h)

Result:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle (r • x) x = 0

case inr
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 = r
⊢ o.oangle (r • x) x = 0

Proof state:
case inl
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x : V
r : ℝ
hr : 0 ≤ r
h : 0 < r
⊢ o.oangle (r • x) x = 0

Tactic:
simp [h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNormEssSup_eq_zero_iff {f : α → F} : eLpNormEssSup f μ = 0 ↔ f =ᵐ[μ] 0

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
⊢ eLpNormEssSup f μ = 0 ↔ f =ᶠ[ae μ] 0

Tactic:
simp [EventuallyEq, eLpNormEssSup_eq_essSup_enorm]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem tendsto_of_tendsto_normalize_testAgainstNN_of_tendsto_mass {γ : Type*} {F : Filter γ}
    {μs : γ → FiniteMeasure Ω} (μs_lim : Tendsto (fun i ↦ (μs i).normalize) F (𝓝 μ.normalize))
    (mass_lim : Tendsto (fun i ↦ (μs i).mass) F (𝓝 μ.mass)) : Tendsto μs F (𝓝 μ)

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))

Tactic:
exact fun f ↦
  tendsto_testAgainstNN_of_tendsto_normalize_testAgainstNN_of_tendsto_mass μs_lim mass_lim f

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
⊢ Tendsto μs F (𝓝 μ)

Tactic:
rw [tendsto_iff_forall_testAgainstNN_tendsto]

Result:
Ω : Type u_1
inst✝² : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
γ : Type u_2
F : Filter γ
μs : γ → FiniteMeasure Ω
μs_lim : Tendsto (fun i => (μs i).normalize) F (𝓝 μ.normalize)
mass_lim : Tendsto (fun i => (μs i).mass) F (𝓝 μ.mass)
⊢ ∀ (f : Ω →ᵇ ℝ≥0), Tendsto (fun i => (μs i).testAgainstNN f) F (𝓝 (μ.testAgainstNN f))
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[simp]
lemma iso_inv_base_hom_base {X Y : LocallyRingedSpace.{u}} (e : X ≅ Y) :
    e.inv.base ≫ e.hom.base = 𝟙 _

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ e.inv.base ≫ e.hom.base = 𝟙 ↑Y.toPresheafedSpace

Tactic:
rw [← SheafedSpace.comp_base, ← LocallyRingedSpace.comp_toShHom]

Result:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ (Hom.toShHom (e.inv ≫ e.hom)).base = 𝟙 ↑Y.toPresheafedSpace

Proof state:
X Y : LocallyRingedSpace
e : X ≅ Y
⊢ (Hom.toShHom (e.inv ≫ e.hom)).base = 𝟙 ↑Y.toPresheafedSpace

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_nonpos_iff_of_base_lt_one (hx : 0 < x) : logb b x ≤ 0 ↔ 1 ≤ x

Proof state:
b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ 0 ↔ 1 ≤ x

Tactic:
rw [← not_lt, logb_pos_iff_of_base_lt_one b_pos b_lt_one hx, not_lt]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Charpoly/Univ.lean
@[simp]
lemma univ_coeff_eval₂Hom (M : n × n → S) (i : ℕ) :
    MvPolynomial.eval₂Hom f M ((univ R n).coeff i) =
      (charpoly (Matrix.of M.curry)).coeff i

Proof state:
R : Type u_1
S : Type u_2
n : Type u_3
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fintype n
inst✝ : DecidableEq n
f : R →+* S
M : n × n → S
i : ℕ
⊢ (MvPolynomial.eval₂Hom f M) ((univ R n).coeff i) = (of (Function.curry M)).charpoly.coeff i

Tactic:
rw [← univ_map_eval₂Hom n f M, Polynomial.coeff_map]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean
@[simp]
lemma volume_ball_fin_two (x : EuclideanSpace ℝ (Fin 2)) (r : ℝ) :
    volume (ball x r) = .ofReal r ^ 2 * .ofReal π

Proof state:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ volume (ball x r) = ENNReal.ofReal r ^ 2 * ENNReal.ofReal π

Tactic:
norm_num [InnerProductSpace.volume_ball_of_dim_even (k := 1) (by simp) x]

Result:
no goals

Proof state:
x : EuclideanSpace ℝ (Fin 2)
r : ℝ
⊢ Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2 * 1

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CondCDF.lean
lemma lintegral_preCDF_fst (ρ : Measure (α × ℝ)) (r : ℚ) [IsFiniteMeasure ρ] :
    ∫⁻ x, preCDF ρ r x ∂ρ.fst = ρ.IicSnd r univ

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
r : ℚ
inst✝ : IsFiniteMeasure ρ
⊢ ∫⁻ (x : α), preCDF ρ r x ∂ρ.fst = (ρ.IicSnd ↑r) univ

Tactic:
rw [← setLIntegral_univ, setLIntegral_preCDF_fst ρ r MeasurableSet.univ]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_bit1 [Semiring α] (n : Num) : (n.bit1 : α) = 2 * (n : α) + 1

Proof state:
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ 2 * ↑n + ↑1 = 2 * ↑n + 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ ↑n.bit1 = 2 * ↑n + 1

Tactic:
rw [← bit1_of_bit1, bit0_of_bit0, cast_add, cast_bit0]

Result:
α : Type u_1
inst✝ : Semiring α
n : Num
⊢ 2 * ↑n + ↑1 = 2 * ↑n + 1
-- Mathlib/Data/Matrix/Basis.lean
theorem stdBasisMatrix_eq_single_vecMulVec_single [MulZeroOneClass α] (i : m) (j : n) :
    stdBasisMatrix i j (1 : α) = vecMulVec (Pi.single i 1) (Pi.single j 1)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ stdBasisMatrix i j 1 = vecMulVec (Pi.single i 1) (Pi.single j 1)

Tactic:
ext i' j'

Result:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (Pi.single i 1) (Pi.single j 1) i' j'

Proof state:
case a
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
i' : m
j' : n
⊢ stdBasisMatrix i j 1 i' j' = vecMulVec (Pi.single i 1) (Pi.single j 1) i' j'

Tactic:
simp [-mul_ite, stdBasisMatrix, vecMulVec, ite_and, Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_eq_ofReal_iff {p q : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) :
    ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

Proof state:
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
⊢ ENNReal.ofReal p = ENNReal.ofReal q ↔ p = q

Tactic:
rw [ENNReal.ofReal, ENNReal.ofReal, coe_inj, Real.toNNReal_eq_toNNReal_iff hp hq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem neg_eval (lc : LinearCombo) (v : Coeffs) : (-lc).eval v = - lc.eval v

Proof state:
case mk
v : Coeffs
a : Int
coeffs : Coeffs
⊢ (-{ const := a, coeffs := coeffs }).eval v = -{ const := a, coeffs := coeffs }.eval v

Tactic:
simp [eval, Int.neg_add]

Result:
no goals

Proof state:
lc : LinearCombo
v : Coeffs
⊢ (-lc).eval v = -lc.eval v

Tactic:
rcases lc with ⟨a, coeffs⟩

Result:
case mk
v : Coeffs
a : Int
coeffs : Coeffs
⊢ (-{ const := a, coeffs := coeffs }).eval v = -{ const := a, coeffs := coeffs }.eval v
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem toListModel_filterMapₘ {m : Raw₀ α β} {f : (a : α) → β a → Option (δ a)} :
    Perm (toListModel (m.filterMapₘ f).1.buckets)
      ((toListModel m.1.buckets).filterMap fun p => (f p.1 p.2).map (⟨p.1, ·⟩)) :=
  toListModel_updateAllBuckets AssocList.toList_filterMap
    (by simp [List.filterMap_append])

Proof state:
α : Type u
β : α → Type v
δ : α → Type w
m : Raw₀ α β
f : (a : α) → β a → Option (δ a)
⊢ ∀ {l l' : List ((a : α) × β a)},
    List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) (l ++ l') ~
      List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l ++
        List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l'

Tactic:
simp [List.filterMap_append]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_sdiff_div_prod_sdiff :
    (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Proof state:
α : Type u_3
β : Type u_4
s₁ s₂ : Finset α
f : α → β
inst✝¹ : CommGroup β
inst✝ : DecidableEq α
⊢ (∏ x ∈ s₂ \ s₁, f x) / ∏ x ∈ s₁ \ s₂, f x = (∏ x ∈ s₂, f x) / ∏ x ∈ s₁, f x

Tactic:
simp [← Finset.prod_sdiff (@inf_le_left _ _ s₁ s₂), ← Finset.prod_sdiff (@inf_le_right _ _ s₁ s₂)]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem le_inv_iff_le_inv : a ≤ b⁻¹ ↔ b ≤ a⁻¹

Proof state:
a b : ℝ≥0∞
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹

Tactic:
simpa only [inv_inv] using @ENNReal.inv_le_inv a⁻¹ b

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
theorem lintegral_rnDeriv_mul [HaveLebesgueDecomposition μ ν] (hμν : μ ≪ ν) {f : α → ℝ≥0∞}
    (hf : AEMeasurable f ν) : ∫⁻ x, μ.rnDeriv ν x * f x ∂ν = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)

Tactic:
rw [lintegral_withDensity_eq_lintegral_mul₀ (measurable_rnDeriv μ ν).aemeasurable hf]

Result:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂μ

Tactic:
nth_rw 2 [← withDensity_rnDeriv_eq μ ν hμν]

Result:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (x : α), f x ∂ν.withDensity (μ.rnDeriv ν)

Proof state:
α : Type u_3
m : MeasurableSpace α
μ ν : Measure α
inst✝ : μ.HaveLebesgueDecomposition ν
hμν : μ ≪ ν
f : α → ℝ≥0∞
hf : AEMeasurable f ν
⊢ ∫⁻ (x : α), μ.rnDeriv ν x * f x ∂ν = ∫⁻ (a : α), (μ.rnDeriv ν * f) a ∂ν

Tactic:
simp only [Pi.mul_apply]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_expand_image_iterateFrobenius [DecidableEq R] :
    (expand R (p ^ n) f).roots.toFinset.image (iterateFrobenius R p n) = f.roots.toFinset

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
p n : ℕ
inst✝² : ExpChar R p
f : R[X]
inst✝¹ : PerfectRing R p
inst✝ : DecidableEq R
⊢ Finset.image (⇑(iterateFrobenius R p n)) ((expand R (p ^ n)) f).roots.toFinset = f.roots.toFinset

Tactic:
rw [Finset.image_toFinset, roots_expand_pow_map_iterateFrobenius,
  (roots f).toFinset_nsmul _ (expChar_pow_pos R p n).ne']

Result:
no goals
-- Mathlib/Algebra/Polynomial/Div.lean
lemma rootMultiplicity_le_iff (p0 : p ≠ 0) (a : R) (n : ℕ) :
    rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
p0 : p ≠ 0
a : R
n : ℕ
⊢ rootMultiplicity a p ≤ n ↔ ¬(X - C a) ^ (n + 1) ∣ p

Tactic:
rw [← (le_rootMultiplicity_iff p0).not, not_le, Nat.lt_add_one_iff]

Result:
no goals
-- Mathlib/Data/List/MinMax.lean
theorem minimum_le_coe_iff : l.minimum ≤ a ↔ ∃ b, b ∈ l ∧ b ≤ a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
l : List α
a : α
⊢ l.minimum ≤ ↑a ↔ ∃ b, b ∈ l ∧ b ≤ a

Tactic:
induction' l <;> simp [minimum_cons, *]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
lemma add_left_inj [IsLeftCancelAdd α] (hx : x ≠ ⊤) : x + y = x + z ↔ y = z

Proof state:
case intro
α : Type u
inst✝¹ : Add α
y z : WithTop α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z

Tactic:
cases y <;> cases z <;> simp [← coe_add]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : Add α
x y z : WithTop α
inst✝ : IsLeftCancelAdd α
hx : x ≠ ⊤
⊢ x + y = x + z ↔ y = z

Tactic:
lift x to α using hx

Result:
case intro
α : Type u
inst✝¹ : Add α
y z : WithTop α
inst✝ : IsLeftCancelAdd α
x : α
⊢ ↑x + y = ↑x + z ↔ y = z
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem periodicOrbit_length : (periodicOrbit f x).length = minimalPeriod f x

Proof state:
α : Type u_1
f : α → α
x : α
⊢ (periodicOrbit f x).length = minimalPeriod f x

Tactic:
rw [periodicOrbit, Cycle.length_coe, List.length_map, List.length_range]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Cardinal.lean
theorem cardinalMk_eq_max {R : Type u} [Semiring R] [Nontrivial R] : #(R[X]) = max #R ℵ₀ :=
  (toFinsuppIso R).toEquiv.cardinal_eq.trans <| by
    rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]
    rfl

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #R ⊔ lift.{u, 0} #ℕ = #R ⊔ ℵ₀

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #(AddMonoidAlgebra R ℕ) = #R ⊔ ℵ₀

Tactic:
rw [AddMonoidAlgebra, mk_finsupp_lift_of_infinite, lift_uzero, max_comm]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ #R ⊔ lift.{u, 0} #ℕ = #R ⊔ ℵ₀
-- Mathlib/Data/Set/Card.lean
theorem encard_exchange' (ha : a ∉ s) (hb : b ∈ s) : (insert a s \ {b}).encard = s.encard

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ a ≠ b

Tactic:
rintro rfl

Result:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Proof state:
α : Type u_1
s : Set α
a : α
ha : a ∉ s
hb : a ∈ s
⊢ False

Tactic:
exact ha hb

Result:
no goals

Proof state:
α : Type u_1
s : Set α
a b : α
ha : a ∉ s
hb : b ∈ s
⊢ (insert a s \ {b}).encard = s.encard

Tactic:
rw [← insert_diff_singleton_comm (by rintro rfl; exact ha hb), encard_exchange ha hb]

Result:
no goals
-- Mathlib/SetTheory/Surreal/Dyadic.lean
theorem powHalf_pos (n : ℕ) : 0 < powHalf n

Proof state:
n : ℕ
⊢ ∃ i, 0 ≤ (powHalf n).moveLeft i

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < powHalf n

Tactic:
rw [← lf_iff_lt numeric_zero (numeric_powHalf n), zero_lf_le]

Result:
n : ℕ
⊢ ∃ i, 0 ≤ (powHalf n).moveLeft i
-- Mathlib/Data/Matroid/Closure.lean
lemma IsBase.eq_of_superset_spanning (hB : M.IsBase B) (hX : M.Spanning X) (hXB : X ⊆ B) : B = X :=
  have ⟨B', hB', hB'X⟩ := hX.exists_isBase_subset
  subset_antisymm (by rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]) hXB

Proof state:
α : Type u_2
M : Matroid α
X B : Set α
hB : M.IsBase B
hX : M.Spanning X
hXB : X ⊆ B
B' : Set α
hB' : M.IsBase B'
hB'X : B' ⊆ X
⊢ B ⊆ X

Tactic:
rwa [← hB'.eq_of_subset_isBase hB (hB'X.trans hXB)]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/FixedDetMatrices.lean
lemma reduce_of_pos {A : Δ m} (hc : (A.1 1 0) = 0) (ha : 0 < A.1 0 0) :
    reduce A = (T ^ (-(A.1 0 1 / A.1 1 1))) • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ reduce A = T ^ (-(↑A 0 1 / ↑A 1 1)) • A

Tactic:
rw [reduce]

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then T ^ (-(↑A 0 1 / ↑A 1 1)) • A else T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(↑A 0 1 / ↑A 1 1)) • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then T ^ (-(↑A 0 1 / ↑A 1 1)) • A else T ^ (-(-↑A 0 1 / -↑A 1 1)) • S • S • A
    else reduce (reduceStep A)) =
    T ^ (-(↑A 0 1 / ↑A 1 1)) • A

Tactic:
simp only [zpow_neg, Int.ediv_neg, neg_neg] at *

Result:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A

Proof state:
m : ℤ
A : FixedDetMatrix (Fin 2) ℤ m
hc : ↑A 1 0 = 0
ha : 0 < ↑A 0 0
⊢ (if ↑A 1 0 = 0 then if 0 < ↑A 0 0 then (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A else T ^ (-↑A 0 1 / ↑A 1 1) • S • S • A
    else reduce (reduceStep A)) =
    (T ^ (↑A 0 1 / ↑A 1 1))⁻¹ • A

Tactic:
simp_rw [if_pos hc, if_pos ha]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem ofReal_lt_iff_lt_toReal {a : ℝ} {b : ℝ≥0∞} (ha : 0 ≤ a) (hb : b ≠ ∞) :
    ENNReal.ofReal a < b ↔ a < ENNReal.toReal b

Proof state:
a : ℝ
b : ℝ≥0∞
ha : 0 ≤ a
hb : b ≠ ⊤
⊢ ENNReal.ofReal a < b ↔ a < b.toReal

Tactic:
lift b to ℝ≥0 using hb

Result:
case intro
a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ ENNReal.ofReal a < ↑b ↔ a < (↑b).toReal

Proof state:
case intro
a : ℝ
ha : 0 ≤ a
b : ℝ≥0
⊢ ENNReal.ofReal a < ↑b ↔ a < (↑b).toReal

Tactic:
simpa [ENNReal.ofReal, ENNReal.toReal] using Real.toNNReal_lt_iff_lt_coe ha

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_X : (X : F[X]).natSepDegree = 1

Proof state:
F : Type u
inst✝ : Field F
⊢ X.natSepDegree = 1

Tactic:
simp only [natSepDegree, aroots_X, Multiset.toFinset_singleton, Finset.card_singleton]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem prod_bij' (i : ∀ a ∈ s, κ) (j : ∀ a ∈ t, ι) (hi : ∀ a ha, i a ha ∈ t)
    (hj : ∀ a ha, j a ha ∈ s) (left_inv : ∀ a ha, j (i a ha) (hi a ha) = a)
    (right_inv : ∀ a ha, i (j a ha) (hj a ha) = a) (h : ∀ a ha, f a = g (i a ha)) :
    ∏ x ∈ s, f x = ∏ x ∈ t, g x

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
⊢ ∏ x ∈ s, f x = ∏ x ∈ t, g x

Tactic:
refine prod_bij i hi (fun a1 h1 a2 h2 eq ↦ ?_) (fun b hb ↦ ⟨_, hj b hb, right_inv b hb⟩) h

Result:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯

Tactic:
simp only [eq]

Result:
no goals

Proof state:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ a1 = a2

Tactic:
rw [← left_inv a1 h1, ← left_inv a2 h2]

Result:
ι : Type u_6
κ : Type u_7
α : Type u_8
inst✝ : CommMonoid α
s : Finset ι
t : Finset κ
f : ι → α
g : κ → α
i : (a : ι) → a ∈ s → κ
j : (a : κ) → a ∈ t → ι
hi : ∀ (a : ι) (ha : a ∈ s), i a ha ∈ t
hj : ∀ (a : κ) (ha : a ∈ t), j a ha ∈ s
left_inv : ∀ (a : ι) (ha : a ∈ s), j (i a ha) ⋯ = a
right_inv : ∀ (a : κ) (ha : a ∈ t), i (j a ha) ⋯ = a
h : ∀ (a : ι) (ha : a ∈ s), f a = g (i a ha)
a1 : ι
h1 : a1 ∈ s
a2 : ι
h2 : a2 ∈ s
eq : i a1 h1 = i a2 h2
⊢ j (i a1 h1) ⋯ = j (i a2 h2) ⋯
-- Mathlib/Algebra/Polynomial/Div.lean
theorem X_dvd_iff {f : R[X]} : X ∣ f ↔ f.coeff 0 = 0 :=
  ⟨fun ⟨g, hfg⟩ => by rw [hfg, coeff_X_mul_zero], fun hf =>
    ⟨f.divX, by rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]⟩⟩

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
x✝ : X ∣ f
g : R[X]
hfg : f = X * g
⊢ f.coeff 0 = 0

Tactic:
rw [hfg, coeff_X_mul_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
hf : f.coeff 0 = 0
⊢ f = X * f.divX

Tactic:
rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]

Result:
no goals
-- Mathlib/Analysis/Convex/Intrinsic.lean
theorem intrinsicFrontier_singleton (x : P) : intrinsicFrontier 𝕜 ({x} : Set P) = ∅

Proof state:
𝕜 : Type u_1
V : Type u_2
P : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : AddCommGroup V
inst✝² : Module 𝕜 V
inst✝¹ : TopologicalSpace P
inst✝ : AddTorsor V P
x : P
⊢ intrinsicFrontier 𝕜 {x} = ∅

Tactic:
rw [intrinsicFrontier, preimage_coe_affineSpan_singleton, frontier_univ, image_empty]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean
theorem OrthonormalBasis.addHaar_eq_volume {ι F : Type*} [Fintype ι] [NormedAddCommGroup F]
    [InnerProductSpace ℝ F] [FiniteDimensional ℝ F] [MeasurableSpace F] [BorelSpace F]
    (b : OrthonormalBasis ι ℝ F) :
    b.toBasis.addHaar = volume

Proof state:
ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ volume ↑b.toBasis.parallelepiped = 1

Tactic:
exact b.volume_parallelepiped

Result:
no goals

Proof state:
ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ b.toBasis.addHaar = volume

Tactic:
rw [Basis.addHaar_eq_iff]

Result:
ι : Type u_4
F : Type u_5
inst✝⁵ : Fintype ι
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace ℝ F
inst✝² : FiniteDimensional ℝ F
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
b : OrthonormalBasis ι ℝ F
⊢ volume ↑b.toBasis.parallelepiped = 1
-- Mathlib/Topology/GDelta/Basic.lean
theorem IsGδ.iInter_of_isOpen [Countable ι'] {f : ι' → Set X} (hf : ∀ i, IsOpen (f i)) :
    IsGδ (⋂ i, f i) :=
  ⟨range f, by rwa [forall_mem_range], countable_range _, by rw [sInter_range]⟩

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen (f i)
⊢ ⋂ i, f i = ⋂₀ range f

Tactic:
rw [sInter_range]

Result:
no goals

Proof state:
X : Type u_1
ι' : Sort u_4
inst✝¹ : TopologicalSpace X
inst✝ : Countable ι'
f : ι' → Set X
hf : ∀ (i : ι'), IsOpen (f i)
⊢ ∀ t ∈ range f, IsOpen t

Tactic:
rwa [forall_mem_range]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem upperClosure_sUnion (S : Set (Set α)) : upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s

Proof state:
α : Type u_1
inst✝ : Preorder α
S : Set (Set α)
⊢ upperClosure (⋃₀ S) = ⨅ s ∈ S, upperClosure s

Tactic:
simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]

Result:
no goals