harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem comp_zero (f : NormedAddGroupHom V₂ V₃) : f.comp (0 : NormedAddGroupHom V₁ V₂) = 0

Proof state:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ (f.comp 0) x✝ = 0 x✝

Tactic:
exact map_zero f

Result:
no goals

Proof state:
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
⊢ f.comp 0 = 0

Tactic:
ext

Result:
case H
V₁ : Type u_2
V₂ : Type u_3
V₃ : Type u_4
inst✝² : SeminormedAddCommGroup V₁
inst✝¹ : SeminormedAddCommGroup V₂
inst✝ : SeminormedAddCommGroup V₃
f : NormedAddGroupHom V₂ V₃
x✝ : V₁
⊢ (f.comp 0) x✝ = 0 x✝
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.forall_mem_mem (h : HasBasis l p s) {x : α} :
    (∀ t ∈ l, x ∈ t) ↔ ∀ i, p i → x ∈ s i

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
exact ⟨fun h i hi => h (s i) i hi Subset.rfl, fun h t i hi ht => ht (h i hi)⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ t ∈ l, x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i

Tactic:
simp only [h.mem_iff, exists_imp, and_imp]

Result:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x : α
⊢ (∀ (t : Set α) (x_1 : ι), p x_1 → s x_1 ⊆ t → x ∈ t) ↔ ∀ (i : ι), p i → x ∈ s i
-- Mathlib/Data/Matroid/Restrict.lean
theorem IsBasis.isBasis_isRestriction (hI : M.IsBasis I X) (hNM : N ≤r M) (hX : X ⊆ N.E) :
    N.IsBasis I X

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
N : Matroid α
hI : M.IsBasis I X
hNM : N ≤r M
hX : X ⊆ N.E
⊢ N.IsBasis I X

Tactic:
obtain ⟨R, hR, rfl⟩ := hNM

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
R : Set α
hR : R ⊆ M.E
hX : X ⊆ (M ↾ R).E
⊢ (M ↾ R).IsBasis I X

