harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem nhds_eq_inf_comap {z : Z} (hz : z ∈ e.source) :
    𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ e) (𝓝 (e z).2)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)

Tactic:
rw [le_inf_iff, ← tendsto_iff_comap, ← tendsto_iff_comap]

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ ↑e) l (𝓝 (↑e z).2)

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ Tendsto proj l (𝓝 (proj z)) ∧ Tendsto (Prod.snd ∘ ↑e) l (𝓝 (↑e z).2)

Tactic:
exact e.tendsto_nhds_iff hz

Result:
no goals

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
⊢ 𝓝 z = comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)

Tactic:
refine eq_of_forall_le_iff fun l ↦ ?_

Result:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝² : TopologicalSpace B
inst✝¹ : TopologicalSpace F
proj : Z → B
inst✝ : TopologicalSpace Z
e : Trivialization F proj
z : Z
hz : z ∈ e.source
l : Filter Z
⊢ l ≤ 𝓝 z ↔ l ≤ comap proj (𝓝 (proj z)) ⊓ comap (Prod.snd ∘ ↑e) (𝓝 (↑e z).2)
-- Mathlib/Topology/EMetricSpace/Diam.lean
theorem diam_le_iff {d : ℝ≥0∞} : diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Proof state:
α : Type u_1
s : Set α
inst✝ : PseudoEMetricSpace α
d : ℝ≥0∞
⊢ diam s ≤ d ↔ ∀ x ∈ s, ∀ y ∈ s, edist x y ≤ d

Tactic:
simp only [diam, iSup_le_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualAnnihilator_inf_eq (W W' : Subspace K V₁) :
    (W ⊓ W').dualAnnihilator = W.dualAnnihilator ⊔ W'.dualAnnihilator

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ LinearMap.range F.dualMap ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ LinearMap.range F.dualMap ≤ dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
intro φ

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ LinearMap.range F.dualMap → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := (mkQ W).prod (mkQ W')
⊢ LinearMap.ker F = W ⊓ W'

Tactic:
simp only [F, LinearMap.ker_prod, ker_mkQ]

Result:
no goals

Proof state:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'

Tactic:
refine le_antisymm ?_ (sup_dualAnnihilator_le_inf W W')

Result:
K : Type uK
inst✝² : Field K
V₁ : Type uV₁
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
-- Mathlib/NumberTheory/Cyclotomic/Basic.lean
theorem finite [IsDomain B] [h₁ : Finite S] [h₂ : IsCyclotomicExtension S A B] :
    Module.Finite A B

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₁ : Finite ↑S
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B

Tactic:
rw [finite_coe_iff] at h₁

Result:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₁ : S.Finite
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B

Proof state:
S : Set ℕ+
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₁ : S.Finite
h₂ : IsCyclotomicExtension S A B
⊢ Module.Finite A B

Tactic:
induction S, h₁ using Set.Finite.induction_on generalizing h₂ A B with
| empty =>
  refine Module.finite_def.2 ⟨({1} : Finset B), ?_⟩
  simp [← top_toSubmodule, ← empty, toSubmodule_bot, Submodule.one_eq_span]
| @insert n S _ _ H =>
  haveI : IsCyclotomicExtension S A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) :=
    union_left _ (insert n S) _ _ (subset_insert n S)
  haveI := H A (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1})
  have : Module.Finite (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) B := by
    rw [← union_singleton] at h₂
    let _ := union_right S {n} A B
    exact finite_of_singleton n _ _
  exact Module.Finite.trans (adjoin A {b : B | ∃ n : ℕ+, n ∈ S ∧ b ^ (n : ℕ) = 1}) _

Result:
no goals

Proof state:
S✝ : Set ℕ+
n : ℕ+
S : Set ℕ+
a✝ : n ∉ S
hs✝ : S.Finite
H :
  ∀ (A : Type u) (B : Type v) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain B]
    [h₂ : IsCyclotomicExtension S A B], Module.Finite A B
A : Type u
B : Type v
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : Algebra A B
inst✝ : IsDomain B
h₂ : IsCyclotomicExtension (S ∪ {n}) A B
this✝ : IsCyclotomicExtension S A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
this : Module.Finite A ↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})
x✝ : IsCyclotomicExtension {n} (↥(adjoin A {b | ∃ a ∈ S, b ^ ↑a = 1})) B := union_right S {n} A B
⊢ Module.Finite (↥(adjoin A {b | ∃ n ∈ S, b ^ ↑n = 1})) B

