harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Category/ModuleCat/Sheaf/Free.lean
@[simp]
lemma freeHomEquiv_freeMap :
    (freeHomEquiv _ (freeMap (R := R) f)) = freeSection.comp f :=
  (freeHomEquiv _).symm.injective (by simp; rfl)

Proof state:
C : Type u'
inst✝³ : Category.{v', u'} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝² : HasWeakSheafify J✝ AddCommGrp
inst✝¹ : J✝.WEqualsLocallyBijective AddCommGrp
inst✝ : J✝.HasSheafCompose (forget₂ RingCat AddCommGrp)
I J : Type u
f : I → J
⊢ (free J).freeHomEquiv.symm ((free J).freeHomEquiv (freeMap f)) = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
simp

Result:
C : Type u'
inst✝³ : Category.{v', u'} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝² : HasWeakSheafify J✝ AddCommGrp
inst✝¹ : J✝.WEqualsLocallyBijective AddCommGrp
inst✝ : J✝.HasSheafCompose (forget₂ RingCat AddCommGrp)
I J : Type u
f : I → J
⊢ freeMap f = (free J).freeHomEquiv.symm (freeSection ∘ f)

Proof state:
C : Type u'
inst✝³ : Category.{v', u'} C
J✝ : GrothendieckTopology C
R : Sheaf J✝ RingCat
inst✝² : HasWeakSheafify J✝ AddCommGrp
inst✝¹ : J✝.WEqualsLocallyBijective AddCommGrp
inst✝ : J✝.HasSheafCompose (forget₂ RingCat AddCommGrp)
I J : Type u
f : I → J
⊢ freeMap f = (free J).freeHomEquiv.symm (freeSection ∘ f)

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem zipWithAll_map_right (l₁ : List α) (l₂ : List β) (f : β → β') (g : Option α → Option β' → γ) :
    zipWithAll g l₁ (l₂.map f) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂

Proof state:
α : Type u_1
β β' : Type u_2
γ : Type u_3
l₁ : List α
l₂ : List β
f : β → β'
g : Option α → Option β' → γ
⊢ zipWithAll g l₁ (map f l₂) = zipWithAll (fun a b => g a (f <$> b)) l₁ l₂

