harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_alter [EquivBEq α] [LawfulHashable α] {k k' : α} {f : Option β → Option β}
    (h : m.WF) {hc : k' ∈ Const.alter m k f} :
    Const.get (Const.alter m k f) k' hc =
      if heq : k == k' then
        haveI h' : (f (Const.get? m k)).isSome := mem_alter_of_beq h heq |>.mp hc
        f (Const.get? m k) |>.get h'
      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
        Const.get m k' h'

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ (alter m k f).contains k' = true →
    get (alter m k f) k' hc = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

Tactic:
simp_to_raw using Raw₀.Const.get_alter

Result:
no goals

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ get (alter m k f) k' hc = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
hc✝ : k' ∈ alter m k f
hc : (alter m k f).contains k' = true
⊢ get (alter m k f) k' hc✝ = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
hc✝ : k' ∈ alter m k f
hc : (alter m k f).contains k' = true
⊢ get (alter m k f) k' hc✝ = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯

Tactic:
revert hc

Result:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k k' : α
f : Option β → Option β
h : m.WF
hc : k' ∈ alter m k f
⊢ (alter m k f).contains k' = true →
    get (alter m k f) k' hc = if heq : (k == k') = true then (f (get? m k)).get ⋯ else get m k' ⋯
-- Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean
theorem aux_ne_zero (f : (L ≃ₐ[K] L) → Lˣ) : aux f ≠ 0 :=
/- the set `Aut_K(L)` is linearly independent in the `L`-vector space `L → L`, by Dedekind's
linear independence of characters -/
  have : LinearIndependent L (fun (f : L ≃ₐ[K] L) => (f : L → L)) :=
    LinearIndependent.comp (ι' := L ≃ₐ[K] L)
      (linearIndependent_monoidHom L L) (fun f => f)
      (fun x y h => by ext; exact DFunLike.ext_iff.1 h _)
  have h := linearIndependent_iff.1 this
    (Finsupp.equivFunOnFinite.symm (fun φ => (f φ : L)))
  fun H => Units.ne_zero (f 1) (DFunLike.ext_iff.1 (h H) 1)

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
x y : L ≃ₐ[K] L
h : (fun f => ↑f) x = (fun f => ↑f) y
a✝ : L
⊢ x a✝ = y a✝

Tactic:
exact DFunLike.ext_iff.1 h _

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
x y : L ≃ₐ[K] L
h : (fun f => ↑f) x = (fun f => ↑f) y
⊢ x = y

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
inst✝ : FiniteDimensional K L
f : (L ≃ₐ[K] L) → Lˣ
x y : L ≃ₐ[K] L
h : (fun f => ↑f) x = (fun f => ↑f) y
a✝ : L
⊢ x a✝ = y a✝
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
/-- Let `A` be an `R`-algebra.
`𝔭 : Spec R` is in the image of `D(f) ⊆ Spec S`
if and only if `f` is not nilpotent on `κ(𝔭) ⊗ A`. -/
lemma mem_image_comap_basicOpen (f : A) (x) :
    x ∈ comap (algebraMap R A) '' basicOpen f ↔
      ¬ IsNilpotent (algebraMap A (A ⊗[R] x.asIdeal.ResidueField) f)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ x ∈ ⇑(comap (algebraMap R A)) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
have e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A]
    (A ⧸ (Ideal.span ∅ : Ideal A)) ⊗[R] x.asIdeal.ResidueField := by
  refine Algebra.TensorProduct.congr ?f AlgEquiv.refl
  rw [Ideal.span_empty]
  exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }

Result:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ ⇑(comap (algebraMap R A)) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField

Tactic:
refine Algebra.TensorProduct.congr ?f AlgEquiv.refl

Result:
case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ Ideal.span ∅

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
e : A ⊗[R] x.asIdeal.ResidueField ≃ₐ[A] (A ⧸ Ideal.span ∅) ⊗[R] x.asIdeal.ResidueField
⊢ x ∈ ⇑(comap (algebraMap R A)) '' ↑(basicOpen f) ↔ ¬IsNilpotent ((algebraMap A (A ⊗[R] x.asIdeal.ResidueField)) f)

