harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Decomposition/RadonNikodym.lean
lemma setIntegral_toReal_rnDeriv_eq_withDensity' [SigmaFinite μ]
    {s : Set α} (hs : MeasurableSet s) :
    ∫ x in s, (μ.rnDeriv ν x).toReal ∂ν = (ν.withDensity (μ.rnDeriv ν) s).toReal

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∫ (x : α) in s, (μ.rnDeriv ν x).toReal ∂ν = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [integral_toReal (Measure.measurable_rnDeriv _ _).aemeasurable]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ ∀ᵐ (x : α) ∂ν.restrict s, μ.rnDeriv ν x < ⊤

Tactic:
exact ae_restrict_of_ae (Measure.rnDeriv_lt_top _ _)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (∫⁻ (a : α) in s, μ.rnDeriv ν a ∂ν).toReal = ((ν.withDensity (μ.rnDeriv ν)) s).toReal

Tactic:
rw [ENNReal.toReal_eq_toReal_iff, ← withDensity_apply _ hs]

Result:
α : Type u_1
m : MeasurableSpace α
μ ν : Measure α
inst✝ : SigmaFinite μ
s : Set α
hs : MeasurableSet s
⊢ (ν.withDensity (μ.rnDeriv ν)) s = (ν.withDensity (μ.rnDeriv ν)) s ∨
    (ν.withDensity (μ.rnDeriv ν)) s = 0 ∧ (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∨
      (ν.withDensity (μ.rnDeriv ν)) s = ⊤ ∧ (ν.withDensity (μ.rnDeriv ν)) s = 0
-- Mathlib/Algebra/Module/Torsion.lean
theorem mem_torsionBySet_iff (x : M) : x ∈ torsionBySet R M s ↔ ∀ a : s, (a : R) • x = 0

Proof state:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a

Tactic:
exact h ⟨a, ha⟩

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
⊢ x ∈ torsionBySet R M s ↔ ∀ (a : ↑s), ↑a • x = 0

Tactic:
refine ⟨fun h ⟨a, ha⟩ => mem_sInf.mp h _ (Set.mem_image_of_mem _ ha), fun h => mem_sInf.mpr ?_⟩

Result:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ p ∈ torsionBy R M '' s, x ∈ p

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
⊢ ∀ p ∈ torsionBy R M '' s, x ∈ p

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set R
x : M
h : ∀ (a : ↑s), ↑a • x = 0
a : R
ha : a ∈ s
⊢ x ∈ torsionBy R M a
-- Mathlib/Algebra/Regular/Basic.lean
theorem isRegular_mul_iff : IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

Proof state:
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine Iff.trans ?_ isRegular_mul_and_mul_iff

Result:
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)

Proof state:
R : Type u_1
inst✝ : CommSemigroup R
a b : R
⊢ IsRegular (a * b) ↔ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨fun ab => ⟨ab, by rwa [mul_comm]⟩, fun rab => rab.1⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommSemigroup R
a b : R
ab : IsRegular (a * b)
⊢ IsRegular (b * a)

