harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
lemma _root_.NumberField.ComplexEmbedding.IsConj.coe_stabilzer_mk
    {φ : K →+* ℂ} (h : ComplexEmbedding.IsConj φ σ) :
    (Stab (mk φ) : Set (K ≃ₐ[k] K)) = {1, σ}

Proof state:
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
⊢ ↑(Stab (mk φ)) = {1, σ}

Tactic:
ext

Result:
case h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : K ≃ₐ[k] K
⊢ x✝ ∈ ↑(Stab (mk φ)) ↔ x✝ ∈ {1, σ}

Proof state:
case h
k : Type u_1
inst✝² : Field k
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra k K
σ : K ≃ₐ[k] K
φ : K →+* ℂ
h : ComplexEmbedding.IsConj φ σ
x✝ : K ≃ₐ[k] K
⊢ x✝ ∈ ↑(Stab (mk φ)) ↔ x✝ ∈ {1, σ}

Tactic:
rw [SetLike.mem_coe, mem_stabilizer_mk_iff, Set.mem_insert_iff, Set.mem_singleton_iff,
  ← h.ext_iff, eq_comm (a := σ)]

Result:
no goals
-- Mathlib/LinearAlgebra/FreeModule/Finite/Matrix.lean
theorem cardinalMk_algHom_le_rank : #(M →ₐ[K] L) ≤ lift.{v} (Module.rank K M)

Proof state:
case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
have := Module.nontrivial K L

Result:
case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Proof state:
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) ≤ lift.{v, u_2} (Module.rank K M)

Tactic:
convert (linearIndependent_algHom_toLinearMap K M L).cardinal_lift_le_rank

Result:
case h.e'_3
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)

case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Proof state:
case h.e'_4
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
this : Nontrivial K
⊢ lift.{v, u_2} (Module.rank K M) = lift.{max u_2 v, max u_2 v} (Module.rank L (M →ₗ[K] L))

Tactic:
rw [lift_id, Module.rank_linearMap_self]

Result:
no goals

Proof state:
case h.e'_3
K : Type u_1
M : Type u_2
L : Type v
inst✝⁷ : CommRing K
inst✝⁶ : Ring M
inst✝⁵ : Algebra K M
inst✝⁴ : Module.Free K M
inst✝³ : Module.Finite K M
inst✝² : CommRing L
inst✝¹ : IsDomain L
inst✝ : Algebra K L
⊢ #(M →ₐ[K] L) = lift.{max u_2 v, max u_2 v} #(M →ₐ[K] L)

Tactic:
rw [lift_id]

Result:
no goals
-- Mathlib/RingTheory/Smooth/StandardSmooth.lean
lemma IsStandardSmooth.trans [IsStandardSmooth.{t, w} R S] [IsStandardSmooth.{t', w'} S T] :
    IsStandardSmooth.{max t t', max w w'} R T where
  out

Proof state:
case mk.intro.mk.intro
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
P : SubmersivePresentation R S
Q : SubmersivePresentation S T
⊢ Nonempty (SubmersivePresentation R T)

Tactic:
exact ⟨Q.comp P⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
⊢ Nonempty (SubmersivePresentation R T)

Tactic:
obtain ⟨⟨P⟩⟩ := ‹IsStandardSmooth R S›

Result:
case mk.intro
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
P : SubmersivePresentation R S
⊢ Nonempty (SubmersivePresentation R T)

Proof state:
case mk.intro
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
P : SubmersivePresentation R S
⊢ Nonempty (SubmersivePresentation R T)

Tactic:
obtain ⟨⟨Q⟩⟩ := ‹IsStandardSmooth S T›

Result:
case mk.intro.mk.intro
R : Type u
S : Type v
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
T : Type u_1
inst✝⁵ : CommRing T
inst✝⁴ : Algebra R T
inst✝³ : Algebra S T
inst✝² : IsScalarTower R S T
inst✝¹ : IsStandardSmooth R S
inst✝ : IsStandardSmooth S T
P : SubmersivePresentation R S
Q : SubmersivePresentation S T
⊢ Nonempty (SubmersivePresentation R T)
-- Mathlib/LinearAlgebra/Basis/Basic.lean
theorem noZeroSMulDivisors [NoZeroDivisors R] (b : Basis ι R M) :
    NoZeroSMulDivisors R M :=
  ⟨fun {c x} hcx => by
    exact or_iff_not_imp_right.mpr fun hx => by
      rw [← b.linearCombination_repr x, ← LinearMap.map_smul,
        ← map_zero (linearCombination R b)] at hcx
      have := b.linearIndependent hcx
      rw [smul_eq_zero] at this
      exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)⟩

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : c • x = 0
⊢ c = 0 ∨ x = 0

Tactic:
exact or_iff_not_imp_right.mpr fun hx => by
  rw [← b.linearCombination_repr x, ← LinearMap.map_smul,
    ← map_zero (linearCombination R b)] at hcx
  have := b.linearIndependent hcx
  rw [smul_eq_zero] at this
  exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
