harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineSpan_eq_affineSpan_lineMap_units [Nontrivial k] {s : Set P} {p : P} (hp : p ∈ s)
    (w : s → Units k) :
    affineSpan k (Set.range fun q : s => AffineMap.lineMap p ↑q (w q : k)) = affineSpan k s

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)

Tactic:
apply le_antisymm
  <;> intro q hq
  <;> erw [mem_affineSpan_iff_eq_weightedVSubOfPoint_vadd k V _ (⟨p, hp⟩ : s) q] at hq ⊢
  <;> obtain ⟨t, μ, rfl⟩ := hq
  <;> use t
  <;> [use fun x => μ x * ↑(w x); use fun x => μ x * ↑(w x)⁻¹]
  <;> simp [smul_smul]

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s

Tactic:
conv_rhs =>
  rw [this]

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k (Set.range Subtype.val)

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s

Tactic:
have : s = Set.range ((↑) : s → P) := by simp

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
this : s = Set.range Subtype.val
⊢ affineSpan k (Set.range fun q => (AffineMap.lineMap p ↑q) ↑(w q)) = affineSpan k s

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
inst✝ : Nontrivial k
s : Set P
p : P
hp : p ∈ s
w : ↑s → kˣ
⊢ s = Set.range Subtype.val

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem rightCoset_eq_iff {x y : α} : op x • (s : Set α) = op y • s ↔ y * x⁻¹ ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
exact s.mul_mem_cancel_right h

Result:
no goals

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

Tactic:
intro h z

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s

Tactic:
intro h

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s

Tactic:
exact s.one_mem

Result:
no goals

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * y⁻¹ ∈ s

Tactic:
rw [mul_inv_cancel]

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ 1 ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s

Tactic:
simp_rw [mem_rightCoset_iff, SetLike.mem_coe]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
rw [← mul_assoc]

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * y⁻¹ * (y * x⁻¹) ∈ s ↔ z * y⁻¹ ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ op x • ↑s = op y • ↑s ↔ y * x⁻¹ ∈ s

Tactic:
rw [Set.ext_iff]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 ∈ op x • ↑s ↔ x_1 ∈ op y • ↑s) ↔ y * x⁻¹ ∈ s

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) ↔ y * x⁻¹ ∈ s

Tactic:
constructor

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ (∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s) → y * x⁻¹ ∈ s

case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
⊢ y * x⁻¹ ∈ s → ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s

Proof state:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * x⁻¹ ∈ s ↔ z * y⁻¹ ∈ s

Tactic:
rw [← inv_mul_cancel_left y x⁻¹]

Result:
case mpr
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : y * x⁻¹ ∈ s
z : α
⊢ z * (y⁻¹ * (y * x⁻¹)) ∈ s ↔ z * y⁻¹ ∈ s

Proof state:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * x⁻¹ ∈ s

Tactic:
apply (h y).mpr

