harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/UniqueFactorizationDomain/Multiplicity.lean
theorem emultiplicity_eq_count_normalizedFactors [DecidableEq R] {a b : R} (ha : Irreducible a)
    (hb : b ≠ 0) : emultiplicity a b = (normalizedFactors b).count (normalize a)

Proof state:
case a.h
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b < ↑(count (normalize a) (normalizedFactors b)) + 1

Tactic:
rw [← Nat.cast_one, ← Nat.cast_add, lt_iff_not_ge, ge_iff_le,
  le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Result:
case a.h
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (normalize a) (normalizedFactors b) + 1 ≤ count (normalize a) (normalizedFactors b)

Proof state:
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b = ↑(count (normalize a) (normalizedFactors b))

Tactic:
apply le_antisymm

Result:
case a
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b ≤ ↑(count (normalize a) (normalizedFactors b))

case a
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Proof state:
case a.h
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ¬count (normalize a) (normalizedFactors b) + 1 ≤ count (normalize a) (normalizedFactors b)

Tactic:
simp

Result:
no goals

Proof state:
case a
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b ≤ ↑(count (normalize a) (normalizedFactors b))

Tactic:
apply Order.le_of_lt_add_one

Result:
case a.h
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ emultiplicity a b < ↑(count (normalize a) (normalizedFactors b)) + 1

Proof state:
case a
R : Type u_2
inst✝³ : CancelCommMonoidWithZero R
inst✝² : UniqueFactorizationMonoid R
inst✝¹ : NormalizationMonoid R
inst✝ : DecidableEq R
a b : R
ha : Irreducible a
hb : b ≠ 0
⊢ ↑(count (normalize a) (normalizedFactors b)) ≤ emultiplicity a b

Tactic:
rw [le_emultiplicity_iff_replicate_le_normalizedFactors ha hb, ← le_count_iff_replicate_le]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean
lemma cfcₙHom_nnreal_eq_restrict {a : A} (ha : 0 ≤ a) :
    cfcₙHom ha = (QuasispectrumRestricts.nnreal_of_nonneg ha).nonUnitalStarAlgHom
      (cfcₙHom (IsSelfAdjoint.of_nonneg ha))

Proof state:
A : Type u_1
inst✝¹¹ : TopologicalSpace A
inst✝¹⁰ : NonUnitalRing A
inst✝⁹ : PartialOrder A
inst✝⁸ : StarRing A
inst✝⁷ : StarOrderedRing A
inst✝⁶ : Module ℝ A
inst✝⁵ : IsTopologicalRing A
inst✝⁴ : IsScalarTower ℝ A A
inst✝³ : SMulCommClass ℝ A A
inst✝² : T2Space A
inst✝¹ : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝ : NonnegSpectrumClass ℝ A
a : A
ha : 0 ≤ a
⊢ cfcₙHom ha = QuasispectrumRestricts.nonUnitalStarAlgHom (cfcₙHom ⋯) ⋯

Tactic:
apply (QuasispectrumRestricts.nnreal_of_nonneg ha).cfcₙHom_eq_restrict _
  isUniformEmbedding_subtype_val

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem Right.inv_le_one_iff : a⁻¹ ≤ 1 ↔ 1 ≤ a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ ≤ 1 ↔ 1 ≤ a

Tactic:
rw [← mul_le_mul_iff_right a]

Result:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a

Proof state:
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : MulRightMono α
a : α
⊢ a⁻¹ * a ≤ 1 * a ↔ 1 ≤ a

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem isUnit_fromBlocks_zero₂₁ {A : Matrix m m α} {B : Matrix m n α} {D : Matrix n n α} :
    IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix m m α
B : Matrix m n α
D : Matrix n n α
⊢ IsUnit (fromBlocks A B 0 D) ↔ IsUnit A ∧ IsUnit D

Tactic:
simp only [← nonempty_invertible_iff_isUnit, ← nonempty_prod,
  (fromBlocksZero₂₁InvertibleEquiv _ _ _).nonempty_congr]

Result:
no goals
-- Mathlib/Order/Lattice.lean
lemma inf_eq_and_sup_eq_iff : a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

Proof state:
case refine_2.intro
α : Type u
inst✝ : Lattice α
b : α
⊢ b ⊓ b = b ∧ b ⊔ b = b

Tactic:
exact ⟨inf_idem _, sup_idem _⟩

Result:
no goals

Proof state:
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a ⊓ b = c ∧ a ⊔ b = c ↔ a = c ∧ b = c

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩

Result:
case refine_1
α : Type u
inst✝ : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c

case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c

Proof state:
case refine_2
α : Type u
inst✝ : Lattice α
a b c : α
⊢ a = c ∧ b = c → a ⊓ b = c ∧ a ⊔ b = c

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case refine_2.intro
α : Type u
inst✝ : Lattice α
b : α
⊢ b ⊓ b = b ∧ b ⊔ b = b

Proof state:
case refine_1
α : Type u
inst✝ : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_1
α : Type u
inst✝ : Lattice α
a b c : α
h : a ⊓ b = c ∧ a ⊔ b = c
⊢ a = c ∧ b = c

Tactic:
obtain rfl := sup_eq_inf.1 (h.2.trans h.1.symm)

Result:
case refine_1
α : Type u
inst✝ : Lattice α
a c : α
h : a ⊓ a = c ∧ a ⊔ a = c
⊢ a = c ∧ a = c
-- Mathlib/LinearAlgebra/Dimension/Finite.lean
theorem Module.finite_of_rank_eq_zero [NoZeroSMulDivisors R M]
    (h : Module.rank R M = 0) :
    Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
⊢ Module.Finite R M

Tactic:
nontriviality R

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
a✝ : Nontrivial R
⊢ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Module.rank R M = 0
a✝ : Nontrivial R
⊢ Module.Finite R M

Tactic:
rw [rank_zero_iff] at h

Result:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Subsingleton M
a✝ : Nontrivial R
⊢ Module.Finite R M

Proof state:
R : Type u
M : Type v
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
h : Subsingleton M
a✝ : Nontrivial R
⊢ Module.Finite R M

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[reassoc]
lemma v_comp_XIsoOfEq_inv
    (γ : Cochain F G n) (p q q' : ℤ) (hpq : p + n = q) (hq' : q' = q) :
    γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' (by rw [hq', hpq])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K L : CochainComplex C ℤ