Tactic:
rw [← IsNilpotent.map_iff e.injective, AlgEquiv.commutes,
  ← mem_image_comap_zeroLocus_sdiff f ∅ x, zeroLocus_empty, ← Set.compl_eq_univ_diff,
  basicOpen_eq_zeroLocus_compl]

Result:
no goals

Proof state:
case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ ⊥

Tactic:
exact { __ := (RingEquiv.quotientBot A).symm, __ := Algebra.ofId _ _ }

Result:
no goals

Proof state:
case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ Ideal.span ∅

Tactic:
rw [Ideal.span_empty]

Result:
case f
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing A
inst✝ : Algebra R A
f : A
x : PrimeSpectrum R
⊢ A ≃ₐ[A] A ⧸ ⊥
-- Mathlib/RingTheory/Norm/Basic.lean
theorem norm_eq_zero_iff_of_basis [IsDomain R] [IsDomain S] (b : Basis ι R S) {x : S} :
    Algebra.norm R x = 0 ↔ x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
this : Free R S
⊢ (norm R) x = 0 ↔ x = 0

Tactic:
haveI : Module.Finite R S := Module.Finite.of_basis b

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
this✝ : Free R S
this : Module.Finite R S
⊢ (norm R) x = 0 ↔ x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
⊢ (norm R) x = 0 ↔ x = 0

Tactic:
haveI : Module.Free R S := Module.Free.of_basis b

Result:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
this : Free R S
⊢ (norm R) x = 0 ↔ x = 0

Proof state:
R : Type u_1
S : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring S
inst✝³ : Algebra R S
ι : Type w
inst✝² : Finite ι
inst✝¹ : IsDomain R
inst✝ : IsDomain S
b : Basis ι R S
x : S
this✝ : Free R S
this : Module.Finite R S
⊢ (norm R) x = 0 ↔ x = 0

Tactic:
exact norm_eq_zero_iff

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_mul (A : M) (h : IsUnit A.det) : ∀ m n : ℤ, A ^ (m * n) = (A ^ m) ^ n
  | (m : ℕ), (n : ℕ) => by rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.ofNat_mul]
  | (m : ℕ), -[n+1] => by
    rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]
  | -[m+1], (n : ℕ) => by
    rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
        inv_pow']
  | -[m+1], -[n+1] => by
    rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_natCast, inv_pow', ←
      pow_mul, nonsing_inv_nonsing_inv]
    rw [det_pow]
    exact h.pow _

Proof state:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (n + 1)))

Tactic:
exact h.pow _

Result:
no goals

Proof state:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A ^ ((m + 1) * (n + 1))).det

Tactic:
rw [det_pow]

Result:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A.det ^ ((m + 1) * (n + 1)))

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (↑m * ↑n) = (A ^ ↑m) ^ ↑n

Tactic:
rw [zpow_natCast, zpow_natCast, ← pow_mul, ← zpow_natCast, Int.ofNat_mul]

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * ↑n) = (A ^ -[m+1]) ^ ↑n

Tactic:
rw [zpow_natCast, zpow_negSucc, ← inv_pow', ← pow_mul, negSucc_mul_ofNat, zpow_neg_natCast,
    inv_pow']

Result:
no goals

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (-[m+1] * -[n+1]) = (A ^ -[m+1]) ^ -[n+1]

Tactic:
rw [zpow_negSucc, zpow_negSucc, negSucc_mul_negSucc, ← Int.ofNat_mul, zpow_natCast, inv_pow', ←
  pow_mul, nonsing_inv_nonsing_inv]

Result:
case h
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ IsUnit (A ^ ((m + 1) * (n + 1))).det

Proof state:
n' : Type u_1
inst✝² : DecidableEq n'
inst✝¹ : Fintype n'
R : Type u_2
inst✝ : CommRing R
A : M
h : IsUnit A.det
m n : ℕ
⊢ A ^ (↑m * -[n+1]) = (A ^ ↑m) ^ -[n+1]

Tactic:
rw [zpow_natCast, zpow_negSucc, ← pow_mul, ofNat_mul_negSucc, zpow_neg_natCast]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/NatAntidiagonal.lean
theorem antidiagonalTuple_one (n : ℕ) : antidiagonalTuple 1 n = [![n]]

Proof state:
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]

