harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalProperties/Reduced.lean
theorem isReduced_localizationPreserves : LocalizationPreserves fun R _ => IsReduced R

Proof state:
case eq_zero.intro.succ.intro.mk.intro
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = ↑m' * (y ^ n.succ * ↑m' ^ n)
⊢ x = 0

Tactic:
rw [← mul_left_comm, ← pow_succ', ← mul_pow] at hm'

Result:
case eq_zero.intro.succ.intro.mk.intro
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
y : R
m : ↥M
hx : x * (algebraMap R S) ↑m = (algebraMap R S) y
hx' : (algebraMap R S) 0 = (algebraMap R S) (y ^ n.succ)
m' : ↥M
hm' : 0 = (y * ↑m') ^ n.succ
⊢ x = 0

Proof state:
case eq_zero
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
⊢ ∀ (x : S), IsNilpotent x → x = 0

Tactic:
rintro x ⟨_ | n, e⟩

Result:
case eq_zero.intro.zero
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
e : x ^ 0 = 0
⊢ x = 0

case eq_zero.intro.succ
R : Type u_1
hR : CommRing R
M : Submonoid R
S : Type u_1
hS : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
a✝ : IsReduced R
x : S
n : ℕ
e : x ^ (n + 1) = 0
⊢ x = 0
-- Mathlib/Data/Set/Lattice.lean
lemma iInter₂_union_iInter₂ {ι₁ κ₁ : Sort*} {ι₂ : ι₁ → Sort*} {k₂ : κ₁ → Sort*}
    (f : ∀ i₁, ι₂ i₁ → Set α) (g : ∀ j₁, k₂ j₁ → Set α) :
    (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Proof state:
α : Type u_1
ι₁ : Sort u_12
κ₁ : Sort u_13
ι₂ : ι₁ → Sort u_14
k₂ : κ₁ → Sort u_15
f : (i₁ : ι₁) → ι₂ i₁ → Set α
g : (j₁ : κ₁) → k₂ j₁ → Set α
⊢ (⋂ i₁, ⋂ i₂, f i₁ i₂) ∪ ⋂ j₁, ⋂ j₂, g j₁ j₂ = ⋂ i₁, ⋂ i₂, ⋂ j₁, ⋂ j₂, f i₁ i₂ ∪ g j₁ j₂

Tactic:
simp_rw [iInter_union, union_iInter]

Result:
no goals
-- Mathlib/Data/Matroid/Restrict.lean
theorem isBase_restrict_iff' : (M ↾ X).IsBase I ↔ M.IsBasis' I X

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
⊢ (M ↾ X).IsBase I ↔ M.IsBasis' I X

Tactic:
simp_rw [isBase_iff_maximal_indep, IsBasis', maximal_iff, restrict_indep_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Presentation/Basic.lean
@[simp]
lemma π_comp_map_apply (x : relations.R →₀ A) : solution.π (relations.map x) = 0

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
x : relations.R →₀ A
⊢ (solution.π ∘ₗ relations.map) x = 0

Tactic:
rw [π_comp_map, LinearMap.zero_apply]

Result:
no goals

Proof state:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
x : relations.R →₀ A
⊢ solution.π (relations.map x) = 0

Tactic:
change solution.π.comp relations.map x = 0

Result:
A : Type u
inst✝² : Ring A
relations : Relations A
M : Type v
inst✝¹ : AddCommGroup M
inst✝ : Module A M
solution : relations.Solution M
x : relations.R →₀ A
⊢ (solution.π ∘ₗ relations.map) x = 0
-- Mathlib/Analysis/Seminorm.lean
theorem ball_eq_emptyset (p : Seminorm 𝕜 E) {x : E} {r : ℝ} (hr : r ≤ 0) : p.ball x r = ∅

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ x✝ ∈ p.ball x r ↔ x✝ ∈ ∅

Tactic:
rw [Seminorm.mem_ball, Set.mem_empty_iff_false, iff_false, not_lt]

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ r ≤ p (x✝ - x)

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
⊢ p.ball x r = ∅

Tactic:
ext

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ x✝ ∈ p.ball x r ↔ x✝ ∈ ∅

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
hr : r ≤ 0
x✝ : E
⊢ r ≤ p (x✝ - x)

Tactic:
exact hr.trans (apply_nonneg p _)

Result:
no goals
-- Mathlib/Tactic/NormNum/PowMod.lean
theorem natPow_zero_natMod_zero : Nat.mod (Nat.pow a (nat_lit 0)) (nat_lit 0) = nat_lit 1

Proof state:
a : ℕ
⊢ (a.pow 0).mod 0 = 1

Tactic:
with_unfolding_all rfl

Result:
no goals

Proof state:
a : ℕ
⊢ (a.pow 0).mod 0 = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Retract.lean
lemma retracts_le (P : MorphismProperty C) [P.IsStableUnderRetracts] :
    P.retracts ≤ P

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : MorphismProperty C
inst✝ : P.IsStableUnderRetracts
⊢ P.retracts ≤ P

Tactic:
rwa [← isStableUnderRetracts_iff_retracts_le]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Operations.lean
theorem comap_id (S : Submonoid P) : S.comap (MonoidHom.id P) = S :=
  ext (by simp)

Proof state:
P : Type u_3
inst✝ : MulOneClass P
S : Submonoid P
⊢ ∀ (x : P), x ∈ comap (MonoidHom.id P) S ↔ x ∈ S

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem map_symm_subset {t : Finset β} {f : α ≃ β} : t.map f.symm ⊆ s ↔ t ⊆ s.map f

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
f : α ≃ β
⊢ map f.symm.toEmbedding t ⊆ s ↔ t ⊆ map f.toEmbedding s

Tactic:
simp only [← subset_map_symm, Equiv.symm_symm]

Result:
no goals
-- Mathlib/Data/Complex/Order.lean
@[simp]
lemma neg_re_eq_norm {z : ℂ} : -z.re = ‖z‖ ↔ z ≤ 0

Proof state:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0

Tactic:
exact neg_nonneg.and <| eq_comm.trans neg_eq_zero

Result:
no goals

Proof state:
z : ℂ
⊢ -z.re = ‖z‖ ↔ z ≤ 0

Tactic:
rw [← neg_re, ← norm_neg z, re_eq_norm]

Result:
z : ℂ
⊢ 0 ≤ -z ↔ z ≤ 0
-- Mathlib/Algebra/Polynomial/Laurent.lean
lemma toLaurent_reverse (p : R[X]) :
    toLaurent p.reverse = invert (toLaurent p) * (T p.natDegree)

Proof state:
case M0
R : Type u_3
inst✝ : CommSemiring R
a✝ : Nontrivial R
⊢ toLaurent (reverse 0) = invert (toLaurent 0) * T ↑(natDegree 0)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
⊢ toLaurent p.reverse = invert (toLaurent p) * T ↑p.natDegree

Tactic:
nontriviality R

Result:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
a✝ : Nontrivial R
⊢ toLaurent p.reverse = invert (toLaurent p) * T ↑p.natDegree

Proof state:
case MC
R : Type u_3
inst✝ : CommSemiring R
a✝³ : Nontrivial R
p✝ : R[X]
a✝² : R
a✝¹ : p✝.coeff 0 = 0
a✝ : a✝² ≠ 0
ih : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ + Polynomial.C a✝²).reverse =
    invert (toLaurent (p✝ + Polynomial.C a✝²)) * T ↑(p✝ + Polynomial.C a✝²).natDegree

Tactic:
simp [add_mul, ← ih]

Result:
no goals

Proof state:
R : Type u_3
inst✝ : CommSemiring R
p : R[X]
a✝ : Nontrivial R
⊢ toLaurent p.reverse = invert (toLaurent p) * T ↑p.natDegree

Tactic:
induction p using Polynomial.recOnHorner with
| M0 => simp
| MC _ _ _ _ ih => simp [add_mul, ← ih]
| MX _ hp => simpa [natDegree_mul_X hp]

Result:
no goals

Proof state:
case MX
R : Type u_3
inst✝ : CommSemiring R
a✝¹ : Nontrivial R
p✝ : R[X]
hp : p✝ ≠ 0
a✝ : toLaurent p✝.reverse = invert (toLaurent p✝) * T ↑p✝.natDegree
⊢ toLaurent (p✝ * X).reverse = invert (toLaurent (p✝ * X)) * T ↑(p✝ * X).natDegree

Tactic:
simpa [natDegree_mul_X hp]

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem sorted_lt_range (n : ℕ) : Sorted (· < ·) (range n)

Proof state:
n : ℕ
⊢ Sorted (fun x1 x2 => x1 < x2) (range n)

Tactic:
rw [Sorted, pairwise_iff_get]

Result:
n : ℕ
⊢ ∀ (i j : Fin (range n).length), i < j → (range n).get i < (range n).get j

Proof state:
n : ℕ
⊢ ∀ (i j : Fin (range n).length), i < j → (range n).get i < (range n).get j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem lintegral_rnDeriv_lt_top_of_measure_ne_top (ν : Measure α) {s : Set α} (hs : μ s ≠ ∞) :
    ∫⁻ x in s, μ.rnDeriv ν x ∂ν < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ (μ.singularPart ν) (toMeasurable μ s) + (ν.withDensity (μ.rnDeriv ν)) (toMeasurable μ s) = μ s

Tactic:
rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

Tactic:
by_cases hl : HaveLebesgueDecomposition μ ν

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

Tactic:
suffices (∫⁻ x in toMeasurable μ s, μ.rnDeriv ν x ∂ν) < ∞ from
  lt_of_le_of_lt (lintegral_mono_set (subset_toMeasurable _ _)) this

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ⊤

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in toMeasurable μ s, μ.rnDeriv ν x ∂ν < ⊤

Tactic:
rw [← withDensity_apply _ (measurableSet_toMeasurable _ _)]

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ (ν.withDensity (μ.rnDeriv ν)) (toMeasurable μ s) < ⊤

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : ¬μ.HaveLebesgueDecomposition ν
⊢ ∫⁻ (x : α) in s, μ.rnDeriv ν x ∂ν < ⊤

Tactic:
simp only [Measure.rnDeriv, dif_neg hl, Pi.zero_apply, lintegral_zero, ENNReal.zero_lt_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ s ≠ ⊤
hl : μ.HaveLebesgueDecomposition ν
⊢ (ν.withDensity (μ.rnDeriv ν)) (toMeasurable μ s) < ⊤

Tactic:
calc
  _ ≤ (singularPart μ ν) (toMeasurable μ s) + _ := le_add_self
  _ = μ s := by rw [← Measure.add_apply, ← haveLebesgueDecomposition_add, measure_toMeasurable]
  _ < ⊤ := hs.lt_top

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_setIfInBounds_self_of_lt (as : Array α) {i : Nat} (v : α) (h : i < as.size) :
    (as.setIfInBounds i v)[i]? = some v

Proof state:
α : Type u_1
as : Array α
i : Nat
v : α
h : i < as.size
⊢ (as.setIfInBounds i v)[i]? = some v

Tactic:
simp [getElem?_setIfInBounds, h]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem lift_comp (g : M →ₗ[R] M'') (h : ∀ x : S, IsUnit ((algebraMap R (Module.End R M'')) x)) :
    (lift S f g h).comp f = g

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
⊢ lift S f g h ∘ₗ f = g

Tactic:
dsimp only [IsLocalizedModule.lift]

Result:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
⊢ (LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
g : M →ₗ[R] M''
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
⊢ (LocalizedModule.lift S g h ∘ₗ ↑(iso S f).symm) ∘ₗ f = g

Tactic:
rw [LinearMap.comp_assoc, iso_symm_comp, LocalizedModule.lift_comp S g h]

Result:
no goals
-- Mathlib/RingTheory/RingHom/Finite.lean
theorem finite_isStableUnderBaseChange : IsStableUnderBaseChange @Finite

Proof state:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : (algebraMap R T).Finite
⊢ Module.Finite R T

Tactic:
rw [RingHom.Finite] at h

Result:
R S T : Type u_1
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : CommRing T
inst✝¹ : Algebra R S
inst✝ : Algebra R T
h : Module.Finite R T
⊢ Module.Finite R T
-- Mathlib/Data/Finset/Disjoint.lean
theorem disjoint_coe : Disjoint (s : Set α) t ↔ Disjoint s t

Proof state:
α : Type u_1
s t : Finset α
⊢ Disjoint ↑s ↑t ↔ Disjoint s t

Tactic:
simp only [Finset.disjoint_left, Set.disjoint_left, mem_coe]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Hermitian.lean
theorem isHermitian_submatrix_equiv {A : Matrix n n α} (e : m ≃ n) :
    (A.submatrix e e).IsHermitian ↔ A.IsHermitian :=
  ⟨fun h => by simpa using h.submatrix e.symm, fun h => h.submatrix _⟩

Proof state:
α : Type u_1
m : Type u_3
n : Type u_4
inst✝ : Star α
A : Matrix n n α
e : m ≃ n
h : (A.submatrix ⇑e ⇑e).IsHermitian
⊢ A.IsHermitian

Tactic:
simpa using h.submatrix e.symm

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/LazyList.lean
theorem forall_mem_cons {α} {p : α → Prop} {a : α} {l : Thunk (LazyList α)} :
    (∀ x ∈ @LazyList.cons _ a l, p x) ↔ p a ∧ ∀ x ∈ l.get, p x

Proof state:
α : Type u_1
p : α → Prop
a : α
l : Thunk (LazyList α)
⊢ (∀ (x : α), x ∈ cons a l → p x) ↔ p a ∧ ∀ (x : α), x ∈ l.get → p x

Tactic:
simp only [Membership.mem, LazyList.Mem, or_imp, forall_and, forall_eq]

Result:
no goals
-- Mathlib/RingTheory/RootsOfUnity/Basic.lean
theorem mem_rootsOfUnity_prime_pow_mul_iff' (p k : ℕ) (m : ℕ) [ExpChar R p] {ζ : Rˣ} :
    ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

Proof state:
R : Type u_4
inst✝² : CommRing R
inst✝¹ : IsReduced R
p k m : ℕ
inst✝ : ExpChar R p
ζ : Rˣ
⊢ ζ ^ (p ^ k * m) = 1 ↔ ζ ∈ rootsOfUnity m R

Tactic:
rw [← mem_rootsOfUnity, mem_rootsOfUnity_prime_pow_mul_iff]

Result:
no goals
-- Mathlib/Probability/Independence/Basic.lean
lemma IndepSets_iff (s1 s2 : Set (Set Ω)) (μ : Measure Ω) :
    IndepSets s1 s2 μ ↔ ∀ t1 t2 : Set Ω, t1 ∈ s1 → t2 ∈ s2 → (μ (t1 ∩ t2) = μ t1 * μ t2)

Proof state:
Ω : Type u_1
x✝ : MeasurableSpace Ω
s1 s2 : Set (Set Ω)
μ : Measure Ω
⊢ IndepSets s1 s2 μ ↔ ∀ (t1 t2 : Set Ω), t1 ∈ s1 → t2 ∈ s2 → μ (t1 ∩ t2) = μ t1 * μ t2

Tactic:
simp only [IndepSets, Kernel.IndepSets, ae_dirac_eq, Filter.eventually_pure, Kernel.const_apply]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inl_fst_f (i : ι) :
    (biprod.inl : K ⟶ K ⊞ L).f i ≫ (biprod.fst : K ⊞ L ⟶ K).f i = 𝟙 _

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inl.f i ≫ biprod.fst.f i = 𝟙 (K.X i)

Tactic:
rw [← comp_f, biprod.inl_fst, id_f]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem cos_angle_mul_dist_of_angle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π / 2) :
    Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π / 2
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [angle, ← inner_eq_zero_iff_angle_eq_pi_div_two, real_inner_comm, ← neg_eq_zero, ←
  inner_neg_left, neg_vsub_eq_vsub_rev] at h

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : inner (p₂ -ᵥ p₃) (p₁ -ᵥ p₂) = 0
⊢ Real.cos (∠ p₂ p₃ p₁) * dist p₁ p₃ = dist p₃ p₂

Tactic:
rw [angle, dist_eq_norm_vsub' V p₃ p₂, dist_eq_norm_vsub V p₁ p₃, ← vsub_add_vsub_cancel p₁ p₂ p₃,
  add_comm, cos_angle_add_mul_norm_of_inner_eq_zero h]

Result:
no goals
-- Mathlib/Data/List/ProdSigma.lean
theorem sigma_nil : ∀ l : List α, (l.sigma fun a => @nil (σ a)) = []
  | [] => rfl
  | _ :: l => by simp [sigma_cons, sigma_nil l]

Proof state:
α : Type u_1
σ : α → Type u_3
head✝ : α
l : List α
⊢ ((head✝ :: l).sigma fun a => []) = []

Tactic:
simp [sigma_cons, sigma_nil l]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem isEmpty_alterKey_eq_isEmpty_eraseKey {k : α} {f : Option (β k) → Option (β k)}
    {l : List ((a : α) × β a)} :
    (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValueCast? k l)).isNone)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ (f (getValueCast? k l)).isNone = true

