harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
/-- The **Ahlswede-Zhang Identity**. -/
lemma infSum_eq_one (h𝒜₁ : 𝒜.Nonempty) (h𝒜₀ : ∅ ∉ 𝒜) : infSum 𝒜 = 1

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ infSum 𝒜 = 1

Tactic:
rw [← compls_compls 𝒜, eq_sub_of_add_eq (infSum_compls_add_supSum _),
  supSum_of_not_univ_mem h𝒜₁.compls, add_sub_cancel_left]

Result:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ univ ∉ 𝒜ᶜˢ

Proof state:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
𝒜 : Finset (Finset α)
inst✝ : Nonempty α
h𝒜₁ : 𝒜.Nonempty
h𝒜₀ : ∅ ∉ 𝒜
⊢ univ ∉ 𝒜ᶜˢ

Tactic:
simpa

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem IsOpen.mul_closure (hs : IsOpen s) (t : Set G) : s * closure t = s * t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
⊢ a * b ∈ s * t

Tactic:
obtain ⟨_, ⟨c, hc, d, rfl : d = _, rfl⟩, hcs⟩ := hb _ hs.inv.mul_right hbU

Result:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
c : G
hc : c ∈ s⁻¹
hcs : (fun x1 x2 => x1 * x2) c (a * b) ∈ t
⊢ a * b ∈ s * t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : b ∈ closure t
⊢ a * b ∈ s * t

Tactic:
rw [mem_closure_iff] at hb

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
⊢ a * b ∈ s * t

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
⊢ a * b ∈ s * t

Tactic:
have hbU : b ∈ s⁻¹ * {a * b} := ⟨a⁻¹, Set.inv_mem_inv.2 ha, a * b, rfl, inv_mul_cancel_left _ _⟩

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
⊢ a * b ∈ s * t

Proof state:
case intro.intro.intro.intro.intro.intro
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : ∀ (o : Set G), IsOpen o → b ∈ o → (o ∩ t).Nonempty
hbU : b ∈ s⁻¹ * {a * b}
c : G
hc : c ∈ s⁻¹
hcs : (fun x1 x2 => x1 * x2) c (a * b) ∈ t
⊢ a * b ∈ s * t

Tactic:
exact ⟨c⁻¹, hc, _, hcs, inv_mul_cancel_left _ _⟩

Result:
no goals

Proof state:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
⊢ s * closure t = s * t

Tactic:
refine (mul_subset_iff.2 fun a ha b hb => ?_).antisymm (mul_subset_mul_left subset_closure)