Tactic:
exact finite_of_singleton n _ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem pred_succ (i : Fin n) {h : i.succ ≠ 0} : i.succ.pred h = i

Proof state:
case mk
n val✝ : Nat
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩.succ ≠ 0
⊢ ⟨val✝, isLt✝⟩.succ.pred h = ⟨val✝, isLt✝⟩

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
i : Fin n
h : i.succ ≠ 0
⊢ i.succ.pred h = i

Tactic:
cases i

Result:
case mk
n val✝ : Nat
isLt✝ : val✝ < n
h : ⟨val✝, isLt✝⟩.succ ≠ 0
⊢ ⟨val✝, isLt✝⟩.succ.pred h = ⟨val✝, isLt✝⟩
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_comp (k l : ℕ) :
    (@hasseDeriv R _ k).comp (hasseDeriv l) = (k + l).choose k • hasseDeriv (k + l)

Proof state:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) (↑((i - l).choose k) * ↑(i.choose l)) =
    (monomial (i - (k + l))) ((k + l).choose k • ↑(i.choose (k + l)))

Tactic:
rw_mod_cast [nsmul_eq_mul]

Result:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) (↑((k + l).choose k) * ↑(i.choose (k + l)))

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! / (↑k ! * ↑(i - l - k)!) * (↑i ! / (↑l ! * ↑(i - l)!)) =
    ↑(k + l)! / (↑k ! * ↑l !) * (↑i ! / (↑(k + l)! * ↑(i - l - k)!))

Tactic:
field_simp

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑(i - l)! * ↑i ! * (↑k ! * ↑l ! * (↑(k + l)! * ↑(i - l - k)!)) =
    ↑(k + l)! * ↑i ! * (↑k ! * ↑(i - l - k)! * (↑l ! * ↑(i - l)!))

Proof state:
case h.h
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (monomial (i - (k + l))) ↑((i - l).choose k * i.choose l) =
    (monomial (i - (k + l))) ↑((k + l).choose k * i.choose (k + l))

Tactic:
congr 2

Result:
case h.h.h.e_6.h.e_a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
⊢ (i - l).choose k * i.choose l = (k + l).choose k * i.choose (k + l)

Proof state:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : ¬i < l
⊢ (i - l).choose k * i.choose l = 0

Tactic:
push_neg at hil

Result:
case neg
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : i < k + l
hil : l ≤ i
⊢ (i - l).choose k * i.choose l = 0

Proof state:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑((i - l).choose k * i.choose l) = ↑((k + l).choose k * i.choose (k + l))

Tactic:
push_cast

Result:
case neg.a
R : Type u_1
inst✝ : Semiring R
k l i : ℕ
hikl : k + l ≤ i
h1 : l ≤ i
h2 : k ≤ i - l
h3 : k ≤ k + l
⊢ ↑((i - l).choose k) * ↑(i.choose l) = ↑((k + l).choose k) * ↑(i.choose (k + l))
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_sub_mul (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (d - c * x)) = c⁻¹ • ∫ x in d - c * b..d - c * a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x

Tactic:
simp only [sub_eq_add_neg, neg_mul_eq_neg_mul]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + -c * x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + -c * x) = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Tactic:
rw [integral_comp_add_mul f (neg_ne_zero.mpr hc) d, integral_symm]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ (-c)⁻¹ • -∫ (x : ℝ) in d + -c * b..d + -c * a, f x = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ (-c)⁻¹ • -∫ (x : ℝ) in d + -c * b..d + -c * a, f x = c⁻¹ • ∫ (x : ℝ) in d + -c * b..d + -c * a, f x

Tactic:
simp only [inv_neg, smul_neg, neg_neg, neg_smul]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem factors_spec (a : R) (h : a ≠ 0) :
    (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧
    Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a

Tactic:
rw [dif_neg h]

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ Classical.choose ⋯, Irreducible b) ∧ Associated (Classical.choose ⋯).prod a

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ Classical.choose ⋯, Irreducible b) ∧ Associated (Classical.choose ⋯).prod a

Tactic:
exact Classical.choose_spec (WfDvdMonoid.exists_factors a h)

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ factors a, Irreducible b) ∧ Associated (factors a).prod a

Tactic:
unfold factors

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
a : R
h : a ≠ 0
⊢ (∀ b ∈ if h : a = 0 then ∅ else Classical.choose ⋯, Irreducible b) ∧
    Associated (if h : a = 0 then ∅ else Classical.choose ⋯).prod a
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem leibniz_of_mul_eq_one {a b : A} (h : a * b = 1) : D a = -a ^ 2 • D b

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a = -(a ^ 2 • D b)

