harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_inv_natCast_pow (hx : 0 ≤ x) (hn : n ≠ 0) : (x ^ (n⁻¹ : ℝ)) ^ n = x

Proof state:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
have hn0 : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.2 hn

Result:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Proof state:
x : ℝ
n : ℕ
hx : 0 ≤ x
hn : n ≠ 0
hn0 : ↑n ≠ 0
⊢ (x ^ (↑n)⁻¹) ^ n = x

Tactic:
rw [← rpow_natCast, ← rpow_mul hx, inv_mul_cancel₀ hn0, rpow_one]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_summable (x y : ∀ i, F i) :
    Summable fun i : ι => min ((1 / 2) ^ encode i : ℝ) (dist (x i) (y i))

Proof state:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ 1 / 2

Tactic:
norm_num

Result:
no goals

Proof state:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ (1 / 2) ^ encode i ⊓ dist (x i) (y i)

Tactic:
exact le_min (pow_nonneg (by norm_num) _) dist_nonneg

Result:
no goals

Proof state:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
⊢ Summable fun i => (1 / 2) ^ encode i ⊓ dist (x i) (y i)

Tactic:
refine .of_nonneg_of_le (fun i => ?_) (fun i => min_le_left _ _)
  summable_geometric_two_encode

Result:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
⊢ 0 ≤ (1 / 2) ^ encode i ⊓ dist (x i) (y i)
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem isPiSystem_Iio_rat : IsPiSystem (⋃ a : ℚ, {Iio (a : ℝ)})

Proof state:
case h.e'_2

⊢ ⋃ a, {Iio ↑a} = Iio '' (Rat.cast '' univ)

Tactic:
ext x

Result:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Iio ↑a} ↔ x ∈ Iio '' (Rat.cast '' univ)

Proof state:
case h.e'_2.h
x : Set ℝ
⊢ x ∈ ⋃ a, {Iio ↑a} ↔ x ∈ Iio '' (Rat.cast '' univ)

Tactic:
simp only [iUnion_singleton_eq_range, mem_range, image_univ, mem_image, exists_exists_eq_and]

Result:
no goals

Proof state:
⊢ IsPiSystem (⋃ a, {Iio ↑a})

Tactic:
convert isPiSystem_image_Iio (((↑) : ℚ → ℝ) '' univ)

Result:
case h.e'_2

⊢ ⋃ a, {Iio ↑a} = Iio '' (Rat.cast '' univ)
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.comp_hasFDerivAtFilter {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x) {L'' : Filter E}
    (hh₂ : HasDerivAtFilter h₂ h₂' (f x) L') (hf : HasFDerivAtFilter f f' x L'')
    (hL : Tendsto f L'' L') : HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Proof state:
case h.e'_12.h.e
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
⊢ HSMul.hSMul h₂' = (ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp

Tactic:
ext x

Result:
case h.e'_12.h.e.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x✝¹ : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x✝¹) L'
hf : HasFDerivAtFilter f f' x✝¹ L''
hL : Tendsto f L'' L'
x : E →L[𝕜] 𝕜'
x✝ : E
⊢ (h₂' • x) x✝ = ((ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp x) x✝

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
⊢ HasFDerivAtFilter (h₂ ∘ f) (h₂' • f') x L''

Tactic:
convert (hh₂.restrictScalars 𝕜).comp x hf hL

Result:
case h.e'_12.h.e
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x) L'
hf : HasFDerivAtFilter f f' x L''
hL : Tendsto f L'' L'
⊢ HSMul.hSMul h₂' = (ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp

Proof state:
case h.e'_12.h.e.h.h
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
𝕜' : Type u_1
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
h₂ : 𝕜' → 𝕜'
h₂' : 𝕜'
L' : Filter 𝕜'
f : E → 𝕜'
f' : E →L[𝕜] 𝕜'
x✝¹ : E
L'' : Filter E
hh₂ : HasDerivAtFilter h₂ h₂' (f x✝¹) L'
hf : HasFDerivAtFilter f f' x✝¹ L''
hL : Tendsto f L'' L'
x : E →L[𝕜] 𝕜'
x✝ : E
⊢ (h₂' • x) x✝ = ((ContinuousLinearMap.restrictScalars 𝕜 (smulRight 1 h₂')).comp x) x✝

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem volumePreserving_toMixed_symm :
    MeasurePreserving (toMixed K).symm

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ MeasurePreserving (⇑(toMixed K).symm) volume volume

Tactic:
have : MeasurePreserving (toMixed K).toHomeomorph.toMeasurableEquiv := volumePreserving_toMixed K