Result:
G : Type w
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
s : Set G
hs : IsOpen s
t : Set G
a : G
ha : a ∈ s
b : G
hb : b ∈ closure t
⊢ a * b ∈ s * t
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
lemma ciSup_image {α ι ι' : Type*} [ConditionallyCompleteLattice α] [Nonempty ι] [Nonempty ι']
    {s : Set ι} (hs : s.Nonempty) {f : ι → ι'} {g : ι' → α}
    (hf : BddAbove (Set.range fun i : s ↦ g (f i))) (hg' : sSup ∅ ≤ ⨆ i : s, g (f i)) :
    ⨆ i ∈ (f '' s), g i = ⨆ x ∈ s, g (f x)

Proof state:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ g ↑t ≤ ⨆ i, g ↑i

Tactic:
refine le_ciSup_set ?_ t.prop

Result:
case intro
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
t : ↑(f '' s)
ht : g ↑t = g (f ↑⟨i, h⟩)
⊢ BddAbove (g '' (f '' s))

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
i : ι
h : i ∈ s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
have : f i ∈ f '' s := Set.mem_image_of_mem _ h

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
⊢ ⨆ i, g (f ↑i) ≤ ⨆ i, g ↑i

Tactic:
refine ciSup_le ?_

Result:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this : Nonempty ↑s
⊢ ∀ (x : ↑s), g (f ↑x) ≤ ⨆ i, g ↑i

Proof state:
α : Type u_5
ι : Type u_6
ι' : Type u_7
inst✝² : ConditionallyCompleteLattice α
inst✝¹ : Nonempty ι
inst✝ : Nonempty ι'
s : Set ι
hs : s.Nonempty
f : ι → ι'
g : ι' → α
hf : BddAbove (range fun i => g (f ↑i))
hg' : sSup ∅ ≤ ⨆ i, g (f ↑i)
hg : BddAbove (range fun i => g ↑i)
this✝ : Nonempty ↑s
i : ι
h : i ∈ s
this : f i ∈ f '' s
⊢ ∃ t, g ↑t = g (f ↑⟨i, h⟩)

Tactic:
exact ⟨⟨f i, this⟩, by simp [this]⟩

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Chain.lean
@[simp] lemma coe_chainTop : (chainTop α β : L → R) = (chainTopCoeff α β : ℤ) • α + β

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ ⇑(chainTop α β) = chainTopCoeff α β • α + ⇑β

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ ⇑(chainTop α β) = ↑(chainTopCoeff α β) • α + ⇑β

Tactic:
rw [Nat.cast_smul_eq_nsmul ℤ]

Result:
R : Type u_1
L : Type u_2
inst✝¹⁰ : CommRing R
inst✝⁹ : LieRing L
inst✝⁸ : LieAlgebra R L
M : Type u_3
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : LieRingModule L M
inst✝⁴ : LieModule R L M
inst✝³ : LieRing.IsNilpotent L
inst✝² : NoZeroSMulDivisors ℤ R
inst✝¹ : NoZeroSMulDivisors R M
inst✝ : IsNoetherian R M
α : L → R
β : Weight R L M
⊢ ⇑(chainTop α β) = chainTopCoeff α β • α + ⇑β
-- Mathlib/RingTheory/RingHom/Finite.lean
theorem finite_stableUnderComposition : StableUnderComposition @Finite

Proof state:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Finite
hg : g.Finite
⊢ (g.comp f).Finite

Tactic:
exact hg.comp hf

Result:
no goals

Proof state:
⊢ StableUnderComposition @Finite

Tactic:
introv R hf hg

Result:
R S T : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
hf : f.Finite
hg : g.Finite
⊢ (g.comp f).Finite
-- Mathlib/Algebra/Module/Basic.lean
lemma indicator_smul_apply (s : Set α) (r : α → R) (f : α → M) (a : α) :
    indicator s (fun a ↦ r a • f a) a = r a • indicator s f a

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ s.indicator (fun a => r a • f a) a = r a • s.indicator f a

Tactic:
dsimp only [indicator]

Result:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0

Proof state:
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
⊢ (if a ∈ s then r a • f a else 0) = r a • if a ∈ s then f a else 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∉ s
⊢ 0 = r a • 0

Proof state:
case pos
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∈ s
⊢ r a • f a = r a • f a

case neg
α : Type u_1
R : Type u_2
M : Type u_3
inst✝¹ : Zero M
inst✝ : SMulZeroClass R M
s : Set α
r : α → R
f : α → M
a : α
h✝ : a ∉ s
⊢ 0 = r a • 0

Tactic:
exacts [rfl, (smul_zero (r a)).symm]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma RightFractionRel.op {X Y : C} {z₁ z₂ : W.RightFraction X Y}
    (h : RightFractionRel z₁ z₂) : LeftFractionRel z₁.op z₂.op

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
Z : C
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.op z₂.op

Tactic:
exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
  Quiver.Hom.unop_inj hf, ht⟩

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
h : RightFractionRel z₁ z₂
⊢ LeftFractionRel z₁.op z₂.op

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.RightFraction X Y
Z : C
t₁ : Z ⟶ z₁.X'
t₂ : Z ⟶ z₂.X'
hs : t₁ ≫ z₁.s = t₂ ≫ z₂.s
hf : t₁ ≫ z₁.f = t₂ ≫ z₂.f
ht : W (t₁ ≫ z₁.s)
⊢ LeftFractionRel z₁.op z₂.op
-- Mathlib/AlgebraicGeometry/Morphisms/SurjectiveOnStalks.lean
lemma Spec_iff {R S : CommRingCat.{u}} {φ : R ⟶ S} :
    SurjectiveOnStalks (Spec.map φ) ↔ RingHom.SurjectiveOnStalks φ.hom

Proof state:
R S : CommRingCat
φ : R ⟶ S
⊢ SurjectiveOnStalks (Spec.map φ) ↔ (CommRingCat.Hom.hom φ).SurjectiveOnStalks

Tactic:
rw [eq_stalkwise, stalkwise_Spec_map_iff RingHom.surjective_respectsIso,
  RingHom.SurjectiveOnStalks]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem List.trop_minimum [LinearOrder R] (l : List R) :
    trop l.minimum = List.sum (l.map (trop ∘ WithTop.some))

Proof state:
case cons
R : Type u_1
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum
⊢ trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum

Tactic:
simp [List.minimum_cons, ← IH]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : LinearOrder R
l : List R
⊢ trop l.minimum = (map (trop ∘ WithTop.some) l).sum

Tactic:
induction' l with hd tl IH

Result:
case nil
R : Type u_1
inst✝ : LinearOrder R
⊢ trop [].minimum = (map (trop ∘ WithTop.some) []).sum

case cons
R : Type u_1
inst✝ : LinearOrder R
hd : R
tl : List R
IH : trop tl.minimum = (map (trop ∘ WithTop.some) tl).sum
⊢ trop (hd :: tl).minimum = (map (trop ∘ WithTop.some) (hd :: tl)).sum

Proof state:
case nil
R : Type u_1
inst✝ : LinearOrder R
⊢ trop [].minimum = (map (trop ∘ WithTop.some) []).sum

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/AlgebraicIndependent/TranscendenceBasis.lean
theorem exists_isTranscendenceBasis (h : Injective (algebraMap R A)) :
    ∃ s : Set A, IsTranscendenceBasis R ((↑) : s → A)

Proof state:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hst : s ≤ t
⊢ s = t

Tactic:
exact hs.2.eq_of_le ⟨ht, subset_univ _⟩ hst

Result:
no goals

Proof state:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
⊢ ∃ s, IsTranscendenceBasis R Subtype.val

Tactic:
refine ⟨s, hs.2.1.1, fun t ht hst ↦ ?_⟩

Result:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hst : range Subtype.val ≤ t
⊢ range Subtype.val = t

Proof state:
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
⊢ ∃ s, IsTranscendenceBasis R Subtype.val

Tactic:
obtain ⟨s, hs⟩ := exists_maximal_algebraicIndependent (∅ : Set A) Set.univ (Set.subset_univ _)
    ((algebraicIndependent_empty_iff R A).2 h)

Result:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
⊢ ∃ s, IsTranscendenceBasis R Subtype.val

Proof state:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hst : range Subtype.val ≤ t
⊢ range Subtype.val = t

Tactic:
simp only [Subtype.range_coe_subtype, setOf_mem_eq] at *

Result:
case intro
R : Type u_3
A : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
h : Injective ⇑(algebraMap R A)
s : Set A
hs : ∅ ⊆ s ∧ Maximal (fun x => AlgebraicIndependent R Subtype.val ∧ x ⊆ univ) s
t : Set A
ht : AlgebraicIndependent R Subtype.val
hst : s ≤ t
⊢ s = t
-- Mathlib/Data/Matrix/Mul.lean
theorem mul_add [Fintype n] (L : Matrix m n α) (M N : Matrix n o α) :
    L * (M + N) = L * M + L * N

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
⊢ L * (M + N) = L * M + L * N

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
j✝ : o
⊢ (L * (M + N)) i✝ j✝ = (L * M + L * N) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type v
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n
L : Matrix m n α
M N : Matrix n o α
i✝ : m
j✝ : o
⊢ (L * (M + N)) i✝ j✝ = (L * M + L * N) i✝ j✝

Tactic:
apply dotProduct_add

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem existsUnique (h : IsUniversal f) (g : CostructuredArrow S T) :
    ∃! η : g.left ⟶ f.left, S.map η ≫ f.hom = g.hom :=
  ⟨h.lift g, h.fac g, fun f w ↦ h.hom_ext <| by simp [w]⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
T : D
S : C ⥤ D
f✝ : CostructuredArrow S T
h : f✝.IsUniversal
g : CostructuredArrow S T
f : g.left ⟶ f✝.left
w : (fun η => S.map η ≫ f✝.hom = g.hom) f
⊢ S.map f ≫ f✝.hom = S.map (h.lift g) ≫ f✝.hom

Tactic:
simp [w]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsert_snd_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} {b : β a} :
    (m.val.containsThenInsert a b).2 = (m.containsThenInsert a b).2.1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
