harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/LinearAlgebra/ExteriorAlgebra/OfAlternating.lean
theorem liftAlternating_ιMulti :
    liftAlternating (R := R) (M := M) (N := ExteriorAlgebra R M) (ιMulti R) =
    (LinearMap.id : ExteriorAlgebra R M →ₗ[R] ExteriorAlgebra R M)

Proof state:
case h.ι_mul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ : CliffordAlgebra 0
m✝ : M
hx : (liftAlternating (ιMulti R)) x✝ = x✝
⊢ (liftAlternating (ιMulti R)) ((CliffordAlgebra.ι 0) m✝ * x✝) = (CliffordAlgebra.ι 0) m✝ * x✝

Tactic:
simp_rw [liftAlternating_ι_mul, ιMulti_succ_curryLeft, liftAlternating_comp,
LinearMap.comp_apply, LinearMap.mulLeft_apply, hx]

Result:
no goals

Proof state:
case h.algebraMap
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
r✝ : R
⊢ (liftAlternating (ιMulti R)) ((algebraMap R (CliffordAlgebra 0)) r✝) = (algebraMap R (CliffordAlgebra 0)) r✝

Tactic:
rw [liftAlternating_algebraMap, ιMulti_zero_apply, Algebra.algebraMap_eq_smul_one]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ liftAlternating (ιMulti R) = LinearMap.id

Tactic:
ext v

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ExteriorAlgebra R M
⊢ (liftAlternating (ιMulti R)) v = LinearMap.id v

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ExteriorAlgebra R M
⊢ (liftAlternating (ιMulti R)) v = v

Tactic:
induction v using CliffordAlgebra.left_induction with
| algebraMap => rw [liftAlternating_algebraMap, ιMulti_zero_apply, Algebra.algebraMap_eq_smul_one]
| add _ _ hx hy => rw [map_add, hx, hy]
| ι_mul _ _ hx => simp_rw [liftAlternating_ι_mul, ιMulti_succ_curryLeft, liftAlternating_comp,
    LinearMap.comp_apply, LinearMap.mulLeft_apply, hx]

Result:
no goals

Proof state:
case h.add
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
x✝ y✝ : CliffordAlgebra 0
hx : (liftAlternating (ιMulti R)) x✝ = x✝
hy : (liftAlternating (ιMulti R)) y✝ = y✝
⊢ (liftAlternating (ιMulti R)) (x✝ + y✝) = x✝ + y✝

Tactic:
rw [map_add, hx, hy]

Result:
no goals

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ExteriorAlgebra R M
⊢ (liftAlternating (ιMulti R)) v = LinearMap.id v

Tactic:
dsimp

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v : ExteriorAlgebra R M
⊢ (liftAlternating (ιMulti R)) v = v
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem findRev?_cons_of_neg (l : Array α) (h : ¬p a) :
    findRev? p (l.push a) = findRev? p l

Proof state:
α : Type
p : α → Bool
a : α
l : Array α
h : ¬p a = true
⊢ findRev? p (l.push a) = findRev? p l

Tactic:
cases l

Result:
case mk
α : Type
p : α → Bool
a : α
h : ¬p a = true
toList✝ : List α
⊢ findRev? p ({ toList := toList✝ }.push a) = findRev? p { toList := toList✝ }

Proof state:
case mk
α : Type
p : α → Bool
a : α
h : ¬p a = true
toList✝ : List α
⊢ findRev? p ({ toList := toList✝ }.push a) = findRev? p { toList := toList✝ }

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem mem_iInf_of_directed {f : ι → Filter α} (h : Directed (· ≥ ·) f) [Nonempty ι] (s) :
    s ∈ iInf f ↔ ∃ i, s ∈ f i

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
h : Directed (fun x1 x2 => x1 ≥ x2) f
inst✝ : Nonempty ι
s : Set α
⊢ s ∈ iInf f ↔ ∃ i, s ∈ f i

Tactic:
simp only [← Filter.mem_sets, iInf_sets_eq h, mem_iUnion]

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashInvariantForms.lean
theorem slash_action_eqn' {k : ℤ} {Γ : Subgroup SL(2, ℤ)} [SlashInvariantFormClass F Γ k]
    (f : F) {γ} (hγ : γ ∈ Γ) (z : ℍ) :
    f (γ • z) = (γ 1 0 * z + γ 1 1) ^ k * f z

