harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem mem_keys [LawfulBEq α] (h : m.1.WF) {k : α} :
    k ∈ m.1.keys ↔ m.contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
⊢ (List.keys (toListModel m.val.buckets)).contains k = true ↔ containsKey k (toListModel m.val.buckets) = true

Tactic:
rw [List.containsKey_eq_keys_contains]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
⊢ k ∈ m.val.keys ↔ m.contains k = true

Tactic:
simp_to_model

Result:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
⊢ (List.keys (toListModel m.val.buckets)).contains k = true ↔ containsKey k (toListModel m.val.buckets) = true
-- Mathlib/Data/Num/Lemmas.lean
theorem mul_to_nat (m) : ∀ n, ((m * n : PosNum) : ℕ) = m * n
  | 1 => (mul_one _).symm
  | bit0 p => show (↑(m * p) + ↑(m * p) : ℕ) = ↑m * (p + p) by rw [mul_to_nat m p, left_distrib]
  | bit1 p =>
    (add_to_nat (bit0 (m * p)) m).trans <|
      show (↑(m * p) + ↑(m * p) + ↑m : ℕ) = ↑m * (p + p) + m by rw [mul_to_nat m p, left_distrib]

Proof state:
m p : PosNum
⊢ ↑(m * p) + ↑(m * p) + ↑m = ↑m * (↑p + ↑p) + ↑m

Tactic:
rw [mul_to_nat m p, left_distrib]

Result:
no goals

Proof state:
m p : PosNum
⊢ ↑(m * p) + ↑(m * p) = ↑m * (↑p + ↑p)

Tactic:
rw [mul_to_nat m p, left_distrib]

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
theorem norm_sub_one_of_prime_ne_two {k : ℕ} (hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1)))
    [hpri : Fact (p : ℕ).Prime] [IsCyclotomicExtension {p ^ (k + 1)} K L]
    (hirr : Irreducible (cyclotomic (↑(p ^ (k + 1)) : ℕ) K)) (h : p ≠ 2) : norm K (ζ - 1) = p

Proof state:
p : ℕ+
K : Type u
L : Type v
inst✝³ : Field L
ζ : L
inst✝² : Field K
inst✝¹ : Algebra K L
k : ℕ
hζ : IsPrimitiveRoot ζ ↑(p ^ (k + 1))
hpri : Fact (Nat.Prime ↑p)
inst✝ : IsCyclotomicExtension {p ^ (k + 1)} K L
hirr : Irreducible (cyclotomic (↑(p ^ (k + 1))) K)
h : p ≠ 2
⊢ (Algebra.norm K) (ζ - 1) = ↑↑p

Tactic:
simpa using hζ.norm_pow_sub_one_of_prime_ne_two hirr k.zero_le h

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem dist_eq_add_dist_of_angle_eq_pi {p₁ p₂ p₃ : P} (h : ∠ p₁ p₂ p₃ = π) :
    dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ P

Tactic:
exact norm_sub_eq_add_norm_of_angle_eq_pi h

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : ∠ p₁ p₂ p₃ = π
⊢ P
-- Mathlib/Order/Filter/AtTopBot/CountablyGenerated.lean
theorem exists_seq_tendsto (f : Filter α) [IsCountablyGenerated f] [NeBot f] :
    ∃ x : ℕ → α, Tendsto x atTop f

Proof state:
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
⊢ ∃ x, Tendsto x atTop f

Tactic:
obtain ⟨B, h⟩ := f.exists_antitone_basis

Result:
case intro
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
⊢ ∃ x, Tendsto x atTop f

Proof state:
case intro
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f

Tactic:
exact ⟨x, h.tendsto hx⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
⊢ ∃ x, Tendsto x atTop f

Tactic:
choose x hx using fun n => Filter.nonempty_of_mem (h.mem n)