b : β a
⊢ (m.val.containsThenInsert a b).snd = (m.containsThenInsert a b).snd.val

Tactic:
simp [Raw.containsThenInsert, m.2]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem constant_factor_ne_zero {R} [CommRing R] {K : Type*} [Field K] [Algebra R K]
    [IsFractionRing R K] {I : FractionalIdeal R⁰ K} (hI : I ≠ 0) {a : R} {J : Ideal R}
    (haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J) :
    (Ideal.span {a} : Ideal R) ≠ 0 := fun h ↦ by
  rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h
  rw [h, RingHom.map_zero, inv_zero, spanSingleton_zero, MulZeroClass.zero_mul] at haJ
  exact hI haJ

Proof state:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : a = 0
⊢ False

Tactic:
exact hI haJ

Result:
no goals

Proof state:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : Ideal.span {a} = 0
⊢ False

Tactic:
rw [Ideal.zero_eq_bot, Ideal.span_singleton_eq_bot] at h

Result:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : a = 0
⊢ False

Proof state:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = spanSingleton R⁰ ((algebraMap R K) a)⁻¹ * ↑J
h : a = 0
⊢ False

Tactic:
rw [h, RingHom.map_zero, inv_zero, spanSingleton_zero, MulZeroClass.zero_mul] at haJ