Proof state:
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
k : ℤ
Γ : Subgroup SL(2, ℤ)
inst✝ : SlashInvariantFormClass F Γ k
f : F
γ : SL(2, ℤ)
hγ : γ ∈ Γ
z : ℍ
⊢ f (γ • z) = (↑(↑γ 1 0) * ↑z + ↑(↑γ 1 1)) ^ k * f z

Tactic:
rw [← ModularForm.slash_action_eq'_iff, slash_action_eqn f γ hγ]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
lemma one_add_div_two_mul_two_of_odd (h : Odd n) : 1 + n / 2 * 2 = n

Proof state:
n : ℕ
h : Odd n
⊢ 1 + n / 2 * 2 = n

Tactic:
rw [← odd_iff.mp h, mod_add_div']

Result:
no goals
-- Mathlib/Data/Finset/SDiff.lean
@[simp] lemma insert_sdiff_cancel (ha : a ∉ s) : insert a s \ s = {a}

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ insert a s \ s = {a}

Tactic:
rw [insert_sdiff_of_not_mem _ ha, Finset.sdiff_self, insert_emptyc_eq]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map_map₂_distrib {n : γ → δ} {m' : α' → β' → δ} {n₁ : α → α'} {n₂ : β → β'}
    (h_distrib : ∀ a b, n (m a b) = m' (n₁ a) (n₂ b)) :
    (map₂ m f g).map n = map₂ m' (f.map n₁) (g.map n₂)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : α' → β' → δ
n₁ : α → α'
n₂ : β → β'
h_distrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ a) (n₂ b)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ f) (map n₂ g)

Tactic:
simp_rw [map_map₂, map₂_map_left, map₂_map_right, h_distrib]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem get_find?_mkArray (n : Nat) (a : α) (p : α → Bool) (h) :
    ((mkArray n a).find? p).get h = a

Proof state:
α : Type u_1
n : Nat
a : α
p : α → Bool
h : (find? p (mkArray n a)).isSome = true
⊢ (find? p (mkArray n a)).get h = a

Tactic:
simp [← List.toArray_replicate]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pred_castSucc_lt {a : Fin (n + 1)} (ha : castSucc a ≠ 0) :
    (castSucc a).pred ha < a

Proof state:
n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < a

Tactic:
rw [pred_castSucc_lt_iff, le_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Replicate.lean
theorem aux3 {a b c : Nat} (hidx : a < b * c) (h : c < n) : a < b * n

Proof state:
case h
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ ?b < b * ?c

case b
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ Nat

case c
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ Nat

Tactic:
assumption

Result:
no goals

Proof state:
case h₁
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ a < ?m

Tactic:
exact hidx

Result:
no goals

Proof state:
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ a < b * n

Tactic:
apply Nat.lt_trans

Result:
case h₁
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ a < ?m

case a
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ ?m < b * n

case m
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ Nat

Proof state:
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ 0 < b

Tactic:
apply aux1

Result:
case h
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ ?b < b * ?c

case b
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ Nat

case c
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ Nat

Proof state:
case a
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ b * c < b * n

Tactic:
apply (Nat.mul_lt_mul_left _).mpr h

Result:
n a b c : Nat
hidx : a < b * c
h : c < n
⊢ 0 < b
-- Mathlib/Data/List/ReduceOption.lean
theorem reduceOption_replicate_none {n : ℕ} : (replicate n (@none α)).reduceOption = []

Proof state:
α : Type u_1
n : ℕ
⊢ (replicate n none).reduceOption = []

Tactic:
dsimp [reduceOption]

Result:
α : Type u_1
n : ℕ
⊢ filterMap id (replicate n none) = []

Proof state:
α : Type u_1
n : ℕ
⊢ filterMap id (replicate n none) = []

Tactic:
rw [filterMap_replicate_of_none (id_def _)]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Any_def {t : RBNode α} : t.Any p ↔ ∃ x ∈ t, p x

Proof state:
α : Type u_1
p : α → Prop
t : RBNode α
⊢ Any p t ↔ ∃ x, x ∈ t ∧ p x

Tactic:
induction t <;> simp [or_and_right, exists_or, *]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem card_ne_eq [Fintype α] (a : α) [Fintype { x : α | x ≠ a }] :
    Fintype.card { x : α | x ≠ a } = Fintype.card α - 1

Proof state:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
haveI := Classical.decEq α

Result:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Proof state:
α : Type u
inst✝¹ : Fintype α
a : α
inst✝ : Fintype ↑{x | x ≠ a}
this : DecidableEq α
⊢ Fintype.card ↑{x | x ≠ a} = Fintype.card α - 1

Tactic:
rw [← toFinset_card, toFinset_setOf, Finset.filter_ne',
  Finset.card_erase_of_mem (Finset.mem_univ _), Finset.card_univ]

Result:
no goals
-- Mathlib/Data/Finset/Max.lean
theorem min_singleton {a : α} : Finset.min {a} = (a : WithTop α)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).min = ↑a

Tactic:
exact min_insert

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ {a}.min = ↑a

Tactic:
rw [← insert_emptyc_eq]

Result:
α : Type u_2
inst✝ : LinearOrder α
a : α
⊢ (insert a ∅).min = ↑a
-- Mathlib/GroupTheory/PGroup.lean
theorem nontrivial_iff_card [Finite G] : Nontrivial G ↔ ∃ n > 0, Nat.card G = p ^ n :=
  ⟨fun hGnt =>
    let ⟨k, hk⟩ := iff_card.1 hG
    ⟨k,
      Nat.pos_of_ne_zero fun hk0 => by
        rw [hk0, pow_zero] at hk; exact Finite.one_lt_card.ne' hk,
      hk⟩,
    fun ⟨_, hk0, hk⟩ =>
    Finite.one_lt_card_iff_nontrivial.1 <|
      hk.symm ▸ one_lt_pow₀ (Fact.out (p := p.Prime)).one_lt (ne_of_gt hk0)⟩

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = 1
hk0 : k = 0
⊢ False

Tactic:
exact Finite.one_lt_card.ne' hk

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = p ^ k
hk0 : k = 0
⊢ False

Tactic:
rw [hk0, pow_zero] at hk

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
hp : Fact (Nat.Prime p)
inst✝ : Finite G
hGnt : Nontrivial G
k : ℕ
hk : Nat.card G = 1
hk0 : k = 0
⊢ False
-- Mathlib/Data/Nat/Factorization/Root.lean
/-- Galois connection between `ceilRoot n : ℕ → ℕ` and `a ↦ a ^ n : ℕ → ℕ` where `ℕ` is ordered
by divisibility.

Note that this cannot possibly hold for `n = 0`, regardless of the value of `ceilRoot 0 a`, because
the statement reduces to `a = 1 ↔ ceilRoot 0 a ∣ b`, which is false for eg `a = 0`,
`b = ceilRoot 0 a`. -/
lemma dvd_pow_iff_ceilRoot_dvd (hn : n ≠ 0) : a ∣ b ^ n ↔ ceilRoot n a ∣ b

Proof state:
case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | hb := eq_or_ne b 0

Result:
case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0

case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Proof state:
case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

Tactic:
aesop

Result:
no goals

Proof state:
case inr.inl
a n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ 0 ^ n ↔ n.ceilRoot a ∣ 0

Tactic:
simp [hn]

Result:
no goals

Proof state:
a b n : ℕ
hn : n ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
obtain rfl | ha := eq_or_ne a 0

Result:
case inl
b n : ℕ
hn : n ≠ 0
⊢ 0 ∣ b ^ n ↔ n.ceilRoot 0 ∣ b

case inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Proof state:
case inr.inr
a b n : ℕ
hn : n ≠ 0
ha : a ≠ 0
hb : b ≠ 0
⊢ a ∣ b ^ n ↔ n.ceilRoot a ∣ b

Tactic:
rw [← factorization_le_iff_dvd ha (pow_ne_zero _ hb),
  ← factorization_le_iff_dvd (ceilRoot_ne_zero.2 ⟨hn, ha⟩) hb, factorization_pow,
  factorization_ceilRoot, ceilDiv_le_iff_le_smul (β := ℕ →₀ ℕ) (pos_iff_ne_zero.2 hn)]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_mul_one : ball 1 δ * s = thickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
⊢ ball 1 δ * s = thickening δ s

Tactic:
rw [mul_comm, mul_ball_one]

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem ker_pow_le_ker_pow_finrank [FiniteDimensional K V] (f : End K V) (m : ℕ) :
    LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Proof state:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)

Tactic:
apply LinearMap.ker_le_ker_comp

Result:
no goals

Proof state:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
rw [← add_tsub_cancel_of_le (Nat.le_of_lt h_cases), add_comm, pow_add]

Result:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ (finrank K V - m) * f ^ m)