Result:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : MeasurePreserving (⇑(toMixed K).toHomeomorph.toMeasurableEquiv) volume volume
⊢ MeasurePreserving (⇑(toMixed K).symm) volume volume

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : MeasurePreserving (⇑(toMixed K).toHomeomorph.toMeasurableEquiv) volume volume
⊢ MeasurePreserving (⇑(toMixed K).symm) volume volume

Tactic:
exact this.symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem le_of_neg_le_neg {a b : Int} (h : -b ≤ -a) : a ≤ b :=
  suffices - -a ≤ - -b by simp [Int.neg_neg] at this; assumption
  Int.neg_le_neg h

Proof state:
a b : Int
h : -b ≤ -a
this : a ≤ b
⊢ a ≤ b

Tactic:
assumption

Result:
no goals

Proof state:
a b : Int
h : -b ≤ -a
this : - -a ≤ - -b
⊢ a ≤ b

Tactic:
simp [Int.neg_neg] at this

Result:
a b : Int
h : -b ≤ -a
this : a ≤ b
⊢ a ≤ b
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem mem_cylinder_iff_dist_le {x y : ∀ n, E n} {n : ℕ} :
    y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
this : (∀ i < n, y i = x i) ↔ n ≤ firstDiff y x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
simpa [dist_eq_of_ne hne]

Result:
no goals

Proof state:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) → n ≤ firstDiff y x

Tactic:
intro hy

Result:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
⊢ n ≤ firstDiff y x

Proof state:
case inl
E : ℕ → Type u_1
y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder y n ↔ dist y y ≤ (1 / 2) ^ n

Tactic:
simp [PiNat.dist_self]

Result:
no goals

Proof state:
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ i < n, y i = x i

Tactic:
intro h i hi

Result:
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff y x
i : ℕ
hi : i < n
⊢ y i = x i

Proof state:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
H : firstDiff y x < n
⊢ False

Tactic:
exact apply_firstDiff_ne hne (hy _ H)

Result:
no goals

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) ↔ n ≤ firstDiff y x

Tactic:
constructor

Result:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) → n ≤ firstDiff y x

case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ n ≤ firstDiff y x → ∀ i < n, y i = x i

Proof state:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
suffices (∀ i : ℕ, i < n → y i = x i) ↔ n ≤ firstDiff y x by simpa [dist_eq_of_ne hne]

Result:
case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ (∀ i < n, y i = x i) ↔ n ≤ firstDiff y x

Proof state:
case inr.mpr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
h : n ≤ firstDiff y x
i : ℕ
hi : i < n
⊢ y i = x i

Tactic:
exact apply_eq_of_lt_firstDiff (hi.trans_le h)

Result:
no goals

Proof state:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
⊢ n ≤ firstDiff y x

Tactic:
by_contra! H

Result:
case inr.mp
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
hy : ∀ i < n, y i = x i
H : firstDiff y x < n
⊢ False

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n

Tactic:
rcases eq_or_ne y x with (rfl | hne)

Result:
case inl
E : ℕ → Type u_1
y : (n : ℕ) → E n
n : ℕ
⊢ y ∈ cylinder y n ↔ dist y y ≤ (1 / 2) ^ n

case inr
E : ℕ → Type u_1
x y : (n : ℕ) → E n
n : ℕ
hne : y ≠ x
⊢ y ∈ cylinder x n ↔ dist y x ≤ (1 / 2) ^ n
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem exists_ball_subset_ball (h : y ∈ ball x ε) : ∃ ε' > 0, ball y ε' ⊆ ball x ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
⊢ 0 < ε - edist y x

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ ∃ ε' > 0, ball y ε' ⊆ ball x ε

Tactic:
refine ⟨ε - edist y x, this, ball_subset ?_ (ne_top_of_lt h)⟩

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ edist y x + (ε - edist y x) ≤ ε

Tactic:
exact (add_tsub_cancel_of_le (mem_ball.mp h).le).le

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
⊢ ∃ ε' > 0, ball y ε' ⊆ ball x ε

