harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma equation_add_iff (x₁ x₂ y₁ ℓ : R) : W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔
    (W'.addPolynomial x₁ y₁ ℓ).eval (W'.addX x₁ x₂ ℓ) = 0

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval (C ℓ * (X - C x₁) + C y₁)
          (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))) =
      0

Tactic:
eval_simp

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ W'.Equation (W'.addX x₁ x₂ ℓ) (W'.negAddY x₁ x₂ y₁ ℓ) ↔ eval (W'.addX x₁ x₂ ℓ) (W'.addPolynomial x₁ y₁ ℓ) = 0

Tactic:
rw [Equation, negAddY, addPolynomial, linePolynomial, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Affine R
x₁ x₂ y₁ ℓ : R
⊢ evalEval (W'.addX x₁ x₂ ℓ) (ℓ * (W'.addX x₁ x₂ ℓ - x₁) + y₁)
        (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆)) =
      0 ↔
    eval (W'.addX x₁ x₂ ℓ)
        (eval (C ℓ * (X - C x₁) + C y₁)
          (Y ^ 2 + C (C W'.a₁ * X + C W'.a₃) * Y - C (X ^ 3 + C W'.a₂ * X ^ 2 + C W'.a₄ * X + C W'.a₆))) =
      0
-- Mathlib/NumberTheory/Padics/RingHoms.lean
theorem lift_spec (n : ℕ) : (toZModPow n).comp (lift f_compat) = f n

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
⊢ (toZModPow n).comp (lift f_compat) = f n

Tactic:
ext r

Result:
case a
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ ((toZModPow n).comp (lift f_compat)) r = (f n) r

Proof state:
case a
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}

Tactic:
apply lift_sub_val_mem_span

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ ((toZModPow n).comp (lift f_compat)) r = (f n) r

Tactic:
rw [RingHom.comp_apply, ← ZMod.natCast_zmod_val (f n r), ← map_natCast <| toZModPow n, ←
  sub_eq_zero, ← RingHom.map_sub, ← RingHom.mem_ker, ker_toZModPow]

Result:
case a
R : Type u_1
inst✝ : NonAssocSemiring R
p : ℕ
f : (k : ℕ) → R →+* ZMod (p ^ k)
hp_prime : Fact (Nat.Prime p)
f_compat : ∀ (k1 k2 : ℕ) (hk : k1 ≤ k2), (ZMod.castHom ⋯ (ZMod (p ^ k1))).comp (f k2) = f k1
n : ℕ
r : R
⊢ (lift f_compat) r - ↑((f n) r).val ∈ Ideal.span {↑p ^ n}
-- Mathlib/Algebra/Group/Pointwise/Finset/Basic.lean
@[to_additive]
lemma card_le_card_pow (hn : n ≠ 0) : s.card ≤ (s ^ n).card

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CancelMonoid α
s : Finset α
n : ℕ
hn : n ≠ 0
⊢ #s ≤ #(s ^ n)

Tactic:
simpa using card_pow_mono (s := s) one_ne_zero (Nat.one_le_iff_ne_zero.2 hn)

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem whiskerLeft_hom_inv (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
    f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c : B
f : a ⟶ b
g h : b ⟶ c
η : g ≅ h
⊢ f ◁ η.hom ≫ f ◁ η.inv = 𝟙 (f ≫ g)

Tactic:
rw [← whiskerLeft_comp, hom_inv_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/Data/List/Sublists.lean
theorem sublistsAux_eq_flatMap :
    sublistsAux = fun (a : α) (r : List (List α)) => r.flatMap fun l => [l, a :: l] :=
  funext fun a => funext fun r =>
  List.reverseRecOn r
    (by simp [sublistsAux])
    (fun r l ih => by
      rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]
      simp [sublistsAux])

Proof state:
α : Type u
a : α
r : List (List α)
⊢ sublistsAux a [] = flatMap (fun l => [l, a :: l]) []

Tactic:
simp [sublistsAux]

Result:
no goals

Proof state:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l => [l, a :: l]) r
⊢ foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]

Tactic:
simp [sublistsAux]

Result:
no goals

Proof state:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l => [l, a :: l]) r
⊢ sublistsAux a (r ++ [l]) = flatMap (fun l => [l, a :: l]) (r ++ [l])

Tactic:
rw [flatMap_append, ← ih, flatMap_singleton, sublistsAux, foldl_append]

Result:
α : Type u
a : α
r✝ r : List (List α)
l : List α
ih : sublistsAux a r = flatMap (fun l => [l, a :: l]) r
⊢ foldl (fun r l => r ++ [l, a :: l]) (foldl (fun r l => r ++ [l, a :: l]) [] r) [l] = sublistsAux a r ++ [l, a :: l]
-- Mathlib/LinearAlgebra/AffineSpace/Pointwise.lean
theorem pointwise_vadd_direction (v : V) (s : AffineSubspace k P) :
    (v +ᵥ s).direction = s.direction

Proof state:
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction

Tactic:
exact Submodule.map_id _

Result:
no goals

Proof state:
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ (v +ᵥ s).direction = s.direction

Tactic:
rw [pointwise_vadd_eq_map, map_direction]

Result:
k : Type u_2
V : Type u_3
P : Type u_4
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
v : V
s : AffineSubspace k P
⊢ Submodule.map (↑(AffineEquiv.constVAdd k P v)).linear s.direction = s.direction
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp.lean
theorem iso_isometry_of_normNoninc {V W : SemiNormedGrp} (i : V ≅ W) (h1 : i.hom.hom.NormNoninc)
    (h2 : i.inv.hom.NormNoninc) : Isometry i.hom

Proof state:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
⊢ Isometry ⇑(ConcreteCategory.hom i.hom)

Tactic:
apply AddMonoidHomClass.isometry_of_norm

Result:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
⊢ ∀ (x : V.carrier), ‖(ConcreteCategory.hom i.hom) x‖ = ‖x‖

Proof state:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ ≤ ‖(Hom.hom i.hom) v‖

Tactic:
calc
  ‖v‖ = ‖i.inv (i.hom v)‖ := by rw [← comp_apply, Iso.hom_inv_id, id_apply]
  _ ≤ ‖i.hom v‖ := h2 _

Result:
no goals

Proof state:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
⊢ ∀ (x : V.carrier), ‖(ConcreteCategory.hom i.hom) x‖ = ‖x‖

Tactic:
intro v

Result:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖(ConcreteCategory.hom i.hom) v‖ = ‖v‖

Proof state:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖(ConcreteCategory.hom i.hom) v‖ = ‖v‖

Tactic:
apply le_antisymm (h1 v)

Result:
case a
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ ≤ ‖(Hom.hom i.hom) v‖

Proof state:
V W : SemiNormedGrp
i : V ≅ W
h1 : (Hom.hom i.hom).NormNoninc
h2 : (Hom.hom i.inv).NormNoninc
v : V.carrier
⊢ ‖v‖ = ‖(ConcreteCategory.hom i.inv) ((ConcreteCategory.hom i.hom) v)‖

Tactic:
rw [← comp_apply, Iso.hom_inv_id, id_apply]

Result:
no goals
-- Mathlib/Data/PNat/Find.lean
theorem find_eq_one : PNat.find h = 1 ↔ p 1

Proof state:
p : ℕ+ → Prop
inst✝ : DecidablePred p
h : ∃ n, p n
⊢ PNat.find h = 1 ↔ p 1

Tactic:
simp [find_eq_iff]

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma mem_corner_iff_mem_range_mul_left (hc : IsMulCentral e) {r : R} :
    r ∈ corner e ↔ r ∈ Set.range (e * ·)

Proof state:
R : Type u_1
e : R
inst✝ : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
⊢ r ∈ corner e ↔ r ∈ Set.range fun x => e * x

Tactic:
simp_rw [corner, mem_mk, Set.mem_range, ← hc.comm, ← mul_assoc, idem.eq]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIcoDiv_sub_zsmul' (a b : α) (m : ℤ) :
    toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIcoDiv hp (a - m • p) b = toIcoDiv hp a b + m

Tactic:
rw [sub_eq_add_neg, ← neg_smul, toIcoDiv_add_zsmul', sub_neg_eq_add]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_false_or_eq_true : (b : Bool) → b = true ∨ b = false

Proof state:
⊢ ∀ (b : Bool), b = true ∨ b = false

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp]
lemma reflect_one (n : ℕ) : (1 : R[X]).reflect n = Polynomial.X ^ n

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
⊢ reflect n 1 = X ^ n

Tactic:
rw [← C.map_one, reflect_C, map_one, one_mul]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma intCast_cast_neg (x : ZMod n) : (cast (-x) : ℤ) = -cast x % n

Proof state:
n : ℕ
x : ZMod n
⊢ (-x).cast = -x.cast % ↑n

Tactic:
rw [← ZMod.coe_intCast, Int.cast_neg, ZMod.intCast_zmod_cast]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem finrank_vectorSpan_insert_le_set (s : Set P) (p : P) :
    finrank k (vectorSpan k (insert p s)) ≤ finrank k (vectorSpan k s) + 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k ↥(affineSpan k s).direction ≤ finrank k ↥(vectorSpan k s)

Tactic:
rw [direction_affineSpan]

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k ↥(vectorSpan k (insert p s)) ≤ finrank k ↥(vectorSpan k s) + 1

Tactic:
rw [← direction_affineSpan, ← affineSpan_insert_affineSpan, direction_affineSpan]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k ↥(vectorSpan k (insert p ↑(affineSpan k s))) ≤ finrank k ↥(vectorSpan k s) + 1

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k ↥(vectorSpan k (insert p ↑(affineSpan k s))) ≤ finrank k ↥(vectorSpan k s) + 1

Tactic:
refine (finrank_vectorSpan_insert_le _ _).trans (add_le_add_right ?_ _)

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
p : P
⊢ finrank k ↥(affineSpan k s).direction ≤ finrank k ↥(vectorSpan k s)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapIdx_append {K L : Array α} :
    (K ++ L).mapIdx f = K.mapIdx f ++ L.mapIdx fun i => f (i + K.size)

Proof state:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : List α
⊢ mapIdx f ({ toList := K } ++ { toList := L }) =
    mapIdx f { toList := K } ++ mapIdx (fun i => f (i + { toList := K }.size)) { toList := L }

Tactic:
simp [List.mapIdx_append]

Result:
no goals

Proof state:
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : Array α
⊢ mapIdx f (K ++ L) = mapIdx f K ++ mapIdx (fun i => f (i + K.size)) L

Tactic:
rcases K with ⟨K⟩

Result:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
L : Array α
K : List α
⊢ mapIdx f ({ toList := K } ++ L) = mapIdx f { toList := K } ++ mapIdx (fun i => f (i + { toList := K }.size)) L

Proof state:
case mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
L : Array α
K : List α
⊢ mapIdx f ({ toList := K } ++ L) = mapIdx f { toList := K } ++ mapIdx (fun i => f (i + { toList := K }.size)) L

Tactic:
rcases L with ⟨L⟩

Result:
case mk.mk
α : Type u_1
α✝ : Type u_2
f : Nat → α → α✝
K L : List α
⊢ mapIdx f ({ toList := K } ++ { toList := L }) =
    mapIdx f { toList := K } ++ mapIdx (fun i => f (i + { toList := K }.size)) { toList := L }
-- Mathlib/MeasureTheory/Measure/DiracProba.lean
/-- The assignment `x ↦ diracProba x` is continuous `X → ProbabilityMeasure X`. -/
lemma continuous_diracProba : Continuous (fun (x : X) ↦ diracProba x)

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ Continuous fun x => diracProba x

Tactic:
rw [continuous_iff_continuousAt]

Result:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ ∀ (x : X), ContinuousAt (fun x => diracProba x) x

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable fun X_1 => ↑(f X_1)
⊢ Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))