Tactic:
induction l₁ generalizing l₂ <;> cases l₂ <;> simp_all

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem isMultiplicative_one [MonoidWithZero R] : IsMultiplicative (1 : ArithmeticFunction R) :=
  IsMultiplicative.iff_ne_zero.2
    ⟨by simp, by
      intro m n hm _hn hmn
      rcases eq_or_ne m 1 with (rfl | hm')
      · simp
      rw [one_apply_ne, one_apply_ne hm', zero_mul]
      rw [Ne, mul_eq_one, not_and_or]
      exact Or.inl hm'⟩

Proof state:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
rw [one_apply_ne, one_apply_ne hm', zero_mul]

Result:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ m * n ≠ 1

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ 1 1 = 1

Tactic:
simp

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ m * n ≠ 1

Tactic:
rw [Ne, mul_eq_one, not_and_or]

Result:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ ¬m = 1 ∨ ¬n = 1

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
⊢ ∀ {m n : ℕ}, m ≠ 0 → n ≠ 0 → m.Coprime n → 1 (m * n) = 1 m * 1 n

Tactic:
intro m n hm _hn hmn

Result:
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
⊢ 1 (m * n) = 1 m * 1 n

Proof state:
case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ ¬m = 1 ∨ ¬n = 1

Tactic:
exact Or.inl hm'

Result:
no goals

Proof state:
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
⊢ 1 (m * n) = 1 m * 1 n

Tactic:
rcases eq_or_ne m 1 with (rfl | hm')

Result:
case inl
R : Type u_1
inst✝ : MonoidWithZero R
n : ℕ
_hn : n ≠ 0
hm : 1 ≠ 0
hmn : Coprime 1 n
⊢ 1 (1 * n) = 1 1 * 1 n

case inr
R : Type u_1
inst✝ : MonoidWithZero R
m n : ℕ
hm : m ≠ 0
_hn : n ≠ 0
hmn : m.Coprime n
hm' : m ≠ 1
⊢ 1 (m * n) = 1 m * 1 n

Proof state:
case inl
R : Type u_1
inst✝ : MonoidWithZero R
n : ℕ
_hn : n ≠ 0
hm : 1 ≠ 0
hmn : Coprime 1 n
⊢ 1 (1 * n) = 1 1 * 1 n

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem edist_ne_top_of_mem_ball {a : β} {r : ℝ≥0∞} (x y : ball a r) : edist x.1 y.1 ≠ ∞ :=
  ne_of_lt <|
    calc
      edist x y ≤ edist a x + edist a y := edist_triangle_left x.1 y.1 a
      _ < r + r

Proof state:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(EMetric.ball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r

Tactic:
exact ENNReal.add_lt_add x.2 y.2

Result:
no goals

Proof state:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(EMetric.ball a r)
⊢ edist a ↑x + edist a ↑y < r + r

Tactic:
rw [edist_comm a x, edist_comm a y]

Result:
β : Type u_2
inst✝ : EMetricSpace β
a : β
r : ℝ≥0∞
x y : ↑(EMetric.ball a r)
⊢ edist (↑x) a + edist (↑y) a < r + r
-- Mathlib/Algebra/RingQuot.lean
theorem Rel.smul {r : A → A → Prop} (k : S) ⦃a b : A⦄ (h : Rel r a b) : Rel r (k • a) (k • b)

Proof state:
S : Type uS
inst✝² : CommSemiring S
A : Type uA
inst✝¹ : Semiring A
inst✝ : Algebra S A
r : A → A → Prop
k : S
a b : A
h : Rel r a b
⊢ Rel r (k • a) (k • b)

Tactic:
simp only [Algebra.smul_def, Rel.mul_right h]

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_series_eq_zero [Nontrivial E] : ofScalars E c = 0 ↔ c = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : Nontrivial E
⊢ ofScalars E c = 0 ↔ c = 0

Tactic:
simp [FormalMultilinearSeries.ext_iff, funext_iff]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem two_mul_arctan_inv_2_sub_arctan_inv_7 : 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4

Proof state:
⊢ 2 * arctan 2⁻¹ - arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, ← arctan_one, sub_eq_iff_eq_add, arctan_add] <;> norm_num

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
theorem toFinset_bitIndices_twoPowSum (s : Finset ℕ) :
    (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

Proof state:
s : Finset ℕ
⊢ (∑ i ∈ s, 2 ^ i).bitIndices.toFinset = s

Tactic:
simp [← (geomSum_injective rfl.le).eq_iff, List.sum_toFinset _ Nat.bitIndices_sorted.nodup]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem two_pow_pred_add_two_pow_pred (h : 0 < w) :
    2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ w

Tactic:
rw [← Nat.pow_pred_mul h]

Result:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ (w - 1) * 2

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) + 2 ^ (w - 1) = 2 ^ (w - 1) * 2

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem pow_sub_lt_descFactorial' {n : ℕ} :
    ∀ {k : ℕ}, k + 2 ≤ n → (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)
  | 0, h => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]
    exact Nat.mul_lt_mul_of_pos_left (by omega) (Nat.sub_pos_of_lt h)
  | k + 1, h => by
    rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]
    refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)
    refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_
    rw [succ_sub_succ]
    exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

Proof state:
n : ℕ
h : 0 + 2 ≤ n
⊢ n - (0 + 1) < n

Tactic:
omega

Result:
no goals

Proof state:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
rw [succ_sub_succ]

Result:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Proof state:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
refine Nat.lt_of_le_of_lt (Nat.pow_le_pow_left (Nat.sub_le_sub_right n.le_succ _) _) ?_

Result:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n.succ - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Proof state:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)

Tactic:
refine Nat.mul_lt_mul_of_pos_left ?_ (Nat.sub_pos_of_lt h)

Result:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Proof state:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) ^ (0 + 2) < n.descFactorial (0 + 2)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.pow_one, descFactorial_one]