Tactic:
rwa [isBasis_restrict_iff, and_iff_left (show X ⊆ R from hX)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
lemma measure_univ_of_tendsto_atBot_atBot (hf : Tendsto f atBot atBot) :
    f.measure univ = ∞

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
⊢ f.measure univ = ⊤

Tactic:
rw [← top_le_iff, ← f.measure_Iio_of_tendsto_atBot_atBot hf 0]

Result:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
⊢ f.measure (Iio 0) ≤ f.measure univ

Proof state:
f : StieltjesFunction
hf : Tendsto (↑f) atBot atBot
⊢ f.measure (Iio 0) ≤ f.measure univ

Tactic:
exact measure_mono (subset_univ _)

Result:
no goals
-- Mathlib/Data/Fin/VecNotation.lean
theorem range_cons (x : α) (u : Fin n → α) : Set.range (vecCons x u) = {x} ∪ Set.range u :=
  Set.ext fun y => by simp [Fin.exists_fin_succ, eq_comm]

Proof state:
α : Type u
n : ℕ
x : α
u : Fin n → α
y : α
⊢ y ∈ Set.range (vecCons x u) ↔ y ∈ {x} ∪ Set.range u

Tactic:
simp [Fin.exists_fin_succ, eq_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem head_take {l : List α} {n : Nat} (h : l.take n ≠ []) :
    (l.take n).head h = l.head (by simp_all)

Proof state:
case hnc
α : Type u_1
l : List α
n : Nat
h : take n l ≠ []
⊢ ¬n = 0

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type ?u.4005
l : List α
n : Nat
h : take n l ≠ []
⊢ l ≠ []

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l : List α
n : Nat
h : take n l ≠ []
⊢ (take n l).head h = l.head ⋯

Tactic:
apply Option.some_inj.1

Result:
α : Type u_1
l : List α
n : Nat
h : take n l ≠ []
⊢ some ((take n l).head h) = some (l.head ⋯)

Proof state:
α : Type u_1
l : List α
n : Nat
h : take n l ≠ []
⊢ some ((take n l).head h) = some (l.head ⋯)

Tactic:
rw [← head?_eq_head, ← head?_eq_head, head?_take, if_neg]

Result:
case hnc
α : Type u_1
l : List α
n : Nat
h : take n l ≠ []
⊢ ¬n = 0
-- Mathlib/LinearAlgebra/Projection.lean
theorem linearProjOfIsCompl_apply_left {F : Type*} [AddCommGroup F] [Module R F]
    (i : F →ₗ[R] E) (hi : Function.Injective i)
    (h : IsCompl (LinearMap.range i) q) (x : F) :
    linearProjOfIsCompl q i hi h (i x) = x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl (range i) q
x : F
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Tactic:
let ix : LinearMap.range i := ⟨i x, mem_range_self i x⟩

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl (range i) q
x : F
ix : ↥(range i) := ⟨i x, ⋯⟩
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl (range i) q
x : F
ix : ↥(range i) := ⟨i x, ⋯⟩
⊢ (linearProjOfIsCompl q i hi h) (i x) = x

Tactic:
change linearProjOfIsCompl q i hi h ix = x

Result:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl (range i) q
x : F
ix : ↥(range i) := ⟨i x, ⋯⟩
⊢ (linearProjOfIsCompl q i hi h) ↑ix = x

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
q : Submodule R E
F : Type u_7
inst✝¹ : AddCommGroup F
inst✝ : Module R F
i : F →ₗ[R] E
hi : Function.Injective ⇑i
h : IsCompl (range i) q
x : F
ix : ↥(range i) := ⟨i x, ⋯⟩
⊢ (linearProjOfIsCompl q i hi h) ↑ix = x

Tactic:
rw [linearProjOfIsCompl, coe_comp, LinearEquiv.coe_coe, Function.comp_apply,
  LinearEquiv.symm_apply_eq, Submodule.linearProjOfIsCompl_apply_left, Subtype.ext_iff,
  LinearEquiv.ofInjective_apply]

Result:
no goals
-- Mathlib/Analysis/Complex/Periodic.lean
theorem cuspFunction_zero_of_zero_at_inf (hh : 0 < h) (h_zer : ZeroAtFilter I∞ f) :
    cuspFunction h f 0 = 0

Proof state:
h : ℝ
f : ℂ → ℂ
hh : 0 < h
h_zer : I∞.ZeroAtFilter f
⊢ cuspFunction h f 0 = 0

Tactic:
simpa only [cuspFunction, update_self] using (h_zer.comp (invQParam_tendsto hh)).limUnder_eq

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem attachWith_map_subtype_val {p : α → Prop} (l : Array α) (H : ∀ a ∈ l, p a) :
    (l.attachWith p H).map Subtype.val = l

Proof state:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map Subtype.val ({ toList := toList✝ }.attachWith p H) = { toList := toList✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
p : α → Prop
l : Array α
H : ∀ (a : α), a ∈ l → p a
⊢ map Subtype.val (l.attachWith p H) = l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → p a
⊢ map Subtype.val ({ toList := toList✝ }.attachWith p H) = { toList := toList✝ }
-- Mathlib/Analysis/Calculus/VectorField.lean
theorem lieBracketWithin_eq_lieBracket (hs : UniqueDiffWithinAt 𝕜 s x)
    (hV : DifferentiableAt 𝕜 V x) (hW : DifferentiableAt 𝕜 W x) :
    lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
V W : E → E
s : Set E
x : E
hs : UniqueDiffWithinAt 𝕜 s x
hV : DifferentiableAt 𝕜 V x
hW : DifferentiableAt 𝕜 W x
⊢ lieBracketWithin 𝕜 V W s x = lieBracket 𝕜 V W x

Tactic:
simp [lieBracketWithin, lieBracket, fderivWithin_eq_fderiv, hs, hV, hW]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem dite_then_false {p : Prop} [Decidable p] {x : ¬ p → Prop} : (if h : p then False else x h) ↔ ∃ h : ¬ p, x h

Proof state:
p : Prop
inst✝ : Decidable p
x : ¬p → Prop
⊢ (if h : p then False else x h) ↔ ∃ h, x h

Tactic:
split <;> simp_all

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/OfNorm.lean
theorem add_left_aux8 (y z : E) :
    ‖(I : 𝕜) • y‖ * ‖(I : 𝕜) • y‖ + ‖(I : 𝕜) • y - 2 • z‖ * ‖(I : 𝕜) • y - 2 • z‖ =
    2 * (‖(I : 𝕜) • y - z‖ * ‖(I : 𝕜) • y - z‖ + ‖z‖ * ‖z‖)

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : InnerProductSpaceable E
y z : E
⊢ ‖I • y‖ * ‖I • y‖ + ‖I • y - 2 • z‖ * ‖I • y - 2 • z‖ = 2 * (‖I • y - z‖ * ‖I • y - z‖ + ‖z‖ * ‖z‖)

Tactic:
convert parallelogram_identity ((I : 𝕜) • y - z) z using 4 <;> module

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem dist_le_tsum_of_dist_le_of_tendsto₀ (d : ℕ → ℝ) (hf : ∀ n, dist (f n) (f n.succ) ≤ d n)
    (hd : Summable d) (ha : Tendsto f atTop (𝓝 a)) : dist (f 0) a ≤ tsum d

Proof state:
α : Type u_1
inst✝ : PseudoMetricSpace α
f : ℕ → α
a : α
d : ℕ → ℝ
hf : ∀ (n : ℕ), dist (f n) (f n.succ) ≤ d n
hd : Summable d
ha : Tendsto f atTop (𝓝 a)
⊢ dist (f 0) a ≤ tsum d

Tactic:
simpa only [zero_add] using dist_le_tsum_of_dist_le_of_tendsto d hf hd ha 0

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MutuallySingular.lean
@[simp]
lemma restrict_nullSet (h : μ ⟂ₘ ν) : μ.restrict h.nullSet = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
h : μ ⟂ₘ ν
⊢ μ.restrict h.nullSet = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem forall_mem_dualAnnihilator_apply_eq_zero_iff (W : Subspace K V) (v : V) :
    (∀ φ : Module.Dual K V, φ ∈ W.dualAnnihilator → φ v = 0) ↔ v ∈ W

Proof state:
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ φ ∈ dualAnnihilator W, φ v = 0) ↔ v ∈ W

Tactic:
rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get?_eq_some_getD [EquivBEq α] [LawfulHashable α] {a : α} {fallback : β} :
    a ∈ m → get? m a = some (getD m a fallback)

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
a : α
fallback : β
⊢ a ∈ m → get? m a = some (getD m a fallback)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem offDiag_inter : (s ∩ t).offDiag = s.offDiag ∩ t.offDiag :=
  ext fun x => by
    simp only [mem_offDiag, mem_inter_iff]
    tauto

Proof state:
α : Type u_1
s t : Set α
x : α × α
⊢ x ∈ (s ∩ t).offDiag ↔ x ∈ s.offDiag ∩ t.offDiag

Tactic:
simp only [mem_offDiag, mem_inter_iff]

Result:
α : Type u_1
s t : Set α
x : α × α
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2

Proof state:
α : Type u_1
s t : Set α
x : α × α
⊢ (x.1 ∈ s ∧ x.1 ∈ t) ∧ (x.2 ∈ s ∧ x.2 ∈ t) ∧ x.1 ≠ x.2 ↔
    (x.1 ∈ s ∧ x.2 ∈ s ∧ x.1 ≠ x.2) ∧ x.1 ∈ t ∧ x.2 ∈ t ∧ x.1 ≠ x.2

Tactic:
tauto

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/BigOperators.lean
theorem multiset_prod_mem_multiset_prod (t : Multiset ι) (f : ι → Set α) (g : ι → α)
    (hg : ∀ i ∈ t, g i ∈ f i) : (t.map g).prod ∈ (t.map f).prod

Proof state:
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
t : Multiset ι
f : ι → Set α
g : ι → α
hg : ∀ i ∈ t, g i ∈ f i
⊢ (Multiset.map g t).prod ∈ (Multiset.map f t).prod

Tactic:
induction t using Quotient.inductionOn

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (Multiset.map g ⟦a✝⟧).prod ∈ (Multiset.map f ⟦a✝⟧).prod

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (List.map g a✝).prod ∈ (List.map f a✝).prod

Tactic:
exact list_prod_mem_list_prod _ _ _ hg

Result:
no goals

Proof state:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (Multiset.map g ⟦a✝⟧).prod ∈ (Multiset.map f ⟦a✝⟧).prod

Tactic:
simp_rw [Multiset.quot_mk_to_coe, Multiset.map_coe, Multiset.prod_coe]

Result:
case h
ι : Type u_1
α : Type u_2
inst✝ : CommMonoid α
f : ι → Set α
g : ι → α
a✝ : List ι
hg : ∀ i ∈ ⟦a✝⟧, g i ∈ f i
⊢ (List.map g a✝).prod ∈ (List.map f a✝).prod
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
lemma finrank_orthogonal (hB : B.Nondegenerate) (hB₀ : B.IsRefl) (W : Submodule K V) :
    finrank K (B.orthogonal W) = finrank K V - finrank K W

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Tactic:
rw [B.orthogonal_top_eq_bot hB hB₀, inf_bot_eq, finrank_bot, add_zero] at this

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Tactic:
omega

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W

Tactic:
have := finrank_add_finrank_orthogonal hB₀ (W := W)

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
this : finrank K ↥W + finrank K ↥(B.orthogonal W) = finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)
⊢ finrank K ↥(B.orthogonal W) = finrank K V - finrank K ↥W
-- Mathlib/Data/Setoid/Basic.lean
theorem eq_top_iff {s : Setoid α} : s = (⊤ : Setoid α) ↔ ∀ x y : α, s x y

Proof state:
α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → s x y) ↔ ∀ (x y : α), s x y

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, forall_true_left]