Proof state:
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : ¬m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
rw [ker_pow_eq_ker_pow_finrank_of_le (le_of_not_lt h_cases)]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

Tactic:
by_cases h_cases : m < finrank K V

Result:
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
m : ℕ
h_cases : ¬m < finrank K V
⊢ LinearMap.ker (f ^ m) ≤ LinearMap.ker (f ^ finrank K V)
-- Mathlib/Analysis/Convex/EGauge.lean
@[simp]
lemma egauge_zero_right (hs : s.Nonempty) : egauge 𝕜 s 0 = 0

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ egauge 𝕜 s 0 = 0

Tactic:
have : 0 ∈ (0 : 𝕜) • s := by simp [zero_smul_set hs]

Result:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : s.Nonempty
this : 0 ∈ 0 • s
⊢ egauge 𝕜 s 0 = 0

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : s.Nonempty
this : 0 ∈ 0 • s
⊢ egauge 𝕜 s 0 = 0

Tactic:
simpa using egauge_le_of_mem_smul this

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NormedDivisionRing 𝕜
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
hs : s.Nonempty
⊢ 0 ∈ 0 • s

Tactic:
simp [zero_smul_set hs]

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isIso₃_of_isIso₁₂ {T T' : Triangle C} (φ : T ⟶ T') (hT : T ∈ distTriang C)
    (hT' : T' ∈ distTriang C) (h₁ : IsIso φ.hom₁) (h₂ : IsIso φ.hom₂) : IsIso φ.hom₃ :=
  isIso₂_of_isIso₁₃ ((rotate C).map φ) (rot_of_distTriang _ hT)
    (rot_of_distTriang _ hT') h₂ (by dsimp; infer_instance)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
⊢ IsIso ((rotate C).map φ).hom₃

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
⊢ IsIso ((shiftFunctor C 1).map φ.hom₁)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T T' : Triangle C
φ : T ⟶ T'
hT : T ∈ distinguishedTriangles
hT' : T' ∈ distinguishedTriangles
h₁ : IsIso φ.hom₁
h₂ : IsIso φ.hom₂
⊢ IsIso ((shiftFunctor C 1).map φ.hom₁)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem Continuous.range_subset_closure_image_dense {f : X → Y} (hf : Continuous f)
    (hs : Dense s) : range f ⊆ closure (f '' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous f
hs : Dense s
⊢ range f ⊆ closure (f '' s)

Tactic:
rw [← image_univ, ← hs.closure_eq]

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous f
hs : Dense s
⊢ f '' closure s ⊆ closure (f '' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set X
f : X → Y
hf : Continuous f
hs : Dense s
⊢ f '' closure s ⊆ closure (f '' s)

Tactic:
exact image_closure_subset_closure_image hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem size_range' {start size step} : (range' start size step).size = size

Proof state:
start size step : Nat
⊢ (range' start size step).size = size

Tactic:
simp [range']

Result:
no goals
-- Mathlib/Data/Set/Function.lean
lemma InjOn.image_ssubset_image_iff (h : s.InjOn f) (h₁ : s₁ ⊆ s) (h₂ : s₂ ⊆ s) :
    f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Proof state:
α : Type u_1
β : Type u_2
s s₁ s₂ : Set α
f : α → β
h : InjOn f s
h₁ : s₁ ⊆ s
h₂ : s₂ ⊆ s
⊢ f '' s₁ ⊂ f '' s₂ ↔ s₁ ⊂ s₂

Tactic:
simp_rw [ssubset_def, h.image_subset_image_iff h₁ h₂, h.image_subset_image_iff h₂ h₁]

Result:
no goals
-- Mathlib/NumberTheory/SmoothNumbers.lean
/-- If `p ∉ s` is a prime and `n` is `s`-factored, then `p` and `n` are coprime. -/
lemma Prime.factoredNumbers_coprime {s : Finset ℕ} {p n : ℕ} (hp : p.Prime) (hs : p ∉ s)
    (hn : n ∈ factoredNumbers s) :
    Nat.Coprime p n

Proof state:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p.Coprime n

Tactic:
rw [hp.coprime_iff_not_dvd, ← mem_primeFactorsList_iff_dvd hn.1 hp]

Result:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Proof state:
s : Finset ℕ
p n : ℕ
hp : Prime p
hs : p ∉ s
hn : n ∈ factoredNumbers s
⊢ p ∉ n.primeFactorsList

Tactic:
exact fun H ↦ hs <| hn.2 p H

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem map_single_le_powerset (s : Multiset α) : s.map singleton ≤ powerset s :=
  Quotient.inductionOn s fun l => by
    simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]
    show l.map (((↑) : List α → Multiset α) ∘ pure) <+~ (sublists l).map (↑)
    rw [← List.map_map]
    exact ((map_pure_sublist_sublists _).map _).subperm

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ map singleton ⟦l⟧ ≤ powerset ⟦l⟧

Tactic:
simp only [powerset_coe, quot_mk_to_coe, coe_le, map_coe]

Result:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList l.sublists

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists

Tactic:
rw [← List.map_map]

Result:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map pure l) <+~ List.map ofList l.sublists

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map ofList (List.map pure l) <+~ List.map ofList l.sublists

Tactic:
exact ((map_pure_sublist_sublists _).map _).subperm

Result:
no goals

Proof state:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map singleton l <+~ List.map ofList l.sublists

Tactic:
show l.map (((↑) : List α → Multiset α) ∘ pure) <+~ (sublists l).map (↑)

Result:
α : Type u_1
s : Multiset α
l : List α
⊢ List.map (ofList ∘ pure) l <+~ List.map ofList l.sublists
-- Mathlib/SetTheory/ZFC/Rank.lean
theorem rank_sUnion_le (x : PSet) : rank (⋃₀ x) ≤ rank x

Proof state:
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank

Tactic:
trans <;> apply rank_lt_of_mem <;> assumption

Result:
no goals

Proof state:
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank

Tactic:
intro _ ⟨_, _, _⟩

Result:
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < x.rank

Proof state:
x : PSet.{u_1}
⊢ (⋃₀ x).rank ≤ x.rank

Tactic:
simp_rw [rank_le_iff, mem_sUnion]

Result:
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, (∃ z ∈ x, y ∈ z) → y.rank < x.rank
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma pOpcycles_opcyclesIsoSc'_inv :
    (K.sc' i j k).pOpcycles ≫ (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).pOpcycles ≫ (K.opcyclesIsoSc' i j k hi hk).inv = K.pOpcycles j

Tactic:
dsimp [opcyclesIsoSc']

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).pOpcycles ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) = K.pOpcycles j

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc j).pOpcycles = K.pOpcycles j

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc' i j k).pOpcycles ≫ ShortComplex.opcyclesMap ((natIsoSc' C c i j k hi hk).inv.app K) = K.pOpcycles j