Tactic:
conv_rhs => rw [← List.nil_append [![n]]]

Result:
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]

Proof state:
n : ℕ
⊢ antidiagonalTuple 1 n = [![n]]

Tactic:
simp_rw [antidiagonalTuple, antidiagonal, List.range_succ, List.map_append, List.map_singleton,
  Nat.sub_self, List.flatMap_append, List.flatMap_singleton, List.flatMap_map]

Result:
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [![n]]

Proof state:
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []

Tactic:
obtain ⟨m, rfl⟩ := Nat.exists_eq_add_of_lt hx

Result:
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []

Proof state:
case e_a.intro
x m : ℕ
hx : x < x + m + 1
⊢ antidiagonalTuple 0 (x + m + 1 - x) = []

Tactic:
rw [add_assoc, add_tsub_cancel_left, antidiagonalTuple_zero_succ]

Result:
no goals

Proof state:
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) ++
      map (fun x => Fin.cons n x) (antidiagonalTuple 0 0) =
    [] ++ [![n]]

Tactic:
congr 1

Result:
case e_a
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) = []

Proof state:
case e_a
n : ℕ
⊢ flatMap (fun a => map (fun x => Fin.cons a x) (antidiagonalTuple 0 (n - a))) (range n) = []

Tactic:
simp_rw [List.flatMap_eq_nil_iff, List.mem_range, List.map_eq_nil_iff]

Result:
case e_a
n : ℕ
⊢ ∀ x < n, antidiagonalTuple 0 (n - x) = []

Proof state:
case e_a
n : ℕ
⊢ ∀ x < n, antidiagonalTuple 0 (n - x) = []

Tactic:
intro x hx

Result:
case e_a
n x : ℕ
hx : x < n
⊢ antidiagonalTuple 0 (n - x) = []
-- Mathlib/LinearAlgebra/TensorProduct/Graded/External.lean
theorem gradedMul_algebraMap (x : (⨁ i, 𝒜 i) ⊗[R] (⨁ i, ℬ i)) (r : R) :
    gradedMul R 𝒜 ℬ x (algebraMap R _ r ⊗ₜ 1) = r • x

Proof state:
case a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ ((gradedMul R 𝒜 ℬ) ((lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝)) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝

Tactic:
erw [tmul_of_gradedMul_of_tmul]

Result:
case a.H.h.H.h
R : Type u_1
ι : Type u_2
inst✝¹¹ : CommSemiring ι
inst✝¹⁰ : Module ι (Additive ℤˣ)
inst✝⁹ : DecidableEq ι
𝒜 : ι → Type u_3
ℬ : ι → Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : (i : ι) → AddCommGroup (𝒜 i)
inst✝⁶ : (i : ι) → AddCommGroup (ℬ i)
inst✝⁵ : (i : ι) → Module R (𝒜 i)
inst✝⁴ : (i : ι) → Module R (ℬ i)
inst✝³ : DirectSum.GRing 𝒜
inst✝² : DirectSum.GRing ℬ
inst✝¹ : DirectSum.GAlgebra R 𝒜
inst✝ : DirectSum.GAlgebra R ℬ
x : (⨁ (i : ι), 𝒜 i) ⊗[R] ⨁ (i : ι), ℬ i
r : R
i✝¹ : ι
x✝¹ : 𝒜 i✝¹
i✝ : ι
x✝ : ℬ i✝
⊢ (-1) ^ (i✝ * 0) • ((lof R ι 𝒜 i✝¹) x✝¹ * (lof R ι 𝒜 0) (DirectSum.GAlgebra.toFun r)) ⊗ₜ[R] ((lof R ι ℬ i✝) x✝ * 1) =
    r • (lof R ι 𝒜 i✝¹) x✝¹ ⊗ₜ[R] (lof R ι ℬ i✝) x✝
-- Mathlib/Algebra/Exact.lean
lemma Exact.inl_snd : Function.Exact (LinearMap.inl R M N) (LinearMap.snd R M N)

Proof state:
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
⊢ Exact ⇑(LinearMap.inl R M N) ⇑(LinearMap.snd R M N)

Tactic:
rintro ⟨x, y⟩

Result:
case mk
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.snd R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inl R M N)