Tactic:
cases f (getValueCast? k l)

Result:
case none
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match none with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ none.isNone = true

case some
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
val✝ : β k
⊢ (match some val✝ with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ (some val✝).isNone = true

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (alterKey k f l).isEmpty = ((eraseKey k l).isEmpty && (f (getValueCast? k l)).isNone)

Tactic:
rw [alterKey, Bool.eq_iff_iff, Bool.and_eq_true_iff]

Result:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match f (getValueCast? k l) with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ (f (getValueCast? k l)).isNone = true

Proof state:
case none
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
⊢ (match none with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ none.isNone = true

case some
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
val✝ : β k
⊢ (match some val✝ with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ (some val✝).isNone = true

Tactic:
repeat simp [isEmpty_insertEntry]

Result:
no goals

Proof state:
case some
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
k : α
f : Option (β k) → Option (β k)
l : List ((a : α) × β a)
val✝ : β k
⊢ (match some val✝ with
        | none => eraseKey k l
        | some v => insertEntry k v l).isEmpty =
      true ↔
    (eraseKey k l).isEmpty = true ∧ (some val✝).isNone = true

Tactic:
simp [isEmpty_insertEntry]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_pure_right : map₂ m f (pure b) = f.map (m · b)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p => m p.1 p.2) ∘ fun a => (a, b)) f = map (fun x => m x b) f

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map₂ m f (pure b) = map (fun x => m x b) f

Tactic:
rw [← map_prod_eq_map₂, prod_pure, map_map]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
f : Filter α
b : β
⊢ map ((fun p => m p.1 p.2) ∘ fun a => (a, b)) f = map (fun x => m x b) f
-- Mathlib/Analysis/Normed/Ring/SeminormFromConst.lean
theorem seminormFromConst_seq_zero (hf : f 0 = 0) : seminormFromConst_seq c f 0 = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
⊢ (fun n => f (0 * c ^ n) / f c ^ n) = 0

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ f (0 * c ^ n) / f c ^ n = 0 n

Proof state:
case h
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
n : ℕ
⊢ f (0 * c ^ n) / f c ^ n = 0 n

Tactic:
rw [zero_mul, hf, zero_div, Pi.zero_apply]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
⊢ seminormFromConst_seq c f 0 = 0

Tactic:
rw [seminormFromConst_seq_def]

Result:
R : Type u_1
inst✝ : CommRing R
c : R
f : RingSeminorm R
hf : f 0 = 0
⊢ (fun n => f (0 * c ^ n) / f c ^ n) = 0