Result:
R : Type u_6
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : FractionalIdeal R⁰ K
hI : I ≠ 0
a : R
J : Ideal R
haJ : I = 0
h : a = 0
⊢ False
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem getKey?_eq_some_getKey! [EquivBEq α] [LawfulHashable α] [Inhabited α] {a : α} :
    a ∈ m → m.getKey? a = some (m.getKey! a)

Proof state:
α : Type u
β : α → Type v
x✝¹ : BEq α
x✝ : Hashable α
m : DHashMap α β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
a : α
⊢ a ∈ m → m.getKey? a = some (m.getKey! a)

Tactic:
simpa [mem_iff_contains] using getKey?_eq_some_getKey!_of_contains

Result:
no goals
-- Mathlib/Tactic/Ring/Basic.lean
theorem mul_add {d : R} (_ : (a : R) * b₁ = c₁) (_ : a * b₂ = c₂) (_ : c₁ + 0 + c₂ = d) :
    a * (b₁ + b₂) = d

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ c₁ c₂ d : R
x✝² : a * b₁ = c₁
x✝¹ : a * b₂ = c₂
x✝ : c₁ + 0 + c₂ = d
⊢ a * (b₁ + b₂) = d

Tactic:
subst_vars

Result:
R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂

Proof state:
R : Type u_1
inst✝ : CommSemiring R
a b₁ b₂ : R
⊢ a * (b₁ + b₂) = a * b₁ + 0 + a * b₂

Tactic:
simp [_root_.mul_add]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem IsBoundedUnder.sup [SemilatticeSup α] {f : Filter β} {u v : β → α} :
    f.IsBoundedUnder (· ≤ ·) u →
      f.IsBoundedUnder (· ≤ ·) v → f.IsBoundedUnder (· ≤ ·) fun a => u a ⊔ v a
  | ⟨bu, (hu : ∀ᶠ x in f, u x ≤ bu)⟩, ⟨bv, (hv : ∀ᶠ x in f, v x ≤ bv)⟩ =>
    ⟨bu ⊔ bv, show ∀ᶠ x in f, u x ⊔ v x ≤ bu ⊔ bv
      by filter_upwards [hu, hv] with _ using sup_le_sup⟩