Tactic:
have : 0 < ε - edist y x := by simpa using h

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
x y : α
ε : ℝ≥0∞
h : y ∈ ball x ε
this : 0 < ε - edist y x
⊢ ∃ ε' > 0, ball y ε' ⊆ ball x ε
-- Mathlib/Algebra/Algebra/Basic.lean
lemma faithfulSMul_iff_injective_smul_one [Module R A] [IsScalarTower R A A] :
    FaithfulSMul R A ↔ Injective (fun r : R ↦ r • (1 : A))

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r => r • 1) r₁ = (fun r => r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

Tactic:
simp only at hr

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
⊢ FaithfulSMul R A ↔ Injective fun r => r • 1

Tactic:
refine ⟨fun ⟨h⟩ {r₁ r₂} hr ↦ h fun a ↦ ?_, fun h ↦ ⟨fun {r₁ r₂} hr ↦ h ?_⟩⟩

Result:
case refine_1
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : (fun r => r • 1) r₁ = (fun r => r • 1) r₂
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

case refine_2
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
h : Injective fun r => r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r => r • 1) r₁ = (fun r => r • 1) r₂

Proof state:
case refine_2
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
h : Injective fun r => r • 1
r₁ r₂ : R
hr : ∀ (a : A), r₁ • a = r₂ • a
⊢ (fun r => r • 1) r₁ = (fun r => r • 1) r₂

Tactic:
simpa using hr 1

Result:
no goals

Proof state:
case refine_1
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : Semiring A
inst✝¹ : Module R A
inst✝ : IsScalarTower R A A
x✝ : FaithfulSMul R A
r₁ r₂ : R
hr : r₁ • 1 = r₂ • 1
h : ∀ {m₁ m₂ : R}, (∀ (a : A), m₁ • a = m₂ • a) → m₁ = m₂
a : A
⊢ r₁ • a = r₂ • a

Tactic:
rw [← one_mul a, ← smul_mul_assoc, ← smul_mul_assoc, hr]

Result:
no goals
-- Mathlib/CategoryTheory/GradedObject/Monoidal.lean
lemma associator_naturality (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃)
    [HasGoodTensor₁₂Tensor X₁ X₂ X₃] [HasGoodTensorTensor₂₃ X₁ X₂ X₃]
    [HasGoodTensor₁₂Tensor Y₁ Y₂ Y₃] [HasGoodTensorTensor₂₃ Y₁ Y₂ Y₃] :
    tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
      (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Proof state:
I : Type u
inst✝¹⁴ : AddMonoid I
C : Type u_1
inst✝¹³ : Category.{u_2, u_1} C
inst✝¹² : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝¹¹ : X₁.HasTensor X₂
inst✝¹⁰ : (tensorObj X₁ X₂).HasTensor X₃
inst✝⁹ : X₂.HasTensor X₃
inst✝⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝⁷ : Y₁.HasTensor Y₂
inst✝⁶ : (tensorObj Y₁ Y₂).HasTensor Y₃
inst✝⁵ : Y₂.HasTensor Y₃
inst✝⁴ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
inst✝³ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝² : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝¹ : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃
inst✝ : Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃
⊢ tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom =
    (associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)

Tactic:
ext x i₁ i₂ i₃ h : 2

Result:
case h.h
I : Type u
inst✝¹⁴ : AddMonoid I
C : Type u_1
inst✝¹³ : Category.{u_2, u_1} C
inst✝¹² : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝¹¹ : X₁.HasTensor X₂
inst✝¹⁰ : (tensorObj X₁ X₂).HasTensor X₃
inst✝⁹ : X₂.HasTensor X₃
inst✝⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝⁷ : Y₁.HasTensor Y₂
inst✝⁶ : (tensorObj Y₁ Y₂).HasTensor Y₃
inst✝⁵ : Y₂.HasTensor Y₃
inst✝⁴ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
inst✝³ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝² : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝¹ : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃
inst✝ : Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃
x i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = x
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ x h ≫ (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) x =
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ x h ≫ ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)) x

Proof state:
case h.h
I : Type u
inst✝¹⁴ : AddMonoid I
C : Type u_1
inst✝¹³ : Category.{u_2, u_1} C
inst✝¹² : MonoidalCategory C
X₁ X₂ X₃ Y₁ Y₂ Y₃ : GradedObject I C
inst✝¹¹ : X₁.HasTensor X₂
inst✝¹⁰ : (tensorObj X₁ X₂).HasTensor X₃
inst✝⁹ : X₂.HasTensor X₃
inst✝⁸ : X₁.HasTensor (tensorObj X₂ X₃)
inst✝⁷ : Y₁.HasTensor Y₂
inst✝⁶ : (tensorObj Y₁ Y₂).HasTensor Y₃
inst✝⁵ : Y₂.HasTensor Y₃
inst✝⁴ : Y₁.HasTensor (tensorObj Y₂ Y₃)
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
inst✝³ : X₁.HasGoodTensor₁₂Tensor X₂ X₃
inst✝² : X₁.HasGoodTensorTensor₂₃ X₂ X₃
inst✝¹ : Y₁.HasGoodTensor₁₂Tensor Y₂ Y₃
inst✝ : Y₁.HasGoodTensorTensor₂₃ Y₂ Y₃
x i₁ i₂ i₃ : I
h : i₁ + i₂ + i₃ = x
⊢ ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ x h ≫ (tensorHom (tensorHom f₁ f₂) f₃ ≫ (associator Y₁ Y₂ Y₃).hom) x =
    ιTensorObj₃' X₁ X₂ X₃ i₁ i₂ i₃ x h ≫ ((associator X₁ X₂ X₃).hom ≫ tensorHom f₁ (tensorHom f₂ f₃)) x