Tactic:
refine eq_neg_of_add_eq_zero_left ?_

Result:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a + a ^ 2 • D b = 0

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a + a ^ 2 • D b = 0

Tactic:
calc
  D a + a ^ 2 • D b = a • b • D a + a • a • D b := by simp only [smul_smul, h, one_smul, sq]
  _ = a • D (a * b) := by rw [leibniz, smul_add, add_comm]
  _ = 0 := by rw [h, map_one_eq_zero, smul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • D (a * b) = 0

Tactic:
rw [h, map_one_eq_zero, smul_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ a • b • D a + a • a • D b = a • D (a * b)

Tactic:
rw [leibniz, smul_add, add_comm]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a = -a ^ 2 • D b

Tactic:
rw [neg_smul]

Result:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a = -(a ^ 2 • D b)

Proof state:
R : Type u_1
inst✝⁵ : CommRing R
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
M : Type u_3
inst✝² : AddCommGroup M
inst✝¹ : Module A M
inst✝ : Module R M
D : Derivation R A M
a b : A
h : a * b = 1
⊢ D a + a ^ 2 • D b = a • b • D a + a • a • D b

Tactic:
simp only [smul_smul, h, one_smul, sq]

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem get_even : ∀ (n : ℕ) (s : Stream' α), get (even s) n = get s (2 * n)
  | 0, _ => rfl
  | succ n, s => by
    change get (even s) (succ n) = get s (succ (succ (2 * n)))
    rw [get_succ, get_succ, tail_even, get_even n]; rfl

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n).succ.succ

Tactic:
rw [get_succ, get_succ, tail_even, get_even n]

Result:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ s.tail.tail.get (2 * n) = s.tail.get (2 * n + 1)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n.succ)

Tactic:
change get (even s) (succ n) = get s (succ (succ (2 * n)))

Result:
α : Type u
n : ℕ
s : Stream' α
⊢ s.even.get n.succ = s.get (2 * n).succ.succ
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem lowerBound?_le' {t : RBNode α} (H : ∀ {x}, x ∈ lb → cut x ≠ .lt) :
    t.lowerBound? cut lb = some x → cut x ≠ .lt

Proof state:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
x✝ : α
h : x✝ ∈ lb
⊢ (cut x✝).swap ≠ Ordering.gt

Tactic:
specialize H h

Result:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
x✝ : α
h : x✝ ∈ lb
H : cut x✝ ≠ Ordering.lt
⊢ (cut x✝).swap ≠ Ordering.gt

Proof state:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
x✝ : α
h : x✝ ∈ lb
H : cut x✝ ≠ Ordering.lt
⊢ (cut x✝).swap ≠ Ordering.gt

Tactic:
rwa [Ne, ← Ordering.swap_inj] at H

Result:
no goals

Proof state:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ lowerBound? cut t lb = some x → cut x ≠ Ordering.lt

Tactic:
rw [← reverse_reverse t, lowerBound?_reverse, Ne, ← Ordering.swap_inj]

Result:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x → ¬(cut x).swap = Ordering.lt.swap

Proof state:
α : Type u_1
lb : Option α
cut : α → Ordering
x : α
t : RBNode α
H : ∀ {x : α}, x ∈ lb → cut x ≠ Ordering.lt
⊢ upperBound? (fun x => (cut x).swap) t.reverse lb = some x → ¬(cut x).swap = Ordering.lt.swap

Tactic:
exact upperBound?_ge' fun h => by specialize H h; rwa [Ne, ← Ordering.swap_inj] at H

Result:
no goals
-- Mathlib/SetTheory/Descriptive/Tree.lean
@[simp] lemma tree_eq_bot : T = ⊥ ↔ [] ∉ T where
  mp

Proof state:
A : Type u_1
T : ↥(tree A)
⊢ T = ⊥ → [] ∉ T

Tactic:
rintro rfl

Result:
A : Type u_1
⊢ [] ∉ ⊥

Proof state:
A : Type u_1
⊢ [] ∉ ⊥

Tactic:
simp

Result:
no goals

Proof state:
case h
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∈ T ↔ x ∈ ⊥

Tactic:
simpa using fun h' ↦ h <| mem_of_prefix x.nil_prefix h'

Result:
no goals

Proof state:
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
⊢ T = ⊥

Tactic:
ext x

Result:
case h
A : Type u_1
T : ↥(tree A)
h : [] ∉ T
x : List A
⊢ x ∈ T ↔ x ∈ ⊥
-- Mathlib/LinearAlgebra/Multilinear/Basis.lean
theorem Basis.ext_multilinear [Finite ι] {f g : MultilinearMap R (fun _ : ι => M₂) M₃} {ι₁ : Type*}
    (e : Basis ι₁ R M₂) (h : ∀ v : ι → ι₁, (f fun i => e (v i)) = g fun i => e (v i)) : f = g

Proof state:
case intro
R : Type u_1
ι : Type u_2
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Finite ι
f g : MultilinearMap R (fun x => M₂) M₃
ι₁ : Type u_6
e : Basis ι₁ R M₂
h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)
val✝ : Fintype ι
⊢ f = g