Result:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n

Proof state:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1)) ^ (k + 2) < n.descFactorial (k + 2)

Tactic:
exact pow_sub_lt_descFactorial' (Nat.le_trans (le_succ _) h)

Result:
no goals

Proof state:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) ^ (k + 1 + 2) < n.descFactorial (k + 1 + 2)

Tactic:
rw [descFactorial_succ, Nat.pow_succ, Nat.mul_comm]

Result:
n k : ℕ
h : k + 1 + 2 ≤ n
⊢ (n - (k + 1 + 1)) * (n - (k + 1 + 1)) ^ (k + 2) < (n - (k + 2)) * n.descFactorial (k + 2)

Proof state:
n : ℕ
h : 0 + 2 ≤ n
⊢ (n - (0 + 1)) * (n - (0 + 1)) < (n - 1) * n

Tactic:
exact Nat.mul_lt_mul_of_pos_left (by omega) (Nat.sub_pos_of_lt h)

Result:
no goals
-- Mathlib/Topology/Instances/Real/Lemmas.lean
theorem Periodic.compact_of_continuous [TopologicalSpace α] {f : ℝ → α} {c : ℝ} (hp : Periodic f c)
    (hc : c ≠ 0) (hf : Continuous f) : IsCompact (range f)

Proof state:
α : Type u
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (range f)

Tactic:
rw [← hp.image_uIcc hc 0]

Result:
α : Type u
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (f '' [[0, 0 + c]])

Proof state:
α : Type u
inst✝ : TopologicalSpace α
f : ℝ → α
c : ℝ
hp : Periodic f c
hc : c ≠ 0
hf : Continuous f
⊢ IsCompact (f '' [[0, 0 + c]])

Tactic:
exact isCompact_uIcc.image hf

Result:
no goals
-- Mathlib/LinearAlgebra/InvariantBasisNumber.lean
theorem strongRankCondition_iff_succ :
    StrongRankCondition R ↔
      ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Function.Injective f

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
⊢ n ≤ m

Tactic:
by_contra H

Result:
case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
H : ¬n ≤ m
⊢ False

Proof state:
case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
this : StrongRankCondition R := h
⊢ False

Tactic:
exact Nat.not_succ_le_self n (le_of_fin_injective R f hf)

Result:
no goals

Proof state:
case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
⊢ False

Tactic:
letI : StrongRankCondition R := h

Result:
case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
this : StrongRankCondition R := h
⊢ False

Proof state:
R : Type u
inst✝ : Semiring R
⊢ StrongRankCondition R ↔ ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f

Tactic:
refine ⟨fun h n => fun f hf => ?_, fun h => ⟨@fun n m f hf => ?_⟩⟩

Result:
case refine_1
R : Type u
inst✝ : Semiring R
h : StrongRankCondition R
n : ℕ
f : (Fin (n + 1) → R) →ₗ[R] Fin n → R
hf : Injective ⇑f
⊢ False

case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
⊢ n ≤ m

Proof state:
case refine_2
R : Type u
inst✝ : Semiring R
h : ∀ (n : ℕ) (f : (Fin (n + 1) → R) →ₗ[R] Fin n → R), ¬Injective ⇑f
n m : ℕ
f : (Fin n → R) →ₗ[R] Fin m → R
hf : Injective ⇑f
H : ¬n ≤ m
⊢ False