this : c • b.repr x = 0
⊢ c = 0

Tactic:
rw [smul_eq_zero] at this

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
this : c = 0 ∨ b.repr x = 0
⊢ c = 0

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
⊢ c = 0

Tactic:
have := b.linearIndependent hcx

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
this : c • b.repr x = 0
⊢ c = 0

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
this : c = 0 ∨ b.repr x = 0
⊢ c = 0

Tactic:
exact this.resolve_right fun hr => hx (b.repr.map_eq_zero_iff.mp hr)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : c • x = 0
hx : ¬x = 0
⊢ c = 0

Tactic:
rw [← b.linearCombination_repr x, ← LinearMap.map_smul,
  ← map_zero (linearCombination R b)] at hcx

Result:
ι : Type u_1
R : Type u_3
M : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroDivisors R
b : Basis ι R M
c : R
x : M
hcx : (linearCombination R ⇑b) (c • b.repr x) = (linearCombination R ⇑b) 0
hx : ¬x = 0
⊢ c = 0
-- Mathlib/Data/Finset/Update.lean
theorem update_eq_updateFinset {i y} :
    Function.update x i y = updateFinset x {i} (uniqueElim y)

Proof state:
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ update x i y = updateFinset x {i} (uniqueElim y)

Tactic:
congr with j

Result:
case h
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Proof state:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
cases hj

Result:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ update x i y i = updateFinset x {i} (uniqueElim y) i

Proof state:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ update x i y i = updateFinset x {i} (uniqueElim y) i

Tactic:
simp only [dif_pos, Finset.mem_singleton, update_self, updateFinset]

Result:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ y = uniqueElim y ⟨i, ⋯⟩

Proof state:
case h
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
by_cases hj : j = i

Result:
case pos
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Proof state:
case pos.refl
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
⊢ y = uniqueElim y ⟨i, ⋯⟩

Tactic:
exact uniqueElim_default (α := fun j : ({i} : Finset ι) => π j) y

Result:
no goals

Proof state:
case neg
ι : Type u_1
π : ι → Sort u_2
x : (i : ι) → π i
inst✝ : DecidableEq ι
i : ι
y : π i
j : ι
hj : ¬j = i
⊢ update x i y j = updateFinset x {i} (uniqueElim y) j

Tactic:
simp [hj, updateFinset]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma HasFPowerSeriesWithinAt.restrictScalars (hf : HasFPowerSeriesWithinAt f p s x) :
    HasFPowerSeriesWithinAt f (p.restrictScalars 𝕜) s x

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
hf : HasFPowerSeriesWithinAt f p s x
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
rcases hf with ⟨r, hr⟩

Result:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Proof state:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
p : FormalMultilinearSeries 𝕜' E F
x : E
s : Set E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f (FormalMultilinearSeries.restrictScalars 𝕜 p) s x

Tactic:
exact ⟨r, hr.restrictScalars⟩

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem disjoint_filter_filter' (s t : Finset α)
    {p q : α → Prop} [DecidablePred p] [DecidablePred q] (h : Disjoint p q) :
    Disjoint (s.filter p) (t.filter q)

Proof state:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)

Tactic:
rintro a ⟨_, hp⟩ ⟨_, hq⟩

Result:
case intro.intro
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Proof state:
case intro.intro
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
simpa [hp, hq] using h a

Result:
no goals

Proof state:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ Disjoint (filter p s) (filter q t)

Tactic:
simp_rw [disjoint_left, mem_filter]

Result:
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
⊢ ∀ ⦃a : α⦄, a ∈ s ∧ p a → ¬(a ∈ t ∧ q a)

Proof state:
case intro.intro
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : Disjoint p q
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False

Tactic:
rw [Pi.disjoint_iff] at h

Result:
case intro.intro
α : Type u_1
s t : Finset α
p q : α → Prop
inst✝¹ : DecidablePred p
inst✝ : DecidablePred q
h : ∀ (i : α), Disjoint (p i) (q i)
a : α
left✝¹ : a ∈ s
hp : p a
left✝ : a ∈ t
hq : q a
⊢ False
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
lemma singularPart_of_not_haveLebesgueDecomposition (h : ¬ HaveLebesgueDecomposition μ ν) :
    μ.singularPart ν = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
h : ¬μ.HaveLebesgueDecomposition ν
⊢ μ.singularPart ν = 0

Tactic:
rw [singularPart, dif_neg h]

Result:
no goals
-- Mathlib/Algebra/DirectSum/Decomposition.lean
theorem degree_eq_of_mem_mem {x : M} {i j : ι} (hxi : x ∈ ℳ i) (hxj : x ∈ ℳ j) (hx : x ≠ 0) :
    i = j

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ x = 0

Tactic:
rw [← decompose_of_mem_same ℳ hxj, decompose_of_mem_ne ℳ hxi hx]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : x ≠ 0
⊢ i = j

Tactic:
contrapose! hx