n m : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ p + n = q'

Tactic:
rw [hq', hpq]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q q' : ℤ
hpq : p + n = q
hq' : q' = q
⊢ γ.v p q hpq ≫ (HomologicalComplex.XIsoOfEq G hq').inv = γ.v p q' ⋯

Tactic:
subst hq'

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q' : ℤ
hpq : p + n = q'
⊢ γ.v p q' hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).inv = γ.v p q' ⋯

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
n : ℤ
γ : Cochain F G n
p q' : ℤ
hpq : p + n = q'
⊢ γ.v p q' hpq ≫ (HomologicalComplex.XIsoOfEq G ⋯).inv = γ.v p q' ⋯

Tactic:
simp only [HomologicalComplex.XIsoOfEq, eqToIso_refl, Iso.refl_inv, comp_id]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma fderiv_pullback (f : E → F) (V : F → F) (x : E) (h'f : (fderiv 𝕜 f x).IsInvertible) :
    fderiv 𝕜 f x (pullback 𝕜 f V x) = V (f x)

Proof state:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : ↑M = fderiv 𝕜 f x
⊢ (fderiv 𝕜 f x) (pullback 𝕜 f V x) = V (f x)

Tactic:
simp [pullback_eq_of_fderiv_eq hM, ← hM]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
V : F → F
x : E
h'f : (fderiv 𝕜 f x).IsInvertible
⊢ (fderiv 𝕜 f x) (pullback 𝕜 f V x) = V (f x)

Tactic:
rcases h'f with ⟨M, hM⟩

Result:
case intro
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
V : F → F
x : E
M : E ≃L[𝕜] F
hM : ↑M = fderiv 𝕜 f x
⊢ (fderiv 𝕜 f x) (pullback 𝕜 f V x) = V (f x)
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.mul_dvd (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
H : IsCoprime x y
H1 : x ∣ z
H2 : y ∣ z
⊢ x * y ∣ z

Tactic:
obtain ⟨a, b, h⟩ := H

Result:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z

Proof state:
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)

Tactic:
rw [mul_comm z, mul_assoc]

Result:
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * (x * z)

Proof state:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z

Tactic:
rw [← mul_one z, ← h, mul_add]

Result:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)

Proof state:
case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * y * b

Tactic:
exact (mul_dvd_mul_right H1 _).mul_right _

Result:
no goals

Proof state:
case intro.intro
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x) + z * (b * y)

Tactic:
apply dvd_add

Result:
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (a * x)

case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)