Tactic:
exact
  h m (f.comp (Function.ExtendByZero.linearMap R (Fin.castLE (not_le.1 H))))
    (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem reduce_isSpecial : ∀ u : XgcdType, u.IsSpecial → u.reduce.IsSpecial
  | u =>
    dite (u.r = 0)
      (fun h hs => by
        rw [reduce_a h]
        exact u.finish_isSpecial hs)
      fun h hs => by
      have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h
      rw [reduce_b h]
      exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
have : SizeOf.sizeOf u.step < SizeOf.sizeOf u := u.step_wf h

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.IsSpecial

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ x✝.reduce.IsSpecial

Tactic:
rw [reduce_a h]

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ u.finish.IsSpecial

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : u.r = 0
hs : x✝.IsSpecial
⊢ u.finish.IsSpecial

Tactic:
exact u.finish_isSpecial hs

Result:
no goals

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ x✝.reduce.IsSpecial

Tactic:
rw [reduce_b h]

Result:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial

Proof state:
x✝ : XgcdType
u : XgcdType := x✝
h : ¬u.r = 0
hs : x✝.IsSpecial
this : sizeOf u.step < sizeOf u
⊢ u.step.reduce.flip.IsSpecial

Tactic:
exact (flip_isSpecial _).mpr (reduce_isSpecial _ (u.step_isSpecial hs))

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem support_subset_iff {s : Set ι} {f : Π₀ i, β i} : ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
s : Set ι
f : Π₀ (i : ι), β i
⊢ ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0

Tactic:
simpa [Set.subset_def] using forall_congr' fun i => not_imp_comm

Result:
no goals
-- Mathlib/Topology/Homotopy/HomotopyGroup.lean
theorem symmAt_indep {i} (j) (f : Ω^ N X x) :
    (⟦symmAt i f⟧ : HomotopyGroup N X x) = ⟦symmAt j f⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦symmAt i f⟧ = ⟦symmAt j f⟧

Tactic:
simp_rw [← fromLoop_symm_toLoop]

Result:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
⊢ ⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧

Proof state:
N : Type u_1
X : Type u_2
inst✝¹ : TopologicalSpace X
x : X
inst✝ : DecidableEq N
i j : N
f : ↑(Ω^ N X x)
inv : (G : Type ?u.355342) → Group G → G → G := fun G x x_1 => x_1⁻¹
⊢ ⟦fromLoop i (Path.symm (toLoop i f))⟧ = ⟦fromLoop j (Path.symm (toLoop j f))⟧

Tactic:
exact congr_fun (congr_arg (inv <| HomotopyGroup N X x) <| auxGroup_indep i j) ⟦f⟧

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderIso.lean
theorem image_Icc (e : α ≃o β) (a b : α) : e '' Icc a b = Icc (e a) (e b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ≃o β
a b : α
⊢ ⇑e '' Icc a b = Icc (e a) (e b)

Tactic:
rw [e.image_eq_preimage, e.symm.preimage_Icc, e.symm_symm]

Result:
no goals
-- Mathlib/Algebra/Homology/QuasiIso.lean
lemma ChainComplex.quasiIsoAt₀_iff {K L : ChainComplex C ℕ} (f : K ⟶ L)
    [K.HasHomology 0] [L.HasHomology 0] [(K.sc' 1 0 0).HasHomology] [(L.sc' 1 0 0).HasHomology] :
    QuasiIsoAt f 0 ↔
      ShortComplex.QuasiIso ((HomologicalComplex.shortComplexFunctor' C _ 1 0 0).map f) :=
  quasiIsoAt_iff' _ _ _ _ (by simp) (by simp)

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : ChainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 1 0 0).HasHomology
inst✝ : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasZeroMorphisms C
K L : ChainComplex C ℕ
f : K ⟶ L
inst✝³ : HasHomology K 0
inst✝² : HasHomology L 0
inst✝¹ : (sc' K 1 0 0).HasHomology
inst✝ : (sc' L 1 0 0).HasHomology
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mfderivWithin_fst {s : Set (M × M')} {x : M × M'}
    (hxs : UniqueMDiffWithinAt (I.prod I') s x) :
    mfderivWithin (I.prod I') I Prod.fst s x =
      ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderiv (I.prod I') I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
exact mfderiv_fst

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderivWithin (I.prod I') I Prod.fst s x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)

Tactic:
rw [MDifferentiable.mfderivWithin mdifferentiableAt_fst hxs]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
s : Set (M × M')
x : M × M'
hxs : UniqueMDiffWithinAt (I.prod I') s x
⊢ mfderiv (I.prod I') I Prod.fst x = ContinuousLinearMap.fst 𝕜 (TangentSpace I x.1) (TangentSpace I' x.2)
-- Mathlib/Algebra/Polynomial/Module/Basic.lean
theorem comp_smul (p p' : R[X]) (q : PolynomialModule R M) :
    comp p (p' • q) = p'.comp p • comp p q

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ (comp p) (p' • q) = p'.comp p • (comp p) q

Tactic:
rw [comp_apply, map_smul, eval_smul, Polynomial.comp, Polynomial.eval_map, comp_apply]

Result:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • (eval p) ((map R[X] (lsingle R 0)) q)

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
p p' : R[X]
q : PolynomialModule R M
⊢ eval₂ (algebraMap R R[X]) p p' • (eval p) ((map R[X] (lsingle R 0)) q) =
    eval₂ C p p' • (eval p) ((map R[X] (lsingle R 0)) q)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem mul_rpow (hx : 0 ≤ x) (hy : 0 ≤ y) : (x * y) ^ z = x ^ z * y ^ z

Proof state:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = x ^ z * y ^ z

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
rw [Real.rpow_def_of_nonneg]

Result:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Proof state:
case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
all_goals positivity

Result:
no goals

Proof state:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ rexp (log (x * y) * z) = (if x = 0 then if z = 0 then 1 else 0 else rexp (log x * z)) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
split_ifs with h_ifs <;> simp_all

Result:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Proof state:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

Tactic:
rw [log_mul ‹_› ‹_›, add_mul, exp_add, rpow_def_of_pos (hy.lt_of_ne' ‹_›)]

Result:
no goals

Proof state:
case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y

Tactic:
positivity

Result:
no goals

Proof state:
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ (x * y) ^ z = x ^ z * y ^ z

Tactic:
iterate 2 rw [Real.rpow_def_of_nonneg]; split_ifs with h_ifs <;> simp_all

Result:
case neg
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs✝ : ¬y = 0
h_ifs : ¬x = 0
⊢ rexp (log (x * y) * z) = rexp (log x * z) * y ^ z

case neg.hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
h_ifs : ¬x = 0 ∧ ¬y = 0
⊢ 0 ≤ x

case hx
x y z : ℝ
hx : 0 ≤ x
hy : 0 ≤ y
⊢ 0 ≤ x * y
-- Mathlib/RingTheory/Norm/Transitivity.lean
/-- `M * aux M k` is upper triangular. -/
lemma mul_auxMat_blockTriangular : (M * auxMat M k).BlockTriangular (· = k) :=
  fun i j lt ↦ by
    simp_rw [lt_iff_not_le, le_Prop_eq, Classical.not_imp] at lt
    simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]
    rw [Finset.sum_ite, Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton,
      Finset.sum_ite_eq', if_pos, lt.1, mul_comm, neg_add_cancel]
    exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : (fun x => x = k) j < (fun x => x = k) i
⊢ (M * auxMat M k) i j = 0

Tactic:
simp_rw [lt_iff_not_le, le_Prop_eq, Classical.not_imp] at lt

Result:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (M * auxMat M k) i j = 0

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (M * auxMat M k) i j = 0

Tactic:
simp_rw [Matrix.mul_apply, auxMat, of_apply, if_neg lt.2, mul_ite, mul_neg, mul_zero]

Result:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x : m, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else 0) = 0

Proof state:
case hc
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ j ∈ Finset.filter (fun x => ¬x = k) Finset.univ

Tactic:
exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, lt.2⟩

Result:
no goals

Proof state:
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ (∑ x : m, if x = k then -(M i x * M k j) else if x = j then M i x * M k k else 0) = 0

Tactic:
rw [Finset.sum_ite, Finset.filter_eq', if_pos (Finset.mem_univ _), Finset.sum_singleton,
  Finset.sum_ite_eq', if_pos, lt.1, mul_comm, neg_add_cancel]

Result:
case hc
S : Type u_2
m : Type u_5
inst✝² : CommRing S
M : Matrix m m S
inst✝¹ : DecidableEq m
k : m
inst✝ : Fintype m
i j : m
lt : i = k ∧ ¬j = k
⊢ j ∈ Finset.filter (fun x => ¬x = k) Finset.univ