Result:
ι : Type u_1
M : Type u_3
σ : Type u_4
inst✝⁴ : DecidableEq ι
inst✝³ : AddCommMonoid M
inst✝² : SetLike σ M
inst✝¹ : AddSubmonoidClass σ M
ℳ : ι → σ
inst✝ : Decomposition ℳ
x : M
i j : ι
hxi : x ∈ ℳ i
hxj : x ∈ ℳ j
hx : i ≠ j
⊢ x = 0
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem tensor_comp {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C}
    (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) :
    tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ tensorHom (f₁ ≫ g₁) (f₂ ≫ g₂) = tensorHom f₁ f₂ ≫ tensorHom g₁ g₂

Tactic:
ext <;> simp

Result:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
      prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) =
    π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)

Proof state:
case hF.h₂.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) = π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F)

Tactic:
simp

Result:
no goals

Proof state:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F = π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F

Tactic:
rw [← Category.assoc]

Result:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F)) ≫ f₂.F = π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F

Proof state:
case hF.h₂
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ (prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F)) ≫ f₂.F = π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F

Tactic:
congr 1

Result:
case hF.h₂.e_a
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) = π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F)

Proof state:
case hF
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Dial C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ π(prod.map π₁ π₁ ≫ π(π₁, prod.map f₁.f (𝟙 Z₁.tgt) ≫ g₁.F) ≫ f₁.F,
      prod.map π₂ π₂ ≫ π(π₁, prod.map f₂.f (𝟙 Z₂.tgt) ≫ g₂.F) ≫ f₂.F) =
    π(π(π₁ ≫ π₁, prod.map (π₁ ≫ f₁.f) π₁ ≫ g₁.F) ≫ f₁.F, π(π₁ ≫ π₂, prod.map (π₂ ≫ f₂.f) π₂ ≫ g₂.F) ≫ f₂.F)

Tactic:
ext <;> simp <;> (rw [← Category.assoc]; congr 1; simp)

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.rotate {u v : V} {c : G.Walk v v} (hc : c.IsTrail) (h : u ∈ c.support) :
    (c.rotate h).IsTrail

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsTrail
h : u ∈ c.support
⊢ (c.rotate h).IsTrail

Tactic:
rw [isTrail_def, (c.rotate_edges h).perm.nodup_iff]

Result:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsTrail
h : u ∈ c.support
⊢ c.edges.Nodup

Proof state:
V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v : V
c : G.Walk v v
hc : c.IsTrail
h : u ∈ c.support
⊢ c.edges.Nodup

Tactic:
exact hc.edges_nodup

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Density.lean
theorem edgeDensity_le_one (s : Finset α) (t : Finset β) : edgeDensity r s t ≤ 1

Proof state:
case h
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ ↑(#(interedges r s t)) ≤ ↑(#s) * ↑(#t)

Tactic:
exact mod_cast card_interedges_le_mul r s t

Result:
no goals

Proof state:
case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)

Tactic:
exact mod_cast Nat.zero_le _

Result:
no goals

Proof state:
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ edgeDensity r s t ≤ 1

Tactic:
apply div_le_one_of_le₀

Result:
case h
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ ↑(#(interedges r s t)) ≤ ↑(#s) * ↑(#t)

case hb
α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
⊢ 0 ≤ ↑(#s) * ↑(#t)
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem measure_le_lintegral_thickenedIndicatorAux (μ : Measure X) {E : Set X}
    (E_mble : MeasurableSet E) (δ : ℝ) : μ E ≤ ∫⁻ x, (thickenedIndicatorAux δ E x : ℝ≥0∞) ∂μ

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E ≤ ∫⁻ (x : X), thickenedIndicatorAux δ E x ∂μ

Tactic:
convert_to lintegral μ (E.indicator fun _ => (1 : ℝ≥0∞)) ≤ lintegral μ (thickenedIndicatorAux δ E)

Result:
case h.e'_3
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = lintegral μ (E.indicator fun x => 1)

X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x => 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Proof state:
case h.e'_3
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = ∫⁻ (a : X) in E, 1 ∂μ

Tactic:
simp only [lintegral_one, Measure.restrict_apply, MeasurableSet.univ, univ_inter]

Result:
no goals

Proof state:
case h.e'_3
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = lintegral μ (E.indicator fun x => 1)

Tactic:
rw [lintegral_indicator E_mble]

Result:
case h.e'_3
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ μ E = ∫⁻ (a : X) in E, 1 ∂μ

Proof state:
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ lintegral μ (E.indicator fun x => 1) ≤ lintegral μ (thickenedIndicatorAux δ E)

Tactic:
apply lintegral_mono

Result:
case hfg
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (E.indicator fun x => 1) ≤ thickenedIndicatorAux δ E

Proof state:
case hfg
X : Type u_1
inst✝¹ : MeasurableSpace X
inst✝ : PseudoEMetricSpace X
μ : Measure X
E : Set X
E_mble : MeasurableSet E
δ : ℝ
⊢ (E.indicator fun x => 1) ≤ thickenedIndicatorAux δ E

Tactic:
apply indicator_le_thickenedIndicatorAux

Result:
no goals