Result:
case mp
α : Type u_1
inst✝ : Group α
s : Subgroup α
x y : α
h : ∀ (x_1 : α), x_1 * x⁻¹ ∈ s ↔ x_1 * y⁻¹ ∈ s
⊢ y * y⁻¹ ∈ s
-- Mathlib/Data/List/Nodup.lean
theorem Nodup.filterMap {f : α → Option β} (h : ∀ a a' b, b ∈ f a → b ∈ f a' → a = a') :
    Nodup l → Nodup (filterMap f l) :=
  (Pairwise.filterMap f) @fun a a' n b bm b' bm' e => n <| h a a' b' (by rw [← e]; exact bm) bm'

Proof state:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : b ∈ f a
b' : β
bm' : b' ∈ f a'
e : b = b'
⊢ b ∈ f a

Tactic:
exact bm

Result:
no goals

Proof state:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : b ∈ f a
b' : β
bm' : b' ∈ f a'
e : b = b'
⊢ b' ∈ f a

Tactic:
rw [← e]

Result:
α : Type u
β : Type v
l : List α
f : α → Option β
h : ∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a'
a a' : α
n : a ≠ a'
b : β
bm : b ∈ f a
b' : β
bm' : b' ∈ f a'
e : b = b'
⊢ b ∈ f a
-- Mathlib/Algebra/Group/Hom/Defs.lean
@[to_additive (attr := simp)]
lemma map_comp_inv [Group G] [DivisionMonoid H] [MonoidHomClass F G H] (f : F) (g : ι → G) :
    f ∘ g⁻¹ = (f ∘ g)⁻¹

Proof state:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
x✝ : ι
⊢ (⇑f ∘ g⁻¹) x✝ = (⇑f ∘ g)⁻¹ x✝

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
⊢ ⇑f ∘ g⁻¹ = (⇑f ∘ g)⁻¹

Tactic:
ext

Result:
case h
ι : Type u_1
G : Type u_7
H : Type u_8
F : Type u_9
inst✝³ : FunLike F G H
inst✝² : Group G
inst✝¹ : DivisionMonoid H
inst✝ : MonoidHomClass F G H
f : F
g : ι → G
x✝ : ι
⊢ (⇑f ∘ g⁻¹) x✝ = (⇑f ∘ g)⁻¹ x✝
-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_id_apply (x : σ → R) : comap (AlgHom.id R (MvPolynomial σ R)) x = x

Proof state:
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x

Tactic:
funext i

Result:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i

Proof state:
case h
σ : Type u_1
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i

Tactic:
simp only [comap, AlgHom.id_apply, id, aeval_X]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_one : basicOpen (1 : R) = ⊤ :=
  TopologicalSpace.Opens.ext <| by simp

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ ↑(basicOpen 1) = ↑⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Cast/Prod.lean
theorem fst_natCast (n : ℕ) : (n : α × β).fst = n

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : AddMonoidWithOne α
inst✝ : AddMonoidWithOne β
n : ℕ
⊢ (↑n).1 = ↑n

Tactic:
induction n <;> simp [*]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
lemma shiftIso_add_inv_app (n m a a' a'' : M) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).inv.app X =
      (shiftIso F m a' a'' ha'').inv.app X ≫
        (shiftIso F n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫
          (shift F a).map ((shiftFunctorAdd C m n).inv.app X)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ (F.shiftIso (m + n) a a'' ⋯).inv.app X =
    (F.shiftIso m a' a'' ha'').inv.app X ≫
      (F.shiftIso n a a' ha').inv.app ((shiftFunctor C m).obj X) ≫ (F.shift a).map ((shiftFunctorAdd C m n).inv.app X)

Tactic:
simp [F.shiftIso_add n m a a' a'' ha' ha'']

Result:
no goals

Proof state:
C : Type u_1
A : Type u_2
inst✝⁶ : Category.{?u.49150, u_1} C
inst✝⁵ : Category.{?u.49154, u_2} A
F : C ⥤ A
M : Type u_3
inst✝⁴ : AddMonoid M
inst✝³ : HasShift C M
G : Type u_4
inst✝² : AddGroup G
inst✝¹ : HasShift C G
inst✝ : F.ShiftSequence M
n m a a' a'' : M
ha' : n + a = a'
ha'' : m + a' = a''
X : C
⊢ m + n + a = a''

Tactic:
rw [add_assoc, ha', ha'']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem append_push {as bs : Array α} {a : α} : as ++ bs.push a = (as ++ bs).push a

Proof state:
α : Type u_1
as bs : Array α
a : α
⊢ as ++ bs.push a = (as ++ bs).push a

Tactic:
cases as

Result:
case mk
α : Type u_1
bs : Array α
a : α
toList✝ : List α
⊢ { toList := toList✝ } ++ bs.push a = ({ toList := toList✝ } ++ bs).push a

Proof state:
case mk
α : Type u_1
bs : Array α
a : α
toList✝ : List α
⊢ { toList := toList✝ } ++ bs.push a = ({ toList := toList✝ } ++ bs).push a

Tactic:
cases bs

Result:
case mk.mk
α : Type u_1
a : α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ++ { toList := toList✝ }.push a = ({ toList := toList✝¹ } ++ { toList := toList✝ }).push a

Proof state:
case mk.mk
α : Type u_1
a : α
toList✝¹ toList✝ : List α
⊢ { toList := toList✝¹ } ++ { toList := toList✝ }.push a = ({ toList := toList✝¹ } ++ { toList := toList✝ }).push a

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_insertIfNewₘ [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {b : β a} : Raw.WFImp (m.insertIfNewₘ a b).1

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ m.containsₘ a = false

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (m.insertIfNewₘ a b).val

Tactic:
rw [insertIfNewₘ]

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (if m.containsₘ a = true then m else (m.consₘ a b).expandIfNecessary).val

Proof state:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : m.containsₘ a = true
⊢ Raw.WFImp m.val

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
⊢ Raw.WFImp (if m.containsₘ a = true then m else (m.consₘ a b).expandIfNecessary).val

Tactic:
split

Result:
case isTrue
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : m.containsₘ a = true
⊢ Raw.WFImp m.val

case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp (m.consₘ a b).expandIfNecessary.val

Proof state:
case isFalse
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp (m.consₘ a b).expandIfNecessary.val

Tactic:
apply wfImp_expandIfNecessary

Result:
case isFalse.h
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp (m.consₘ a b).val

Proof state:
case isFalse.h
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
b : β a
h✝ : ¬m.containsₘ a = true
⊢ Raw.WFImp (m.consₘ a b).val

Tactic:
apply wfImp_consₘ _ h _ _ (by simp_all)

Result:
no goals
-- Mathlib/Analysis/Polynomial/CauchyBound.lean
theorem IsRoot.norm_lt_cauchyBound {p : K[X]} (hp : p ≠ 0) {a : K} (h : p.IsRoot a) :
    ‖a‖₊ < cauchyBound p

Proof state:
case inl
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
ha : ‖a‖₊ = 1
this : 1 ≤ (p.cauchyBound - 1) * ↑p.natDegree
nh : 1 = p.cauchyBound
⊢ False

Tactic:
simp [← nh, tsub_self] at this

Result:
no goals

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ∑ i ∈ insert p.natDegree (range p.natDegree), p.coeff i * a ^ i = 0
⊢ ‖a‖₊ < p.cauchyBound

Tactic:
simp only [mem_range, lt_self_iff_false, not_false_eq_true, sum_insert, coeff_natDegree,
  add_eq_zero_iff_eq_neg] at h

Result:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : p.leadingCoeff * a ^ p.natDegree = -∑ i ∈ range p.natDegree, p.coeff i * a ^ i
⊢ ‖a‖₊ < p.cauchyBound

Proof state:
K : Type u_1
inst✝ : NormedDivisionRing K
p : K[X]
hp : p ≠ 0
a : K
h : ‖p.leadingCoeff‖₊ * ‖a‖₊ ^ p.natDegree = ‖∑ i ∈ range p.natDegree, p.coeff i * a ^ i‖₊
this : ‖a‖₊ ^ p.natDegree ≤ (p.cauchyBound - 1) * ((‖a‖₊ ^ p.natDegree - 1) / (‖a‖₊ - 1))
ha✝ : ‖a‖₊ ≠ 1
ha : ‖a‖₊ > 1
⊢ 0 ≤ p.cauchyBound - 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_flatMap {p : β → Prop} {l : Vector α n} {f : α → Vector β m} :
    (∀ (x) (_ : x ∈ l.flatMap f), p x) ↔ ∀ (a) (_ : a ∈ l) (b) (_ : b ∈ f a), p b

Proof state:
case mpr
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
⊢ (∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b) → ∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x

Tactic:
intros

Result:
case mpr
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Proof state:
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
⊢ (∀ (x : β), x ∈ l.flatMap f → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
simp only [mem_flatMap, forall_exists_index, and_imp]

Result:
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Proof state:
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
⊢ (∀ (x : β) (x_1 : α), x_1 ∈ l → x ∈ f x_1 → p x) ↔ ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals

Proof state:
case mpr
β : Type u_1
α : Type u_2
n m : Nat
p : β → Prop
l : Vector α n
f : α → Vector β m
a✝² : ∀ (a : α), a ∈ l → ∀ (b : β), b ∈ f a → p b
x✝¹ : β
x✝ : α
a✝¹ : x✝ ∈ l
a✝ : x✝¹ ∈ f x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.to_image_id' (h : l.HasBasis p s) : l.HasBasis (fun t ↦ ∃ i, p i ∧ s i = t) id :=
  ⟨fun _ ↦ by simp [h.mem_iff]⟩

Proof state:
α : Type u_1
ι : Sort u_4
l : Filter α
p : ι → Prop
s : ι → Set α
h : l.HasBasis p s
x✝ : Set α
⊢ x✝ ∈ l ↔ ∃ i, (∃ i_1, p i_1 ∧ s i_1 = i) ∧ id i ⊆ x✝

Tactic:
simp [h.mem_iff]

Result:
no goals
-- Mathlib/Topology/Order.lean
theorem isClosed_induced_iff [t : TopologicalSpace β] {s : Set α} {f : α → β} :
    IsClosed[t.induced f] s ↔ ∃ t, IsClosed t ∧ f ⁻¹' t = s

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s

Tactic:
letI := t.induced f

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ x, IsOpen xᶜ ∧ f ⁻¹' xᶜ = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
simp only [preimage_compl, compl_inj_iff]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ IsClosed s ↔ ∃ t_1, IsClosed t_1 ∧ f ⁻¹' t_1 = s

Tactic:
simp only [← isOpen_compl_iff, isOpen_induced_iff]

Result:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s

Proof state:
α : Type u_1
β : Type u_2
t : TopologicalSpace β
s : Set α
f : α → β
this : TopologicalSpace α := TopologicalSpace.induced f t
⊢ (∃ t_1, IsOpen t_1 ∧ f ⁻¹' t_1 = sᶜ) ↔ ∃ t_1, IsOpen t_1ᶜ ∧ f ⁻¹' t_1 = s

Tactic:
exact compl_surjective.exists.trans (by simp only [preimage_compl, compl_inj_iff])

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem norm_integral_le_abs_integral_norm : ‖∫ x in a..b, f x ∂μ‖ ≤ |∫ x in a..b, ‖f x‖ ∂μ|

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in a..b, f x ∂μ‖ ≤ |∫ (x : ℝ) in a..b, ‖f x‖ ∂μ|

Tactic:
simp only [← Real.norm_eq_abs, norm_integral_eq_norm_integral_Ioc]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ ‖∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ‖

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f : ℝ → E
μ : Measure ℝ
⊢ ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖ ≤ ‖∫ (x : ℝ) in Ι a b, ‖f x‖ ∂μ‖

Tactic:
exact le_trans (norm_integral_le_integral_norm _) (le_abs_self _)

Result:
no goals
-- Mathlib/Order/Interval/Finset/Box.lean
lemma disjoint_box_succ_prod (n : ℕ) : Disjoint (box (n + 1)) (Icc (-n : α) n)

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)

Tactic:
exact disjoint_sdiff_self_left

Result:
no goals

Proof state:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (box (n + 1)) (Icc (-↑n) ↑n)

Tactic:
rw [box_succ_eq_sdiff]

Result:
α : Type u_1
inst✝² : OrderedRing α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
n : ℕ
⊢ Disjoint (Icc (-↑n.succ) ↑n.succ \ Icc (-↑n) ↑n) (Icc (-↑n) ↑n)
-- Mathlib/Analysis/Convex/Gauge.lean
theorem Convex.gauge_le (hs : Convex ℝ s) (h₀ : (0 : E) ∈ s) (absorbs : Absorbent ℝ s) (a : ℝ) :
    Convex ℝ { x | gauge s x ≤ a }

Proof state:
case h.e'_6
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ {x | gauge s x ≤ a} = ∅

Tactic:
exact eq_empty_iff_forall_not_mem.2 fun x hx => ha <| (gauge_nonneg _).trans hx

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
⊢ Convex ℝ {x | gauge s x ≤ a}

Tactic:
by_cases ha : 0 ≤ a

Result:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

Proof state:
case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

Tactic:
convert convex_empty (𝕜 := ℝ) (E := E)

Result:
case h.e'_6
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : ¬0 ≤ a
⊢ {x | gauge s x ≤ a} = ∅

Proof state:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ {x | gauge s x ≤ a}

Tactic:
rw [gauge_le_eq hs h₀ absorbs ha]

Result:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ (⋂ r, ⋂ (_ : a < r), r • s)

Proof state:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
hs : Convex ℝ s
h₀ : 0 ∈ s
absorbs : Absorbent ℝ s
a : ℝ
ha : 0 ≤ a
⊢ Convex ℝ (⋂ r, ⋂ (_ : a < r), r • s)

Tactic:
exact convex_iInter fun i => convex_iInter fun _ => hs.smul _

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/UnderlyingMap.lean
lemma IsDominant.of_comp_of_isOpenImmersion
    (f : X ⟶ Y) (g : Y ⟶ Z) [H : IsDominant (f ≫ g)] [IsOpenImmersion g] :
    IsDominant f

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion g
H : Dense (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))
⊢ Dense (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
convert H.preimage g.isOpenEmbedding.isOpenMap using 1

Result:
case h.e'_3
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion g
H : Dense (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))
⊢ Set.range ⇑(ConcreteCategory.hom f.base) =
    ⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : IsDominant (f ≫ g)
inst✝ : IsOpenImmersion g
⊢ IsDominant f

Tactic:
rw [isDominant_iff, DenseRange] at H ⊢

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Dense (Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
inst✝ : IsOpenImmersion g
⊢ Dense (Set.range ⇑(ConcreteCategory.hom f.base))

Proof state:
case h.e'_3
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion g
H : Dense (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))
⊢ Set.range ⇑(ConcreteCategory.hom f.base) =
    ⇑(ConcreteCategory.hom g.base) ⁻¹' (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
rw [Set.preimage_image_eq _ g.isOpenEmbedding.injective]

Result:
no goals

Proof state:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
H : Dense (Set.range ⇑(ConcreteCategory.hom (f ≫ g).base))
inst✝ : IsOpenImmersion g
⊢ Dense (Set.range ⇑(ConcreteCategory.hom f.base))

Tactic:
simp only [Scheme.comp_coeBase, TopCat.coe_comp, Set.range_comp] at H

Result:
X Y Z : Scheme
f : X ⟶ Y
g : Y ⟶ Z
inst✝ : IsOpenImmersion g
H : Dense (⇑(ConcreteCategory.hom g.base) '' Set.range ⇑(ConcreteCategory.hom f.base))
⊢ Dense (Set.range ⇑(ConcreteCategory.hom f.base))