Proof state:
case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * (b * y)

Tactic:
rw [mul_comm b, ← mul_assoc]

Result:
case intro.intro.h₂
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ z * y * b

Proof state:
case intro.intro.h₁
R : Type u
inst✝ : CommSemiring R
x y z : R
H1 : x ∣ z
H2 : y ∣ z
a b : R
h : a * x + b * y = 1
⊢ x * y ∣ a * (x * z)

Tactic:
exact (mul_dvd_mul_left _ H2).mul_left _

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem self_trans_symm : e.trans e.symm ≈ ofSet e.source

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ (e.trans e.symm).source = (ofSet e.source).source

Tactic:
rw [A, ofSet_source]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Tactic:
simp only [hx, mfld_simps]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
refine ⟨by rw [A, ofSet_source], fun x hx => ?_⟩

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ e.trans e.symm ≈ ofSet e.source

Tactic:
have A : (e.trans e.symm).source = e.source := by mfld_set_tac

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
⊢ e.trans e.symm ≈ ofSet e.source

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ (e.trans e.symm).source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Tactic:
rw [A] at hx

Result:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
A : (e.trans e.symm).source = e.source
x : α
hx : x ∈ e.source
⊢ ↑(e.trans e.symm) x = ↑(ofSet e.source) x

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
⊢ (e.trans e.symm).source = e.source

Tactic:
mfld_set_tac

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasDerivAtFilter.sub (hf : HasDerivAtFilter f f' x L) (hg : HasDerivAtFilter g g' x L) :
    HasDerivAtFilter (fun x => f x - g x) (f' - g') x L

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : 𝕜 → F
f' g' : F
x : 𝕜
L : Filter 𝕜
hf : HasDerivAtFilter f f' x L
hg : HasDerivAtFilter g g' x L
⊢ HasDerivAtFilter (fun x => f x - g x) (f' - g') x L

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/Induced.lean
theorem extend_iUnion_nat {f : ℕ → Set α} (hm : ∀ i, P (f i))
    (mU : m (⋃ i, f i) (PU hm) = ∑' i, m (f i) (hm i)) :
    extend m (⋃ i, f i) = ∑' i, extend m (f i) :=
  (extend_eq _ _).trans <|
    mU.trans <| by
      congr with i
      rw [extend_eq]

Proof state:
case e_f.h
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
⊢ m (f i) ⋯ = extend m (f i)

Tactic:
rw [extend_eq]

Result:
no goals

Proof state:
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
⊢ ∑' (i : ℕ), m (f i) ⋯ = ∑' (i : ℕ), extend m (f i)

Tactic:
congr with i

Result:
case e_f.h
α : Type u_1
P : Set α → Prop
m : (s : Set α) → P s → ℝ≥0∞
PU : ∀ ⦃f : ℕ → Set α⦄, (∀ (i : ℕ), P (f i)) → P (⋃ i, f i)
f : ℕ → Set α
hm : ∀ (i : ℕ), P (f i)
mU : m (⋃ i, f i) ⋯ = ∑' (i : ℕ), m (f i) ⋯
i : ℕ
⊢ m (f i) ⋯ = extend m (f i)
-- Mathlib/Order/CompleteLattice.lean
theorem biSup_prod {f : β × γ → α} {s : Set β} {t : Set γ} :
    ⨆ x ∈ s ×ˢ t, f x = ⨆ (a ∈ s) (b ∈ t), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
exact iSup_congr fun _ => iSup_comm

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ x ∈ s ×ˢ t, f x = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)