Tactic:
simp only [categoryOfGradedObjects_comp, ιTensorObj₃'_tensorHom_assoc,
  associator_conjugation, ιTensorObj₃'_associator_hom, assoc, Iso.inv_hom_id_assoc,
  ιTensorObj₃'_associator_hom_assoc, ιTensorObj₃_tensorHom]

Result:
no goals
-- Mathlib/LinearAlgebra/Pi.lean
theorem pi_apply_eq_sum_univ [Fintype ι] (f : (ι → R) →ₗ[R] M₂) (x : ι → R) :
    f x = ∑ i, x i • f fun j => if i = j then 1 else 0

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ f x = ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Tactic:
conv_lhs => rw [pi_eq_sum_univ x, map_sum]

Result:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ ∑ x_1 : ι, f (x x_1 • fun j => if x_1 = j then 1 else 0) = ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
x✝¹ : ι
x✝ : x✝¹ ∈ Finset.univ
⊢ f (x x✝¹ • fun j => if x✝¹ = j then 1 else 0) = x x✝¹ • f fun j => if x✝¹ = j then 1 else 0

Tactic:
rw [map_smul]

Result:
no goals

Proof state:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
⊢ ∑ x_1 : ι, f (x x_1 • fun j => if x_1 = j then 1 else 0) = ∑ i : ι, x i • f fun j => if i = j then 1 else 0

Tactic:
refine Finset.sum_congr rfl (fun _ _ => ?_)

Result:
R : Type u
M₂ : Type w
ι : Type x
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M₂
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : (ι → R) →ₗ[R] M₂
x : ι → R
x✝¹ : ι
x✝ : x✝¹ ∈ Finset.univ
⊢ f (x x✝¹ • fun j => if x✝¹ = j then 1 else 0) = x x✝¹ • f fun j => if x✝¹ = j then 1 else 0
-- Mathlib/Topology/Basic.lean
theorem closure_diff_frontier (s : Set X) : closure s \ frontier s = interior s

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
⊢ closure s \ frontier s = interior s

Tactic:
rw [frontier, diff_diff_right_self, inter_eq_self_of_subset_right interior_subset_closure]

Result:
no goals
-- Mathlib/Data/List/Palindrome.lean
theorem append_reverse (l : List α) : Palindrome (l ++ reverse l)

Proof state:
α : Type u_1
l : List α
⊢ (l ++ l.reverse).Palindrome

Tactic:
apply of_reverse_eq

Result:
case a
α : Type u_1
l : List α
⊢ (l ++ l.reverse).reverse = l ++ l.reverse

Proof state:
case a
α : Type u_1
l : List α
⊢ (l ++ l.reverse).reverse = l ++ l.reverse

Tactic:
rw [reverse_append, reverse_reverse]

Result:
no goals
-- Mathlib/Data/Finset/Pi.lean
@[simp] lemma card_piDiag (s : Finset α) (ι : Type*) [DecidableEq (ι → α)] [Nonempty ι] :
    (s.piDiag ι).card = s.card

Proof state:
α : Type u_1
s : Finset α
ι : Type u_3
inst✝¹ : DecidableEq (ι → α)
inst✝ : Nonempty ι
⊢ #(s.piDiag ι) = #s

Tactic:
rw [piDiag, card_image_of_injective _ const_injective]

Result:
no goals
-- Mathlib/Data/Matroid/Map.lean
lemma map_image_isBase_iff {hf} {B : Set α} (hB : B ⊆ M.E) :
    (M.map f hf).IsBase (f '' B) ↔ M.IsBase B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ M.IsBase B

Tactic:
rw [hf.image_eq_image_iff hB hJ.subset_ground] at hIJ

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
⊢ M.IsBase B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (M.map f hf).IsBase (f '' B) ↔ M.IsBase B

Tactic:
rw [map_isBase_iff]

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
⊢ (∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀) ↔ M.IsBase B

Tactic:
refine ⟨fun ⟨J, hJ, hIJ⟩ ↦ ?_, fun h ↦ ⟨B, h, rfl⟩⟩

Result:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : f '' B = f '' J
⊢ M.IsBase B

Proof state:
α : Type u_1
β : Type u_2
f : α → β
M : Matroid α
hf : InjOn f M.E
B : Set α
hB : B ⊆ M.E
x✝ : ∃ B₀, M.IsBase B₀ ∧ f '' B = f '' B₀
J : Set α
hJ : M.IsBase J
hIJ : B = J
⊢ M.IsBase B

Tactic:
rwa [hIJ]

Result:
no goals
-- Mathlib/Topology/Connected/Basic.lean
theorem connectedComponentIn_nonempty_iff {x : α} {F : Set α} :
    (connectedComponentIn F x).Nonempty ↔ x ∈ F

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (connectedComponentIn F x).Nonempty ↔ x ∈ F

Tactic:
rw [connectedComponentIn]

Result:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F

Proof state:
α : Type u
inst✝ : TopologicalSpace α
x : α
F : Set α
⊢ (if h : x ∈ F then Subtype.val '' connectedComponent ⟨x, h⟩ else ∅).Nonempty ↔ x ∈ F

Tactic:
split_ifs <;> simp [connectedComponent_nonempty, *]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
lemma mk₀_comp (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y) {a : M} (g : ShiftedHom Y Z a) :
    (mk₀ m₀ hm₀ f).comp g (by rw [hm₀, add_zero]) = f ≫ g

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ 0 ⋯ f).comp g ⋯ = f ≫ g