Proof state:
case mk
R : Type u_1
M : Type u_2
N : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : AddCommMonoid N
inst✝¹ : Module R M
inst✝ : Module R N
x : M
y : N
⊢ (LinearMap.snd R M N) (x, y) = 0 ↔ (x, y) ∈ Set.range ⇑(LinearMap.inl R M N)

Tactic:
simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq,
  exists_eq_left]

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma ofHom_neg (φ : F ⟶ G) :
    Cochain.ofHom (-φ) = -Cochain.ofHom φ

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
⊢ ofHom (-φ) = -ofHom φ

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Order/SuccPred/Archimedean.lean
theorem Succ.rec {P : α → Prop} {m : α} (h0 : P m) (h1 : ∀ n, m ≤ n → P n → P (succ n)) ⦃n : α⦄
    (hmn : m ≤ n) : P n

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
⊢ P (succ^[n] m)

Tactic:
induction' n with n ih

Result:
case intro.zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
⊢ P (succ^[0] m)

case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ^[n + 1] m)

Proof state:
case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ^[n + 1] m)

Tactic:
rw [Function.iterate_succ_apply']

Result:
case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ (succ^[n] m))

Proof state:
case intro.succ
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
ih : P (succ^[n] m)
⊢ P (succ (succ^[n] m))

Tactic:
exact h1 _ (id_le_iterate_of_id_le le_succ n m) ih

Result:
no goals

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : α
hmn : m ≤ n
⊢ P n

Tactic:
obtain ⟨n, rfl⟩ := hmn.exists_succ_iterate

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
hmn : m ≤ succ^[n] m
⊢ P (succ^[n] m)

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
hmn : m ≤ succ^[n] m
⊢ P (succ^[n] m)

Tactic:
clear hmn

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
n : ℕ
⊢ P (succ^[n] m)

Proof state:
case intro.zero
α : Type u_1
inst✝² : Preorder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
P : α → Prop
m : α
h0 : P m
h1 : ∀ (n : α), m ≤ n → P n → P (succ n)
⊢ P (succ^[0] m)

Tactic:
exact h0