Result:
case intro
α : Type u_1
f : Filter α
inst✝¹ : f.IsCountablyGenerated
inst✝ : f.NeBot
B : ℕ → Set α
h : f.HasAntitoneBasis B
x : ℕ → α
hx : ∀ (n : ℕ), x n ∈ B n
⊢ ∃ x, Tendsto x atTop f
-- Mathlib/RingTheory/Ideal/GoingUp.lean
theorem isMaximal_comap_of_isIntegral_of_isMaximal [Algebra.IsIntegral R S] (I : Ideal S)
    [hI : I.IsMaximal] : IsMaximal (I.comap (algebraMap R S))

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (R ⧸ comap (algebraMap R S) I)

Tactic:
exact isField_of_isIntegral_of_isField
  algebraMap_quotient_injective (by rwa [← Quotient.maximal_ideal_iff_isField_quotient])

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (S ⧸ I)

Tactic:
rwa [← Quotient.maximal_ideal_iff_isField_quotient]

Result:
no goals

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ (comap (algebraMap R S) I).IsMaximal

Tactic:
refine Ideal.Quotient.maximal_of_isField _ ?_

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsField (R ⧸ comap (algebraMap R S) I)

Proof state:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
⊢ IsField (R ⧸ comap (algebraMap R S) I)

Tactic:
haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _

Result:
R : Type u_1
inst✝³ : CommRing R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : Algebra.IsIntegral R S
I : Ideal S
hI : I.IsMaximal
this : (comap (algebraMap R S) I).IsPrime
⊢ IsField (R ⧸ comap (algebraMap R S) I)
-- Mathlib/Data/Finset/Max.lean
theorem max'_image [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α)
    (h : (s.image f).Nonempty) : (s.image f).max' h = f (s.max' h.of_image)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)

Tactic:
exact .symm <| comp_sup'_eq_sup'_comp _ _ fun _ _ ↦ hf.map_max

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ (image f s).max' h = f (s.max' ⋯)

Tactic:
simp only [max', sup'_image]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : α → β
hf : Monotone f
s : Finset α
h : (image f s).Nonempty
⊢ s.sup' ⋯ (id ∘ f) = f (s.sup' ⋯ id)
-- Mathlib/Data/Fin/Rev.lean
theorem le_rev_iff {i j : Fin n} : i ≤ rev j ↔ j ≤ rev i

Proof state:
n : ℕ
i j : Fin n
⊢ i ≤ j.rev ↔ j ≤ i.rev

Tactic:
rw [← rev_le_rev, rev_rev]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem degree_eq_card_roots' {p : K[X]} {i : K →+* L} (p_ne_zero : p.map i ≠ 0)
    (hsplit : Splits i p) : (p.map i).degree = Multiset.card (p.map i).roots

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
p : K[X]
i : K →+* L
p_ne_zero : map i p ≠ 0
hsplit : Splits i p
⊢ (map i p).degree = ↑(map i p).roots.card