Result:
no goals

Proof state:
α : Type u_1
s : Setoid α
⊢ s = ⊤ ↔ ∀ (x y : α), s x y

Tactic:
rw [_root_.eq_top_iff, Setoid.le_def, Setoid.top_def]

Result:
α : Type u_1
s : Setoid α
⊢ (∀ {x y : α}, ⊤ x y → s x y) ↔ ∀ (x y : α), s x y
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem divX_one : divX (1 : R[X]) = 0

Proof state:
case a
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (divX 1).coeff n✝ = coeff 0 n✝

Tactic:
simpa only [coeff_divX, coeff_zero] using coeff_one

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
⊢ divX 1 = 0

Tactic:
ext

Result:
case a
R : Type u
inst✝ : Semiring R
n✝ : ℕ
⊢ (divX 1).coeff n✝ = coeff 0 n✝
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMap_prod_left {p : TangentBundle I M} {y₀ : M'} :
    tangentMap I (I.prod I') (fun x => (x, y₀)) p = ⟨(p.1, y₀), (p.2, 0)⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I M
y₀ : M'
⊢ (ContinuousLinearMap.inl 𝕜 (TangentSpace I p.proj) (TangentSpace I' y₀)) p.snd = (p.snd, 0)

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I M
y₀ : M'
⊢ tangentMap I (I.prod I') (fun x => (x, y₀)) p = { proj := (p.proj, y₀), snd := (p.snd, 0) }

Tactic:
simp only [tangentMap, mfderiv_prod_left, TotalSpace.mk_inj]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle I M
y₀ : M'
⊢ (ContinuousLinearMap.inl 𝕜 (TangentSpace I p.proj) (TangentSpace I' y₀)) p.snd = (p.snd, 0)
-- Mathlib/CategoryTheory/SmallObject/Iteration/FunctorOfCocone.lean
lemma ofCocone_map_to_top (i : J) (hi : i < j) :
    (ofCocone c).map (homOfLE hi.le) =
      (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ (ofCocone c).map (homOfLE ⋯) = (ofCoconeObjIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCoconeObjIsoPt c).inv

Tactic:
dsimp [ofCocone, ofCocone.map, ofCoconeObjIso, ofCoconeObjIsoPt]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ (if h₂ : j < j then (ofCocone.objIso c i ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c j h₂).inv
    else
      if h₁ : i < j then
        (ofCocone.objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j)
      else eqToHom ⋯) =
    (ofCocone.objIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCocone.objIsoPt c).inv

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ ¬j < j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
J : Type u
inst✝ : LinearOrder J
j : J
F : ↑(Set.Iio j) ⥤ C
c : Cocone F
i : J
hi : i < j
⊢ (if h₂ : j < j then (ofCocone.objIso c i ⋯).hom ≫ F.map (homOfLE ⋯) ≫ (ofCocone.objIso c j h₂).inv
    else
      if h₁ : i < j then
        (ofCocone.objIso c i h₁).hom ≫ c.ι.app ⟨i, h₁⟩ ≫ (ofCocone.objIsoPt c).inv ≫ 𝟙 (ofCocone.obj c j)
      else eqToHom ⋯) =
    (ofCocone.objIso c i hi).hom ≫ c.ι.app ⟨i, hi⟩ ≫ (ofCocone.objIsoPt c).inv

Tactic:
rw [dif_neg (by simp), dif_pos hi, comp_id]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem t2Space_iff_nhds :
    T2Space X ↔ Pairwise fun x y : X => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
⊢ T2Space X ↔ Pairwise fun x y => ∃ U ∈ 𝓝 x, ∃ V ∈ 𝓝 y, Disjoint U V

Tactic:
simp only [t2Space_iff_disjoint_nhds, Filter.disjoint_iff, Pairwise]

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem coe_range (φ : F) :
    ((NonUnitalStarAlgHom.range φ : NonUnitalStarSubalgebra R B) : Set B) = Set.range (φ : A → B) :=
  by ext; rw [SetLike.mem_coe, mem_range]; rfl

Proof state:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : Star B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
rfl

Result:
no goals

Proof state:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : Star B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalStarAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ

Tactic:
rw [SetLike.mem_coe, mem_range]

Result:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : Star B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
x✝ : B
⊢ (∃ x, φ x = x✝) ↔ x✝ ∈ Set.range ⇑φ

Proof state:
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : Star B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
⊢ ↑(NonUnitalStarAlgHom.range φ) = Set.range ⇑φ

Tactic:
ext

Result:
case h
F : Type v'
R : Type u
A : Type v
B : Type w
inst✝⁹ : CommSemiring R
inst✝⁸ : NonUnitalNonAssocSemiring A
inst✝⁷ : Module R A
inst✝⁶ : Star A
inst✝⁵ : NonUnitalNonAssocSemiring B
inst✝⁴ : Module R B
inst✝³ : Star B
inst✝² : FunLike F A B
inst✝¹ : NonUnitalAlgHomClass F R A B
inst✝ : StarHomClass F A B
φ : F
x✝ : B
⊢ x✝ ∈ ↑(NonUnitalStarAlgHom.range φ) ↔ x✝ ∈ Set.range ⇑φ
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
lemma dist_mono_right_pi : MonotoneOn (dist x) (Ici x)

Proof state:
ι : Type u_2
inst✝ : Fintype ι
x : ι → ℝ
⊢ MonotoneOn (dist x) (Ici x)

Tactic:
simpa only [dist_comm _ x] using dist_mono_left_pi (y := x)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z || y && z)

Proof state:
⊢ ∀ (x y z : Bool), ((x || y) && z) = (x && z || y && z)

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem inv_Ioo_0_right {a : α} (ha : a < 0) : (Ioo a 0)⁻¹ = Iio a⁻¹

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
⊢ (Ioo a 0)⁻¹ = Iio a⁻¹

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
⊢ x ∈ (Ioo a 0)⁻¹ ↔ x ∈ Iio a⁻¹

Tactic:
refine ⟨fun h ↦ (lt_inv_of_neg (inv_neg''.1 h.2) ha).2 h.1, fun h ↦ ?_⟩

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
⊢ x ∈ (Ioo a 0)⁻¹

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
⊢ x ∈ (Ioo a 0)⁻¹

Tactic:
have h' := (h.trans (inv_neg''.2 ha))

Result:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
h' : x < 0
⊢ x ∈ (Ioo a 0)⁻¹

Proof state:
case h
α : Type u_1
inst✝ : LinearOrderedField α
a : α
ha : a < 0
x : α
h : x ∈ Iio a⁻¹
h' : x < 0
⊢ x ∈ (Ioo a 0)⁻¹

Tactic:
exact ⟨(lt_inv_of_neg ha h').2 h, inv_neg''.2 h'⟩

Result:
no goals