Tactic:
simp_rw [iSup_prod, mem_prod, iSup_and]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
s : Set β
t : Set γ
⊢ ⨆ i, ⨆ j, ⨆ (_ : i ∈ s), ⨆ (_ : j ∈ t), f (i, j) = ⨆ a ∈ s, ⨆ b ∈ t, f (a, b)
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma comp_units_smul {n₁ n₂ n₁₂ : ℤ} (z₁ : Cochain F G n₁) (k : Rˣ) (z₂ : Cochain G K n₂)
    (h : n₁ + n₂ = n₁₂ ) : z₁.comp (k • z₂) h = k • (z₁.comp z₂ h)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
F G K : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
k : Rˣ
z₂ : Cochain G K n₂
h : n₁ + n₂ = n₁₂
⊢ z₁.comp (k • z₂) h = k • z₁.comp z₂ h

Tactic:
apply Cochain.comp_smul

Result:
no goals
-- Mathlib/Data/Real/Pi/Irrational.lean
/--
Auxiliary for the proof that `π` is irrational.
The integrand in the definition of `I` is nonnegative and takes a positive value at least one point,
so the integral is positive.
-/
private lemma I_pos : 0 < I n (π / 2)

Proof state:
n : ℕ
⊢ Continuous fun x => (1 - x ^ 2) ^ n * cos (x * (π / 2))

Tactic:
continuity

Result:
no goals

Proof state:
n : ℕ
⊢ ∀ x ∈ Ioc (-1) 1, 0 ≤ (1 - x ^ 2) ^ n * cos (x * (π / 2))

Tactic:
refine fun x hx => mul_nonneg (pow_nonneg ?_ _) ?_

Result:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ 1 - x ^ 2

case refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ cos (x * (π / 2))

Proof state:
n : ℕ
⊢ -1 < 1

Tactic:
norm_num

Result:
no goals

Proof state:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ -1 ≤ x ∧ x ≤ 1

Tactic:
exact ⟨hx.1.le, hx.2⟩

Result:
no goals

Proof state:
n : ℕ
⊢ 0 < I n (π / 2)

Tactic:
refine integral_pos (by norm_num) (Continuous.continuousOn (by continuity)) ?_ ⟨0, by simp⟩

Result:
n : ℕ
⊢ ∀ x ∈ Ioc (-1) 1, 0 ≤ (1 - x ^ 2) ^ n * cos (x * (π / 2))

Proof state:
case refine_2
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ cos (x * (π / 2))

Tactic:
refine cos_nonneg_of_neg_pi_div_two_le_of_le ?_ ?_ <;>
nlinarith [hx.1, hx.2, pi_pos]

Result:
no goals

Proof state:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ 0 ≤ 1 - x ^ 2

Tactic:
rw [sub_nonneg, sq_le_one_iff_abs_le_one, abs_le]

Result:
case refine_1
n : ℕ
x : ℝ
hx : x ∈ Ioc (-1) 1
⊢ -1 ≤ x ∧ x ≤ 1