Result:
no goals
-- Mathlib/Data/Stream/Init.lean
theorem get_unfolds_head_tail : ∀ (n : ℕ) (s : Stream' α),
    get (unfolds head tail s) n = get s n

Proof state:
case zero
α : Type u
⊢ ∀ (s : Stream' α), (unfolds head tail s).get 0 = s.get 0

Tactic:
intro s

Result:
case zero
α : Type u
s : Stream' α
⊢ (unfolds head tail s).get 0 = s.get 0

Proof state:
case zero
α : Type u
s : Stream' α
⊢ (unfolds head tail s).get 0 = s.get 0

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u
⊢ ∀ (n : ℕ) (s : Stream' α), (unfolds head tail s).get n = s.get n

Tactic:
intro n

Result:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n

Proof state:
α : Type u
n : ℕ
⊢ ∀ (s : Stream' α), (unfolds head tail s).get n = s.get n

Tactic:
induction' n with n' ih

Result:
case zero
α : Type u
⊢ ∀ (s : Stream' α), (unfolds head tail s).get 0 = s.get 0

case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n' = s.get n'
⊢ ∀ (s : Stream' α), (unfolds head tail s).get (n' + 1) = s.get (n' + 1)

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n' = s.get n'
⊢ ∀ (s : Stream' α), (unfolds head tail s).get (n' + 1) = s.get (n' + 1)

Tactic:
intro s

Result:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n' = s.get n'
s : Stream' α
⊢ (unfolds head tail s).get (n' + 1) = s.get (n' + 1)

Proof state:
case succ
α : Type u
n' : ℕ
ih : ∀ (s : Stream' α), (unfolds head tail s).get n' = s.get n'
s : Stream' α
⊢ (unfolds head tail s).get (n' + 1) = s.get (n' + 1)

Tactic:
rw [get_succ, get_succ, unfolds_eq, tail_cons, ih]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq
    {s : Set E} {t : Set F} {g : F → G} {f : E → F} {y : F} (x : E)
    (hg : ContDiffWithinAt 𝕜 n g t y) (hf : ContDiffWithinAt 𝕜 n f s x)
    (hs : f ⁻¹' t ∈ 𝓝[s] x) (hy : f x = y) : ContDiffWithinAt 𝕜 n (g ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
exact hg.comp_of_preimage_mem_nhdsWithin x hf hs

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
y : F
x : E
hg : ContDiffWithinAt 𝕜 n g t y
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hy : f x = y
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
n : WithTop ℕ∞
s : Set E
t : Set F
g : F → G
f : E → F
x : E
hf : ContDiffWithinAt 𝕜 n f s x
hs : f ⁻¹' t ∈ 𝓝[s] x
hg : ContDiffWithinAt 𝕜 n g t (f x)
⊢ ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_cons {l : List α} (h : 0 < n) : take n (a :: l) = a :: take (n - 1) l

Proof state:
case succ
α : Type u_1
a : α
l : List α
n : Nat
h : 0 < n + 1
⊢ take (n + 1) (a :: l) = a :: take (n + 1 - 1) l

Tactic:
rfl

Result:
no goals

Proof state:
case zero
α : Type u_1
a : α
l : List α
h : 0 < 0
⊢ take 0 (a :: l) = a :: take (0 - 1) l

Tactic:
exact absurd h (Nat.lt_irrefl _)

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
h : 0 < n
⊢ take n (a :: l) = a :: take (n - 1) l

Tactic:
cases n with
| zero => exact absurd h (Nat.lt_irrefl _)
| succ n => rfl

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem norm_toL1_eq_lintegral_norm (f : α → β) (hf : Integrable f μ) :
    ‖hf.toL1 f‖ = ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
hf : Integrable f μ
⊢ ‖toL1 f hf‖ = (∫⁻ (a : α), ENNReal.ofReal ‖f a‖ ∂μ).toReal

Tactic:
rw [norm_toL1, lintegral_norm_eq_lintegral_edist]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem coordChange_apply_snd (e₁ e₂ : Trivialization F proj) {p : Z} (h : proj p ∈ e₁.baseSet) :
    e₁.coordChange e₂ (proj p) (e₁ p).snd = (e₂ p).snd

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₁ e₂ : Trivialization F proj
p : Z
h : proj p ∈ e₁.baseSet
⊢ e₁.coordChange e₂ (proj p) (↑e₁ p).2 = (↑e₂ p).2

Tactic:
rw [coordChange, e₁.symm_apply_mk_proj (e₁.mem_source.2 h)]

Result:
no goals
-- Mathlib/Probability/Process/PartitionFiltration.lean
lemma iSup_countableFiltration (α : Type*) [m : MeasurableSpace α] [CountablyGenerated α] :
    ⨆ n, countableFiltration α n = m

Proof state:
α : Type u_2
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ⨆ n, ↑(countableFiltration α) n = m

Tactic:
conv_rhs => rw [← generateFrom_iUnion_countablePartition α, ← iSup_generateFrom]

Result:
α : Type u_2
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ⨆ n, ↑(countableFiltration α) n = ⨆ i, generateFrom (countablePartition α i)

Proof state:
α : Type u_2
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ ⨆ n, ↑(countableFiltration α) n = ⨆ i, generateFrom (countablePartition α i)

Tactic:
rfl

Result:
no goals