Tactic:
simp only [diracProba, ProbabilityMeasure.coe_mk, lintegral_dirac' _ f_mble]

Result:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable fun X_1 => ↑(f X_1)
⊢ Tendsto (fun i => ↑(f i)) (𝓝 x) (𝓝 ↑(f x))

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
⊢ ∀ (x : X), ContinuousAt (fun x => diracProba x) x

Tactic:
apply fun x ↦ ProbabilityMeasure.tendsto_iff_forall_lintegral_tendsto.mpr fun f ↦ ?_

Result:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
⊢ Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable fun X_1 => ↑(f X_1)
⊢ Tendsto (fun i => ↑(f i)) (𝓝 x) (𝓝 ↑(f x))

Tactic:
exact (ENNReal.continuous_coe.comp f.continuous).continuousAt

Result:
no goals

Proof state:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
⊢ Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))

Tactic:
have f_mble : Measurable (fun X ↦ (f X : ℝ≥0∞)) :=
  measurable_coe_nnreal_ennreal_iff.mpr f.continuous.measurable

Result:
X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
inst✝ : OpensMeasurableSpace X
x : X
f : X →ᵇ ℝ≥0
f_mble : Measurable fun X_1 => ↑(f X_1)
⊢ Tendsto (fun i => ∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba i)) (𝓝 x) (𝓝 (∫⁻ (ω : X), ↑(f ω) ∂↑(diracProba x)))
-- Mathlib/Data/Set/Pointwise/SMul.lean
theorem smul_zero_subset (s : Set α) : s • (0 : Set β) ⊆ 0

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : Zero β
inst✝ : SMulZeroClass α β
s : Set α
⊢ s • 0 ⊆ 0