Proof state:
n : ℕ
⊢ 0 ∈ Icc (-1) 1 ∧ 0 < (1 - 0 ^ 2) ^ n * cos (0 * (π / 2))

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_comp_lmapDomain (f : α → α') :
    (linearCombination R v').comp (Finsupp.lmapDomain R R f) = linearCombination R (v' ∘ f)

Proof state:
case h.h
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
a✝ : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1 = (linearCombination R (v' ∘ f) ∘ₗ lsingle a✝) 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
⊢ linearCombination R v' ∘ₗ lmapDomain R R f = linearCombination R (v' ∘ f)

Tactic:
ext

Result:
case h.h
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α → α'
a✝ : α
⊢ ((linearCombination R v' ∘ₗ lmapDomain R R f) ∘ₗ lsingle a✝) 1 = (linearCombination R (v' ∘ f) ∘ₗ lsingle a✝) 1
-- Mathlib/Analysis/Convex/Segment.lean
theorem mem_segment_add_sub [Invertible (2 : 𝕜)] (x y : E) : x ∈ [x + y -[𝕜] x - y]

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x ∈ [x + y-[𝕜]x - y]

Tactic:
convert @midpoint_mem_segment 𝕜 _ _ _ _ _ (x + y) (x - y)

Result:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x + y) (x - y)

Proof state:
case h.e'_5
𝕜 : Type u_1
E : Type u_2
inst✝³ : LinearOrderedRing 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Invertible 2
x y : E
⊢ x = midpoint 𝕜 (x + y) (x - y)

Tactic:
rw [midpoint_add_sub]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Defs.lean
/-- Equality holds when `c ≠ 0`. See `mul_div_mul_right`. -/
lemma le_mul_div_mul_right (h : a / b ≤ 0) : a / b ≤ a * c / (b * c)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a * c / (b * c)

Tactic:
rw [mul_div_mul_right _ _ hc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
⊢ a / b ≤ a * c / (b * c)

Tactic:
obtain rfl | hc := eq_or_ne c 0

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : a / b ≤ 0
⊢ a / b ≤ a * 0 / (b * 0)

case inr
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b c : α
h : a / b ≤ 0
hc : c ≠ 0
⊢ a / b ≤ a * c / (b * c)

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedSemifield α
a b : α
h : a / b ≤ 0
⊢ a / b ≤ a * 0 / (b * 0)

Tactic:
simpa

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma Differentiable.add_iff_left (hg : Differentiable 𝕜 g) :
    Differentiable 𝕜 (fun y => f y + g y) ↔ Differentiable 𝕜 f

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hg : Differentiable 𝕜 g
⊢ (Differentiable 𝕜 fun y => f y + g y) ↔ Differentiable 𝕜 f

Tactic:
refine ⟨fun h ↦ ?_, fun hf ↦ hf.add hg⟩

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hg : Differentiable 𝕜 g
h : Differentiable 𝕜 fun y => f y + g y
⊢ Differentiable 𝕜 f

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
hg : Differentiable 𝕜 g
h : Differentiable 𝕜 fun y => f y + g y
⊢ Differentiable 𝕜 f

Tactic:
simpa only [add_sub_cancel_right] using h.sub hg

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
private lemma Fintype.sum_div_mul_card_choose_card :
    ∑ s : Finset α, (card α / ((card α - #s) * (card α).choose #s) : ℚ) =
      card α * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
have : ∀ {x : ℕ}, ∀ s ∈ powersetCard x (univ : Finset α),
  (card α / ((card α - #s) * (card α).choose #s) : ℚ) =
    card α / ((card α - x) * (card α).choose x) := by
  intros n s hs
  rw [mem_powersetCard_univ.1 hs]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ i ∈ range (#univ + 1), ∑ x ∈ powersetCard i univ, ↑(card α) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1

Tactic:
simp_rw [sum_congr rfl this, sum_const, card_powersetCard, card_univ, nsmul_eq_mul, mul_div,
  mul_comm, ← mul_div]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : Nonempty α
this :
  ∀ {x : ℕ},
    ∀ s ∈ powersetCard x univ,
      ↑(card α) / ((↑(card α) - ↑(#s)) * ↑((card α).choose #s)) = ↑(card α) / ((↑(card α) - ↑x) * ↑((card α).choose x))
⊢ ∑ x ∈ range (card α + 1), ↑(card α) * (↑((card α).choose x) / ((↑(card α) - ↑x) * ↑((card α).choose x))) =
    ↑(card α) * ∑ k ∈ range (card α), (↑k)⁻¹ + 1