Tactic:
simp [degree_eq_natDegree p_ne_zero, natDegree_eq_card_roots' hsplit]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lex.lean
theorem le_empty [LT α] (l : Vector α 0) : l ≤ #v[] ↔ l = #v[]

Proof state:
case mk
α : Type u_1
inst✝ : LT α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ≤ { toArray := #[], size_toArray := ⋯ } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[], size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
l : Vector α 0
⊢ l ≤ { toArray := #[], size_toArray := ⋯ } ↔ l = { toArray := #[], size_toArray := ⋯ }

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝ : LT α
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 0
⊢ { toArray := toArray✝, size_toArray := size_toArray✝ } ≤ { toArray := #[], size_toArray := ⋯ } ↔
    { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[], size_toArray := ⋯ }
-- Mathlib/Order/Filter/Cocardinal.lean
theorem frequently_cocardinal {p : α → Prop} :
    (∃ᶠ x in cocardinal α hreg, p x) ↔ c ≤ # { x | p x }

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
p : α → Prop
⊢ (∃ᶠ (x : α) in cocardinal α hreg, p x) ↔ c ≤ #↑{x | p x}

Tactic:
simp only [Filter.Frequently, eventually_cocardinal, not_not,coe_setOf, not_lt]

Result:
no goals
-- Mathlib/LinearAlgebra/CliffordAlgebra/SpinGroup.lean
theorem star_mem_iff {x : CliffordAlgebra Q} : star x ∈ pinGroup Q ↔ x ∈ pinGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ pinGroup Q → x ∈ pinGroup Q

Tactic:
intro hx

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ pinGroup Q
⊢ x ∈ pinGroup Q

Proof state:
case h.e'_5
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ pinGroup Q
⊢ x = star (star x)

Tactic:
exact (star_star x).symm

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ pinGroup Q ↔ x ∈ pinGroup Q

Tactic:
refine ⟨?_, star_mem⟩

Result:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star x ∈ pinGroup Q → x ∈ pinGroup Q

Proof state:
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ pinGroup Q
⊢ x ∈ pinGroup Q

Tactic:
convert star_mem hx

Result:
case h.e'_5
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
hx : star x ∈ pinGroup Q
⊢ x = star (star x)
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem inf_sdiff_left (hs : s.Nonempty) (f : ι → α) (a : α) :
    (s.inf fun b => a \ f b) = a \ s.sup f

Proof state:
case cons
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
s✝ : Finset ι
h✝ : a✝ ∉ s✝
hs✝ : s✝.Nonempty
ih : (s✝.inf fun b => a \ f b) = a \ s✝.sup f
⊢ ((cons a✝ s✝ h✝).inf fun b => a \ f b) = a \ (cons a✝ s✝ h✝).sup f

Tactic:
rw [sup_cons, inf_cons, ih, sdiff_sup]

Result:
no goals

Proof state:
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
hs : s.Nonempty
f : ι → α
a : α
⊢ (s.inf fun b => a \ f b) = a \ s.sup f

Tactic:
induction hs using Finset.Nonempty.cons_induction with
| singleton => rw [sup_singleton, inf_singleton]
| cons _ _ _ _ ih => rw [sup_cons, inf_cons, ih, sdiff_sup]

Result:
no goals

Proof state:
case singleton
α : Type u_2
ι : Type u_5
inst✝ : BooleanAlgebra α
s : Finset ι
f : ι → α
a : α
a✝ : ι
⊢ ({a✝}.inf fun b => a \ f b) = a \ {a✝}.sup f

Tactic:
rw [sup_singleton, inf_singleton]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma krullDim_nonneg_iff : 0 ≤ krullDim α ↔ Nonempty α

Proof state:
α : Type u_1
inst✝ : Preorder α
⊢ 0 ≤ krullDim α ↔ Nonempty α

Tactic:
rw [← not_iff_not, not_le, not_nonempty_iff, ← krullDim_eq_bot_iff, ← WithBot.lt_coe_bot,
  bot_eq_zero, WithBot.coe_zero]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean
theorem norm_mkPiAlgebra_of_empty [IsEmpty ι] :
    ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖(1 : A)‖

Proof state:
case a
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖

Tactic:
convert ratio_le_opNorm (ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun _ => (1 : A)

Result:
case h.e'_3
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖1‖ = ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun x => 1‖ / ∏ i : ι, ‖1‖

Proof state:
case a
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ ‖1‖

Tactic:
apply opNorm_le_bound <;> simp

Result:
no goals

Proof state:
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ = ‖1‖

Tactic:
apply le_antisymm

Result:
case a
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖ ≤ ‖1‖

case a
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖1‖ ≤ ‖ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A‖

Proof state:
case h.e'_3
𝕜 : Type u
ι : Type v
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : Fintype ι
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra 𝕜 A
inst✝ : IsEmpty ι
⊢ ‖1‖ = ‖(ContinuousMultilinearMap.mkPiAlgebra 𝕜 ι A) fun x => 1‖ / ∏ i : ι, ‖1‖

Tactic:
simp [eq_empty_of_isEmpty (univ : Finset ι)]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem absNorm_ne_zero_iff_mem_nonZeroDivisors {I : Ideal S} :
    absNorm I ≠ 0 ↔ I ∈ (Ideal S)⁰

Proof state:
S : Type u_1
inst✝⁴ : CommRing S
inst✝³ : Nontrivial S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Free ℤ S
inst✝ : Module.Finite ℤ S
I : Ideal S
⊢ absNorm I ≠ 0 ↔ I ∈ (Ideal S)⁰

Tactic:
simp_rw [ne_eq, Ideal.absNorm_eq_zero_iff, mem_nonZeroDivisors_iff_ne_zero, Submodule.zero_eq_bot]

Result:
no goals
-- Mathlib/Data/Set/UnionLift.lean
theorem preimage_liftCover (t : Set β) : liftCover S f hf hS ⁻¹' t = ⋃ i, (↑) '' (f i ⁻¹' t)

Proof state:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ (iUnionLift S f hf univ ⋯ ∘ fun a => ⟨a, ⋯⟩) ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)

Tactic:
rw [preimage_comp, preimage_iUnionLift]

Result:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ (fun a => ⟨a, ⋯⟩) ⁻¹' (inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' t)) = ⋃ i, Subtype.val '' (f i ⁻¹' t)

Proof state:
case h
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈ (fun a => ⟨a, ⋯⟩) ⁻¹' (inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' t)) ↔ x✝ ∈ ⋃ i, Subtype.val '' (f i ⁻¹' t)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ liftCover S f hf hS ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)

Tactic:
change (iUnionLift S f hf univ hS.symm.subset ∘ fun a => ⟨a, mem_univ a⟩) ⁻¹' t = _

Result:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ (iUnionLift S f hf univ ⋯ ∘ fun a => ⟨a, ⋯⟩) ⁻¹' t = ⋃ i, Subtype.val '' (f i ⁻¹' t)