Tactic:
simp [subset_def, mem_smul]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
lemma sup_iInf_eq (a : α) (f : ι → α) : (a ⊔ ⨅ i, f i) = ⨅ i, a ⊔ f i

Proof state:
α : Type u
ι : Sort w
minAx : MinimalAxioms α
a : α
f : ι → α
⊢ a ⊔ ⨅ i, f i = ⨅ i, a ⊔ f i

Tactic:
simpa only [sup_comm] using minAx.iInf_sup_eq f a

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal'_smul {R : Type*} [Semiring R] [AddCommMonoid α] [Module R α] (x : R)
    (M : ∀ i, Matrix (m' i) (n' i) α) : blockDiagonal' (x • M) = x • blockDiagonal' M

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ j✝ = (x • blockDiagonal' M) i✝ j✝

Tactic:
simp only [blockDiagonal'_apply, Pi.smul_apply, smul_apply]

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    x • if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0

Proof state:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ (if h : i✝.fst = j✝.fst then x • M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0) =
    x • if h : i✝.fst = j✝.fst then M i✝.fst i✝.snd (cast ⋯ j✝.snd) else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
⊢ blockDiagonal' (x • M) = x • blockDiagonal' M

Tactic:
ext

Result:
case a
o : Type u_4
m' : o → Type u_7
n' : o → Type u_8
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Semiring R
inst✝¹ : AddCommMonoid α
inst✝ : Module R α
x : R
M : (i : o) → Matrix (m' i) (n' i) α
i✝ : (i : o) × m' i
j✝ : (i : o) × n' i
⊢ blockDiagonal' (x • M) i✝ j✝ = (x • blockDiagonal' M) i✝ j✝
-- Mathlib/CategoryTheory/Shift/ShiftedHom.lean
@[simp]
lemma mk₀_comp_mk₀_assoc (f : X ⟶ Y) (g : Y ⟶ Z) {a : M}
    (ha : a = 0) {d : M} (h : ShiftedHom Z T d) :
    (mk₀ a ha f).comp ((mk₀ a ha g).comp h
        (show _ = d by rw [ha, add_zero])) (show _ = d by rw [ha, add_zero]) =
      (mk₀ a ha (f ≫ g)).comp h (by rw [ha, add_zero])

Proof state:
case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ d + 0 + 0 = d

Tactic:
simp

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 T : C
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
⊢ (mk₀ a ha f).comp ((mk₀ a ha g).comp h ⋯) ⋯ = (mk₀ a ha (f ≫ g)).comp h ⋯

Tactic:
subst ha

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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ (mk₀ 0 ⋯ f).comp ((mk₀ 0 ⋯ g).comp h ⋯) ⋯ = (mk₀ 0 ⋯ (f ≫ g)).comp h ⋯

Proof state:
C : Type u_1
inst✝⁶ : Category.{?u.29535, u_1} C
D : Type u_2
inst✝⁵ : Category.{?u.29542, u_2} D
E : Type u_3
inst✝⁴ : Category.{?u.29549, 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
f : X ⟶ Y
g : Y ⟶ Z
a : M
ha : a = 0
d : M
h : ShiftedHom Z T d
⊢ d + a = d

Tactic:
rw [ha, add_zero]

Result:
no goals

Proof state:
case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ 0 + 0 = 0

case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ d + 0 + 0 = d

Tactic:
all_goals simp

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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ (mk₀ 0 ⋯ f).comp ((mk₀ 0 ⋯ g).comp h ⋯) ⋯ = (mk₀ 0 ⋯ (f ≫ g)).comp h ⋯

Tactic:
rw [← comp_assoc, mk₀_comp_mk₀]

Result:
case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ 0 + 0 = 0

case h
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 T : C
f : X ⟶ Y
g : Y ⟶ Z
d : M
h : ShiftedHom Z T d
⊢ d + 0 + 0 = d
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem mem_support_cycle_of_cycle {g d c : Perm α}
    (hc : c ∈ g.cycleFactorsFinset) (hd : d ∈ g.cycleFactorsFinset) :
    ∀ x : α, x ∈ c.support ↔ d x ∈ c.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ c x = x ↔ c (d x) = d x

Tactic:
by_cases h : c = d

Result:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x

Proof state:
case neg
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : ¬c = d
⊢ c x = x ↔ c (d x) = d x

Tactic:
rw [← Perm.mul_apply,
  Commute.eq (cycleFactorsFinset_mem_commute g hc hd h),
  mul_apply, EmbeddingLike.apply_eq_iff_eq]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
⊢ ∀ (x : α), x ∈ c.support ↔ d x ∈ c.support

Tactic:
intro x

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ x ∈ c.support ↔ d x ∈ c.support

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ x ∈ c.support ↔ d x ∈ c.support

Tactic:
simp only [mem_support, not_iff_not]

Result:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
⊢ c x = x ↔ c (d x) = d x

Proof state:
case pos
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g d c : Perm α
hc : c ∈ g.cycleFactorsFinset
hd : d ∈ g.cycleFactorsFinset
x : α
h : c = d
⊢ c x = x ↔ c (d x) = d x

Tactic:
rw [← h, EmbeddingLike.apply_eq_iff_eq]

Result:
no goals