Tactic:
simp only [ShortComplex.p_opcyclesMap, shortComplexFunctor'_obj_X₂, shortComplexFunctor_obj_X₂,
  natIsoSc'_inv_app_τ₂, id_comp]

Result:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ (K.sc j).pOpcycles = K.pOpcycles j
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem isClosed_polar (s : Set E) : IsClosed (polar 𝕜 s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ x ∈ s, {y | ‖((dualPairing 𝕜 E) y) x‖ ≤ 1})

Tactic:
refine isClosed_biInter fun z _ => ?_

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖((dualPairing 𝕜 E) y) z‖ ≤ 1}

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (polar 𝕜 s)

Tactic:
dsimp only [NormedSpace.polar]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed ((dualPairing 𝕜 E).flip.polar s)

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed ((dualPairing 𝕜 E).flip.polar s)

Tactic:
simp only [LinearMap.polar_eq_iInter, LinearMap.flip_apply]

Result:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
⊢ IsClosed (⋂ x ∈ s, {y | ‖((dualPairing 𝕜 E) y) x‖ ≤ 1})

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
s : Set E
z : E
x✝ : z ∈ s
⊢ IsClosed {y | ‖((dualPairing 𝕜 E) y) z‖ ≤ 1}

Tactic:
exact isClosed_Iic.preimage (ContinuousLinearMap.apply 𝕜 𝕜 z).continuous.norm

Result:
no goals