Tactic:
exact
  (domDomCongr_eq_iff (Fintype.equivFin ι) f g).mp
    (Basis.ext_multilinear_fin (fun _ => e) fun i => h (i ∘ _))

Result:
no goals

Proof state:
R : Type u_1
ι : Type u_2
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Finite ι
f g : MultilinearMap R (fun x => M₂) M₃
ι₁ : Type u_6
e : Basis ι₁ R M₂
h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)
⊢ f = g

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type u_1
ι : Type u_2
M₂ : Type u_4
M₃ : Type u_5
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M₂
inst✝¹ : Module R M₃
inst✝ : Finite ι
f g : MultilinearMap R (fun x => M₂) M₃
ι₁ : Type u_6
e : Basis ι₁ R M₂
h : ∀ (v : ι → ι₁), (f fun i => e (v i)) = g fun i => e (v i)
val✝ : Fintype ι
⊢ f = g
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem rightDistributor_inv {J : Type} [Fintype J] (f : J → C) (X : C) :
    (rightDistributor f X).inv = ∑ j : J, biproduct.π _ j ≫ (biproduct.ι f j ▷ X)

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).inv = ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Tactic:
ext

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.ι (fun j => f j ⊗ X) j✝ ≫ biproduct.desc fun j => biproduct.ι f j ▷ X) =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Tactic:
simp only [biproduct.ι_desc, Preadditive.comp_sum, ne_eq, biproduct.ι_π_assoc, dite_comp,
  zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
⊢ (rightDistributor f X).inv = ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Tactic:
classical
ext
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]
simp only [biproduct.ι_desc, Preadditive.comp_sum, ne_eq, biproduct.ι_π_assoc, dite_comp,
  zero_comp, Finset.sum_dite_eq, Finset.mem_univ, eqToHom_refl, Category.id_comp, ite_true]

Result:
no goals

Proof state:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ biproduct.ι (fun j => f j ⊗ X) j✝ ≫ (rightDistributor f X).inv =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X

Tactic:
dsimp [rightDistributor, Functor.mapBiproduct, Functor.mapBicone]

Result:
case w
C : Type u_1
inst✝⁵ : Category.{u_2, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : MonoidalCategory C
inst✝² : MonoidalPreadditive C
inst✝¹ : HasFiniteBiproducts C
J : Type
inst✝ : Fintype J
f : J → C
X : C
j✝ : J
⊢ (biproduct.ι (fun j => f j ⊗ X) j✝ ≫ biproduct.desc fun j => biproduct.ι f j ▷ X) =
    biproduct.ι (fun j => f j ⊗ X) j✝ ≫ ∑ j : J, biproduct.π (fun j => f j ⊗ X) j ≫ biproduct.ι f j ▷ X
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem image2_subset_map₂ (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    Set.image2 (fun m n => f m n) (↑p : Set M) (↑q : Set N) ⊆ (↑(map₂ f p q) : Set P)

Proof state:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
i : M
hi : i ∈ ↑p
j : N
hj : j ∈ ↑q
⊢ (fun m n => (f m) n) i j ∈ ↑(map₂ f p q)

Tactic:
exact apply_mem_map₂ _ hi hj

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ image2 (fun m n => (f m) n) ↑p ↑q ⊆ ↑(map₂ f p q)

Tactic:
rintro _ ⟨i, hi, j, hj, rfl⟩

Result:
case intro.intro.intro.intro
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
i : M
hi : i ∈ ↑p
j : N
hj : j ∈ ↑q
⊢ (fun m n => (f m) n) i j ∈ ↑(map₂ f p q)