Tactic:
rwa [mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem le_append_left [LT α] [Std.Irrefl (· < · : α → α → Prop)]
    {l₁ l₂ : Array α} : l₁ ≤ l₁ ++ l₂

Proof state:
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₁ l₂ : Array α
⊢ l₁ ≤ l₁ ++ l₂

Tactic:
cases l₁

Result:
case mk
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₂ : Array α
toList✝ : List α
⊢ { toList := toList✝ } ≤ { toList := toList✝ } ++ l₂

Proof state:
case mk
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
l₂ : Array α
toList✝ : List α
⊢ { toList := toList✝ } ≤ { toList := toList✝ } ++ l₂

Tactic:
cases l₂

Result:
case mk.mk
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ≤ { toList := toList✝¹ } ++ { toList := toList✝ }

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : LT α
inst✝ : Std.Irrefl fun x1 x2 => x1 < x2
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ≤ { toList := toList✝¹ } ++ { toList := toList✝ }

Tactic:
simpa using List.le_append_left

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Finite.lean
theorem edgeFinset_sdiff [DecidableEq V] :
    (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset

Proof state:
V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑G₁.edgeSet
inst✝¹ : Fintype ↑G₂.edgeSet
inst✝ : DecidableEq V
⊢ (G₁ \ G₂).edgeFinset = G₁.edgeFinset \ G₂.edgeFinset

Tactic:
simp [edgeFinset]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/EpiMono.lean
theorem g_ne_h (x : B) (hx : x ∉ f.hom.range) : g ≠ h

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r :
  fromCoset ⟨x • ↑⟨↑(Hom.hom f).range, ⋯⟩, ⋯⟩ =
    (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False

Tactic:
simp only [MonoidHom.coe_range, Subtype.coe_mk, Equiv.symm_swap, Equiv.toFun_as_coe,
  Equiv.coe_trans, Function.comp_apply] at r

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : fromCoset ⟨x • Set.range ⇑(Hom.hom f), ⋯⟩ = τ ((g x) ((Equiv.symm τ) (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩)))
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : (g x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (h x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False

Tactic:
change _ = ((τ).symm.trans (g x)).trans τ _ at r

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r :
  (g x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r :
  (g x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False

Tactic:
rw [g_apply_fromCoset] at r

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r :
  fromCoset ⟨x • ↑⟨↑(Hom.hom f).range, ⋯⟩, ⋯⟩ =
    (((Equiv.symm τ).trans (g x)).trans τ) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : fromCoset ⟨x • Set.range ⇑(Hom.hom f), ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Tactic:
exact fromCoset_ne_of_nin_range _ hx r

Result:
no goals

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : fromCoset ⟨x • Set.range ⇑(Hom.hom f), ⋯⟩ = τ ((g x) ((Equiv.symm τ) (fromCoset ⟨Set.range ⇑(Hom.hom f), ⋯⟩)))
⊢ False

Tactic:
erw [Equiv.swap_apply_left, g_apply_infinity, Equiv.swap_apply_right] at r

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : fromCoset ⟨x • Set.range ⇑(Hom.hom f), ⋯⟩ = fromCoset ⟨↑(Hom.hom f).range, ⋯⟩
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
⊢ g ≠ h

Tactic:
intro r

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : g = h
⊢ False

Proof state:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : g = h
⊢ False

Tactic:
replace r :=
  DFunLike.congr_fun (DFunLike.congr_fun r x) (fromCoset ⟨f.hom.range, ⟨1, one_leftCoset _⟩⟩)

Result:
A B : Grp
f : A ⟶ B
x : ↑B
hx : x ∉ (Hom.hom f).range
r : (g x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩) = (h x) (fromCoset ⟨↑(Hom.hom f).range, ⋯⟩)
⊢ False
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_eq_pow_card (s : Finset α) (f : α → β) (comm) (m : β) (h : ∀ x ∈ s, f x = m) :
    s.noncommProd f comm = m ^ s.card

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

Tactic:
simp only [Finset.card_def, Multiset.card_map]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ s.noncommProd f comm = m ^ #s

Tactic:
rw [noncommProd, Multiset.noncommProd_eq_pow_card _ _ m]

Result:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ m ^ (Multiset.map f s.val).card = m ^ #s

α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Proof state:
α : Type u_3
β : Type u_4
inst✝ : Monoid β
s : Finset α
f : α → β
comm : (↑s).Pairwise (Commute on f)
m : β
h : ∀ x ∈ s, f x = m
⊢ ∀ x ∈ Multiset.map f s.val, x = m

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem continuousAt_iff' [TopologicalSpace β] {f : β → α} {b : β} :
    ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ x in 𝓝 b, dist (f x) (f b) < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : TopologicalSpace β
f : β → α
b : β
⊢ ContinuousAt f b ↔ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 b, dist (f x) (f b) < ε

Tactic:
rw [ContinuousAt, tendsto_nhds]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LinearMap.lean
theorem inner_map_self_eq_zero (T : V →ₗ[ℂ] V) : (∀ x : V, ⟪T x, x⟫_ℂ = 0) ↔ T = 0

Proof state:
case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪T x, x⟫_ℂ = 0) → T = 0

Tactic:
intro hT

Result:
case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
⊢ T = 0

Proof state:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ (0 - 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0

Tactic:
norm_num

Result:
no goals

Proof state:
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪T x, x⟫_ℂ = 0) ↔ T = 0

Tactic:
constructor

Result:
case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ (∀ (x : V), ⟪T x, x⟫_ℂ = 0) → T = 0

case mpr
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T = 0 → ∀ (x : V), ⟪T x, x⟫_ℂ = 0

Proof state:
case mp
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
⊢ T = 0

Tactic:
ext x

Result:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ T x = 0 x

Proof state:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ T x = 0 x

Tactic:
rw [LinearMap.zero_apply, ← @inner_self_eq_zero ℂ V, inner_map_polarization]

Result:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ (⟪T (T x + x), T x + x⟫_ℂ - ⟪T (T x - x), T x - x⟫_ℂ + Complex.I * ⟪T (T x + Complex.I • x), T x + Complex.I • x⟫_ℂ -
        Complex.I * ⟪T (T x - Complex.I • x), T x - Complex.I • x⟫_ℂ) /
      4 =
    0

Proof state:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ (⟪T (T x + x), T x + x⟫_ℂ - ⟪T (T x - x), T x - x⟫_ℂ + Complex.I * ⟪T (T x + Complex.I • x), T x + Complex.I • x⟫_ℂ -
        Complex.I * ⟪T (T x - Complex.I • x), T x - Complex.I • x⟫_ℂ) /
      4 =
    0

Tactic:
simp only [hT]

Result:
case mp.h
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
hT : ∀ (x : V), ⟪T x, x⟫_ℂ = 0
x : V
⊢ (0 - 0 + Complex.I * 0 - Complex.I * 0) / 4 = 0

Proof state:
case mpr
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
T : V →ₗ[ℂ] V
⊢ T = 0 → ∀ (x : V), ⟪T x, x⟫_ℂ = 0

Tactic:
rintro rfl x

Result:
case mpr
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
x : V
⊢ ⟪0 x, x⟫_ℂ = 0

Proof state:
case mpr
V : Type u_4
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℂ V
x : V
⊢ ⟪0 x, x⟫_ℂ = 0

Tactic:
simp only [LinearMap.zero_apply, inner_zero_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/InsertIdx.lean
theorem getElem?_insertIdx_self {l : List α} {x : α} {n : Nat} :
    (insertIdx n x l)[n]? = if n ≤ l.length then some x else none

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ (if n = n then if n ≤ l.length then some x else none else l[n - 1]?) = if n ≤ l.length then some x else none

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ ¬n < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type u
l : List α
x : α
n : Nat
⊢ (insertIdx n x l)[n]? = if n ≤ l.length then some x else none

Tactic:
rw [getElem?_insertIdx, if_neg (by omega)]

Result:
α : Type u
l : List α
x : α
n : Nat
⊢ (if n = n then if n ≤ l.length then some x else none else l[n - 1]?) = if n ≤ l.length then some x else none
-- Mathlib/RingTheory/Ideal/Maps.lean
lemma disjoint_map_primeCompl_iff_comap_le {S : Type*} [Semiring S] {f : R →+* S}
    {p : Ideal R} {I : Ideal S} [p.IsPrime] :
    Disjoint (I : Set S) (p.primeCompl.map f) ↔ I.comap f ≤ p

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
f : R →+* S
p : Ideal R
I : Ideal S
inst✝ : p.IsPrime
⊢ Disjoint ↑(Submonoid.map f p.primeCompl) ↑I ↔ comap f I ≤ p

Tactic:
simp [Set.disjoint_iff, Set.ext_iff, Ideal.primeCompl, not_imp_not, SetLike.le_def]

Result:
no goals

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
f : R →+* S
p : Ideal R
I : Ideal S
inst✝ : p.IsPrime
⊢ Disjoint ↑I ↑(Submonoid.map f p.primeCompl) ↔ comap f I ≤ p

Tactic:
rw [disjoint_comm]

Result:
R : Type u
inst✝² : CommSemiring R
S : Type u_2
inst✝¹ : Semiring S
f : R →+* S
p : Ideal R
I : Ideal S
inst✝ : p.IsPrime
⊢ Disjoint ↑(Submonoid.map f p.primeCompl) ↑I ↔ comap f I ≤ p
-- Mathlib/ModelTheory/Semantics.lean
theorem Model.union {T' : L.Theory} (h : M ⊨ T) (h' : M ⊨ T') : M ⊨ T ∪ T'

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : M ⊨ T
h' : M ⊨ T'
⊢ M ⊨ T ∪ T'

Tactic:
simp only [model_iff, Set.mem_union] at *

Result:
L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : ∀ φ ∈ T, M ⊨ φ
h' : ∀ φ ∈ T', M ⊨ φ
⊢ ∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ

Proof state:
L : Language
M : Type w
inst✝ : L.Structure M
T T' : L.Theory
h : ∀ φ ∈ T, M ⊨ φ
h' : ∀ φ ∈ T', M ⊨ φ
⊢ ∀ (φ : L.Sentence), φ ∈ T ∨ φ ∈ T' → M ⊨ φ

Tactic:
exact fun φ hφ => hφ.elim (h _) (h' _)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.ι_π [DecidableEq J] (f : J → C) [HasBiproduct f] (j j' : J) :
    biproduct.ι f j ≫ biproduct.π f j' = if h : j = j' then eqToHom (congr_arg f h) else 0

Proof state:
J : Type w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : DecidableEq J
f : J → C
inst✝ : HasBiproduct f
j j' : J
⊢ ι f j ≫ π f j' = if h : j = j' then eqToHom ⋯ else 0

Tactic:
convert (biproduct.bicone f).ι_π j j'

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem biproduct.lift_eq {T : C} {g : ∀ j, T ⟶ f j} :
    biproduct.lift g = ∑ j, g j ≫ biproduct.ι f j

Proof state:
case w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
j : J
⊢ lift g ≫ π f j = (∑ j : J, g j ≫ ι f j) ≫ π f j

Tactic:
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
⊢ lift g = ∑ j : J, g j ≫ ι f j

Tactic:
ext j

Result:
case w
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
j : J
⊢ lift g ≫ π f j = (∑ j : J, g j ≫ ι f j) ≫ π f j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Fintype J
f : J → C
inst✝ : HasBiproduct f
T : C
g : (j : J) → T ⟶ f j
⊢ lift g = ∑ j : J, g j ≫ ι f j

Tactic:
classical
ext j
simp only [sum_comp, biproduct.ι_π, comp_dite, biproduct.lift_π, Category.assoc, comp_zero,
  Finset.sum_dite_eq', Finset.mem_univ, eqToHom_refl, Category.comp_id, if_true]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_ne_top (h : s.Nonempty) : infEdist x s ≠ ⊤

Proof state:
case intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hy : y ∈ s
⊢ infEdist x s ≠ ⊤

Tactic:
exact ne_top_of_le_ne_top (edist_ne_top _ _) (infEdist_le_edist_of_mem hy)

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
h : s.Nonempty
⊢ infEdist x s ≠ ⊤

Tactic:
rcases h with ⟨y, hy⟩

Result:
case intro
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x y : α
hy : y ∈ s
⊢ infEdist x s ≠ ⊤
-- Mathlib/Data/Sym/Basic.lean
theorem map_id {α : Type*} {n : ℕ} (s : Sym α n) : Sym.map id s = s

Proof state:
case h
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s

Tactic:
simp only [map, id_eq, Multiset.map_id', ← val_eq_coe]

Result:
no goals

Proof state:
α : Type u_3
n : ℕ
s : Sym α n
⊢ map id s = s

Tactic:
ext

Result:
case h
α : Type u_3
n : ℕ
s : Sym α n
⊢ ↑(map id s) = ↑s
-- Mathlib/Data/Finset/Density.lean
@[simp] lemma dens_disjUnion (s t : Finset α) (h) : dens (s.disjUnion t h) = dens s + dens t

Proof state:
α : Type u_2
inst✝ : Fintype α
s t : Finset α
h : Disjoint s t
⊢ (s.disjUnion t h).dens = s.dens + t.dens

Tactic:
simp_rw [dens, card_disjUnion, Nat.cast_add, add_div]

Result:
no goals
-- Mathlib/Algebra/Module/Projective.lean
theorem Projective.of_split [Module.Projective R M]
    (i : P →ₗ[R] M) (s : M →ₗ[R] P) (H : s.comp i = LinearMap.id) : Module.Projective R P

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
⊢ Projective R P

Tactic:
obtain ⟨g, hg⟩ := projective_lifting_property (Finsupp.linearCombination R id) s
  (fun x ↦ ⟨Finsupp.single x 1, by simp⟩)

Result:
case intro
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
⊢ Projective R P

Proof state:
case intro
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
⊢ Projective R P

Tactic:
refine ⟨g.comp i, fun x ↦ ?_⟩

Result:
case intro
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id) ((g ∘ₗ i) x) = x

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
x : P
⊢ (linearCombination R id) (Finsupp.single x 1) = x

Tactic:
simp

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝⁵ : Semiring R
P : Type u_2
inst✝⁴ : AddCommMonoid P
inst✝³ : Module R P
M : Type u_3
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Projective R M
i : P →ₗ[R] M
s : M →ₗ[R] P
H : s ∘ₗ i = LinearMap.id
g : M →ₗ[R] P →₀ R
hg : linearCombination R id ∘ₗ g = s
x : P
⊢ (linearCombination R id) ((g ∘ₗ i) x) = x

Tactic:
rw [LinearMap.comp_apply, ← LinearMap.comp_apply, hg,
  ← LinearMap.comp_apply, H, LinearMap.id_apply]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ofNat_natAbs_of_nonpos {a : Int} (H : a ≤ 0) : (natAbs a : Int) = -a

Proof state:
a : Int
H : a ≤ 0
⊢ ↑a.natAbs = -a

Tactic:
rw [← natAbs_neg, natAbs_of_nonneg (Int.neg_nonneg_of_nonpos H)]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Expect.lean
lemma expect_add_distrib (s : Finset ι) (f g : ι → M) :
    𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i

Proof state:
ι : Type u_1
M : Type u_3
inst✝¹ : AddCommMonoid M
inst✝ : Module ℚ≥0 M
s : Finset ι
f g : ι → M
⊢ 𝔼 i ∈ s, (f i + g i) = 𝔼 i ∈ s, f i + 𝔼 i ∈ s, g i

Tactic:
simp [expect, sum_add_distrib]

Result:
no goals
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma hasFPowerSeriesAt_pi_iff :
    HasFPowerSeriesAt (fun x ↦ (f · x)) (FormalMultilinearSeries.pi p) e ↔
      ∀ i, HasFPowerSeriesAt (f i) (p i) e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) e ↔ ∀ (i : ι), HasFPowerSeriesAt (f i) (p i) e

Tactic:
simp_rw [← hasFPowerSeriesWithinAt_univ]

Result:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e

Proof state:
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_9
inst✝² : Fintype ι
e : E
Fm : ι → Type u_10
inst✝¹ : (i : ι) → NormedAddCommGroup (Fm i)
inst✝ : (i : ι) → NormedSpace 𝕜 (Fm i)
f : (i : ι) → E → Fm i
p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)
⊢ HasFPowerSeriesWithinAt (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) Set.univ e ↔
    ∀ (i : ι), HasFPowerSeriesWithinAt (f i) (p i) Set.univ e

Tactic:
exact hasFPowerSeriesWithinAt_pi_iff

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Basic.lean
theorem lift_rank_eq_of_equiv_equiv (i : R → R') (j : M ≃+ M')
    (hi : Bijective i) (hc : ∀ (r : R) (m : M), j (r • m) = i r • j m) :
    lift.{v'} (Module.rank R M) = lift.{v} (Module.rank R' M') :=
  (lift_rank_le_of_surjective_injective i j hi.2 j.injective hc).antisymm <|
    lift_rank_le_of_injective_injectiveₛ i j.symm hi.1
      j.symm.injective fun _ _ ↦ j.symm_apply_eq.2 <| by erw [hc, j.apply_symm_apply]

Proof state:
R : Type u
R' : Type u'
M : Type v
M' : Type v'
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : Semiring R'
inst✝¹ : AddCommMonoid M'
inst✝ : Module R' M'
i : R → R'
j : M ≃+ M'
hi : Bijective i
hc : ∀ (r : R) (m : M), j (r • m) = i r • j m
x✝¹ : R
x✝ : M'
⊢ i x✝¹ • x✝ = j (x✝¹ • ↑j.symm x✝)

Tactic:
erw [hc, j.apply_symm_apply]

Result:
no goals