Tactic:
simp [comp, mk₀, shiftFunctorAdd'_add_zero_inv_app, shiftFunctorZero']

Result:
no goals

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.17434, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.17441, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.17448, u_3} E
M : Type u_4
inst✝³ : AddMonoid M
inst✝² : HasShift C M
inst✝¹ : HasShift D M
inst✝ : HasShift E M
X Y Z T : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ a + m₀ = a

Tactic:
rw [hm₀, add_zero]

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
m₀ : M
hm₀ : m₀ = 0
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ m₀ hm₀ f).comp g ⋯ = f ≫ g

Tactic:
subst hm₀

Result:
C : Type u_1
inst✝² : Category.{u_5, u_1} C
M : Type u_4
inst✝¹ : AddMonoid M
inst✝ : HasShift C M
X Y Z : C
f : X ⟶ Y
a : M
g : ShiftedHom Y Z a
⊢ (mk₀ 0 ⋯ f).comp g ⋯ = f ≫ g
-- Mathlib/Order/Ideal.lean
theorem IsProper.not_mem_or_compl_not_mem (hI : IsProper I) : x ∉ I ∨ xᶜ ∉ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
have h : xᶜ ∈ I → x ∉ I := hI.not_mem_of_compl_mem

Result:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I

Proof state:
P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsProper
h : xᶜ ∈ I → x ∉ I
⊢ x ∉ I ∨ xᶜ ∉ I

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Finset/SuccPred.lean
lemma Ioc_sub_one_sub_one_eq_Ico (a b : α) : Ioc (a - 1) (b - 1) = Ico a b

Proof state:
α : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : One α
inst✝³ : LocallyFiniteOrder α
inst✝² : Sub α
inst✝¹ : PredSubOrder α
inst✝ : NoMinOrder α
a b : α
⊢ Ioc (a - 1) (b - 1) = Ico a b

Tactic:
simpa [pred_eq_sub_one] using Ioc_pred_pred_eq_Ico a b

Result:
no goals
-- Mathlib/Data/Int/Interval.lean
theorem card_Ico_of_le (h : a ≤ b) : (#(Ico a b) : ℤ) = b - a

Proof state:
a b : ℤ
h : a ≤ b
⊢ ↑(#(Ico a b)) = b - a

Tactic:
rw [card_Ico, toNat_sub_of_le h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_div {𝕜 : Type*} [RCLike 𝕜] (r : 𝕜) (f : ℝ → 𝕜) :
    ∫ x in a..b, f x / r ∂μ = (∫ x in a..b, f x ∂μ) / r

Proof state:
a b : ℝ
μ : Measure ℝ
𝕜 : Type u_6
inst✝ : RCLike 𝕜
r : 𝕜
f : ℝ → 𝕜
⊢ ∫ (x : ℝ) in a..b, f x / r ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) / r

Tactic:
simpa only [div_eq_mul_inv] using integral_mul_const r⁻¹ f

Result:
no goals