Proof state:
α : Type u_1
β : Type u_2
inst✝ : SemilatticeSup α
f : Filter β
u v : β → α
bu : α
hu : ∀ᶠ (x : β) in f, u x ≤ bu
bv : α
hv : ∀ᶠ (x : β) in f, v x ≤ bv
⊢ ∀ᶠ (x : β) in f, u x ⊔ v x ≤ bu ⊔ bv

Tactic:
filter_upwards [hu, hv] with _ using sup_le_sup

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma indicator_mul_right (s : Set ι) (f g : ι → M₀) :
    indicator s (fun j ↦ f j * g j) i = f i * indicator s g i

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0

Tactic:
split_ifs

Result:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∉ s
⊢ 0 = f i * 0

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ s.indicator (fun j => f j * g j) i = f i * s.indicator g i

Tactic:
simp only [indicator]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
⊢ (if i ∈ s then f i * g i else 0) = f i * if i ∈ s then g i else 0

Proof state:
case neg
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∉ s
⊢ 0 = f i * 0

Tactic:
rw [mul_zero]

Result:
no goals

Proof state:
case pos
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
i : ι
s : Set ι
f g : ι → M₀
h✝ : i ∈ s
⊢ f i * g i = f i * g i

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Idempotents.lean
lemma bijective_pi_of_isIdempotentElem (e : I → R)
    (he : ∀ i, IsIdempotentElem (e i))
    (he₁ : ∀ i j, i ≠ j → (1 - e i) * (1 - e j) = 0) (he₂ : ∏ i, e i = 0) :
    Function.Bijective (Pi.ringHom fun i ↦ Ideal.Quotient.mk (Ideal.span {e i})) :=
  (CompleteOrthogonalIdempotents.of_prod_one_sub
      ⟨fun i ↦ (he i).one_sub, he₁⟩ (by simpa using he₂)).bijective_pi'

Proof state:
R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : ∀ (i : I), IsIdempotentElem (e i)
he₁ : ∀ (i j : I), i ≠ j → (1 - e i) * (1 - e j) = 0
he₂ : ∏ i : I, e i = 0
⊢ ∏ i : I, (1 - (1 - e i)) = 0

Tactic:
simpa using he₂

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ico_diff_Ico_right (a b c : α) : Ico a b \ Ico c b = Ico a (min b c)

Proof state:
case inr
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
⊢ Ico a b \ Ico c b = Ico a (b ⊓ c)

Tactic:
ext x

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
x : α
⊢ x ∈ Ico a b \ Ico c b ↔ x ∈ Ico a (b ⊓ c)

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∧ (x < b → x < c) ↔ a ≤ x ∧ x < c

Tactic:
exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩

Result:
no goals

Proof state:
case inr.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
x : α
⊢ x ∈ Ico a b \ Ico c b ↔ x ∈ Ico a (b ⊓ c)

Tactic:
rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]

Result:
case inr.h
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : c ≤ b
x : α
⊢ a ≤ x ∧ x < b ∧ (x < b → x < c) ↔ a ≤ x ∧ x < c

Proof state:
case inl
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h : b ≤ c
⊢ Ico a b \ Ico c b = Ico a (b ⊓ c)

Tactic:
rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]

Result:
no goals

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
⊢ Ico a b \ Ico c b = Ico a (b ⊓ c)

Tactic:
cases le_total b c with
| inl h => rw [Ico_eq_empty_of_le h, sdiff_empty, min_eq_left h]
| inr h =>
  ext x
  rw [mem_sdiff, mem_Ico, mem_Ico, mem_Ico, min_eq_right h, and_assoc, not_and', not_le]
  exact and_congr_right' ⟨fun hx => hx.2 hx.1, fun hx => ⟨hx.trans_le h, fun _ => hx⟩⟩

Result:
no goals