Proof state:
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
⊢ (fun a => ⟨a, ⋯⟩) ⁻¹' (inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' t)) = ⋃ i, Subtype.val '' (f i ⁻¹' t)

Tactic:
ext

Result:
case h
α : Type u_1
ι : Sort u_3
β : Type u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
hS : iUnion S = univ
t : Set β
x✝ : α
⊢ x✝ ∈ (fun a => ⟨a, ⋯⟩) ⁻¹' (inclusion ⋯ ⁻¹' ⋃ i, inclusion ⋯ '' (f i ⁻¹' t)) ↔ x✝ ∈ ⋃ i, Subtype.val '' (f i ⁻¹' t)
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma shift_add (a : ℤ) :
    (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq

Tactic:
dsimp

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a).v p q hpq + (γ₂.shift a).v p q hpq

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a : ℤ
⊢ (γ₁ + γ₂).shift a = γ₁.shift a + γ₂.shift a

Tactic:
ext p q hpq

Result:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a + γ₂.shift a).v p q hpq

Proof state:
case h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n : ℤ
γ₁ γ₂ : Cochain K L n
a p q : ℤ
hpq : p + n = q
⊢ ((γ₁ + γ₂).shift a).v p q hpq = (γ₁.shift a).v p q hpq + (γ₂.shift a).v p q hpq

Tactic:
simp only [shift_v', add_v]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Basic.lean
theorem natCast_mem (n : ℕ) : (n : L) ∈ S

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
S : IntermediateField K L
n : ℕ
⊢ ↑n ∈ S

Tactic:
simpa using intCast_mem S n

Result:
no goals
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem _root_.Finset.coe_infsep_of_offDiag_nonempty [DecidableEq α] {s : Finset α}
    (hs : s.offDiag.Nonempty) : (s : Set α).infsep = s.offDiag.inf' hs (uncurry dist)

Proof state:
α : Type u_1
inst✝¹ : PseudoMetricSpace α
inst✝ : DecidableEq α
s : Finset α
hs : s.offDiag.Nonempty
⊢ (↑s).infsep = s.offDiag.inf' hs (uncurry dist)

Tactic:
rw [Finset.coe_infsep, dif_pos hs]

Result:
no goals
-- Mathlib/GroupTheory/Subgroup/Simple.lean
theorem isSimpleGroup_of_surjective {H : Type*} [Group H] [IsSimpleGroup G] [Nontrivial H]
    (f : G →* H) (hf : Function.Surjective f) : IsSimpleGroup H :=
  ⟨fun H iH => by
    refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_
    · rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]
    · rw [← comap_top f] at h
      exact comap_injective hf h⟩

Proof state:
case refine_1
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊥
⊢ H = ⊥

Tactic:
rw [← map_bot f, ← h, map_comap_eq_self_of_surjective hf]

Result:
no goals

Proof state:
case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊤
⊢ H = ⊤

Tactic:
rw [← comap_top f] at h

Result:
case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = comap f ⊤
⊢ H = ⊤

Proof state:
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
⊢ H = ⊥ ∨ H = ⊤

Tactic:
refine (iH.comap f).eq_bot_or_eq_top.imp (fun h => ?_) fun h => ?_

Result:
case refine_1
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊥
⊢ H = ⊥

case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = ⊤
⊢ H = ⊤

Proof state:
case refine_2
G : Type u_1
inst✝³ : Group G
H✝ : Type u_3
inst✝² : Group H✝
inst✝¹ : IsSimpleGroup G
inst✝ : Nontrivial H✝
f : G →* H✝
hf : Function.Surjective ⇑f
H : Subgroup H✝
iH : H.Normal
h : comap f H = comap f ⊤
⊢ H = ⊤

Tactic:
exact comap_injective hf h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem combo_eq_smul_add_smul (a : Int) (xs : IntList) (b : Int) (ys : IntList) :
    combo a xs b ys = a * xs + b * ys

Proof state:
a : Int
xs : IntList
b : Int
ys : IntList
⊢ combo a xs b ys = a * xs + b * ys

Tactic:
dsimp [combo]

Result:
a : Int
xs : IntList
b : Int
ys : IntList
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys

Proof state:
case nil
a b : Int
ys : IntList
⊢ List.map (fun b_1 => b * b_1) ys = b * ys

Tactic:
rfl

Result:
no goals

Proof state:
case cons.nil
a b x : Int
xs : List Int
ih : ∀ (ys : IntList), List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys
⊢ List.map (fun a_1 => a * a_1) xs = a * xs

Tactic:
rfl

Result:
no goals

Proof state:
case cons.nil
a b x : Int
xs : List Int
ih : ∀ (ys : IntList), List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) (x :: xs) [] = a * (x :: xs) + b * []

Tactic:
simp

Result:
case cons.nil
a b x : Int
xs : List Int
ih : ∀ (ys : IntList), List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys
⊢ List.map (fun a_1 => a * a_1) xs = a * xs

Proof state:
case nil
a b : Int
ys : IntList
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) [] ys = a * [] + b * ys

Tactic:
simp

Result:
case nil
a b : Int
ys : IntList
⊢ List.map (fun b_1 => b * b_1) ys = b * ys

Proof state:
case cons
a b x : Int
xs : List Int
ih : ∀ (ys : IntList), List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys
ys : IntList
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) (x :: xs) ys = a * (x :: xs) + b * ys

Tactic:
cases ys with
| nil => simp; rfl
| cons y ys => simp_all

Result:
no goals

Proof state:
case cons.cons
a b x : Int
xs : List Int
ih : ∀ (ys : IntList), List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys
y : Int
ys : List Int
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) (x :: xs) (y :: ys) = a * (x :: xs) + b * (y :: ys)

Tactic:
simp_all

Result:
no goals

Proof state:
a : Int
xs : IntList
b : Int
ys : IntList
⊢ List.zipWithAll (fun x y => a * x.getD 0 + b * y.getD 0) xs ys = a * xs + b * ys

Tactic:
induction xs generalizing ys with
| nil => simp; rfl
| cons x xs ih =>
  cases ys with
  | nil => simp; rfl
  | cons y ys => simp_all

Result:
no goals