harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/ToArray.lean
theorem foldr_toArray (f : α → β → β) (init : β) (l : List α) :
    l.toArray.foldr f init = l.foldr f init

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
init : β
l : List α
⊢ Array.foldr f init l.toArray = foldr f init l

Tactic:
rw [foldr_toList]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ZPow.lean
theorem zpow_sub_one {A : M} (h : IsUnit A.det) (n : ℤ) : A ^ (n - 1) = A ^ n * A⁻¹ :=
  calc
    A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹

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
n : ℤ
⊢ A ^ (n - 1) = A ^ (n - 1) * A * A⁻¹

Tactic:
rw [mul_assoc, mul_nonsing_inv _ h, mul_one]

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
n : ℤ
⊢ A ^ (n - 1) * A * A⁻¹ = A ^ n * A⁻¹

Tactic:
rw [← zpow_add_one h, sub_add_cancel]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_replicate : (replicate n a).filter p = if p a then replicate n a else []

Proof state:
case zero
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ filter p (replicate 0 a) = if p a = true then replicate 0 a else []

Tactic:
simp

Result:
no goals

Proof state:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ (if p a = true then a :: filter p (replicate n a) else filter p (replicate n a)) =
    if p a = true then a :: replicate n a else []

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
p : α✝ → Bool
⊢ filter p (replicate n a) = if p a = true then replicate n a else []

Tactic:
cases n with
| zero => simp
| succ n =>
  simp only [replicate_succ, filter_cons]
  split <;> simp_all

Result:
no goals

Proof state:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ filter p (replicate (n + 1) a) = if p a = true then replicate (n + 1) a else []

Tactic:
simp only [replicate_succ, filter_cons]

Result:
case succ
α✝ : Type u_1
a : α✝
p : α✝ → Bool
n : Nat
⊢ (if p a = true then a :: filter p (replicate n a) else filter p (replicate n a)) =
    if p a = true then a :: replicate n a else []
-- Mathlib/GroupTheory/Perm/Cycle/Basic.lean
theorem IsCycleOn.conj (h : f.IsCycleOn s) : (g * f * g⁻¹).IsCycleOn ((g : Perm α) '' s) :=
  ⟨(g.bijOn_image.comp h.1).comp g.bijOn_symm_image, fun x hx y hy => by
    rw [← preimage_inv] at hx hy
    convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]⟩

Proof state:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑g '' s
y : α
hy : y ∈ ⇑g '' s
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
rw [← preimage_inv] at hx hy

Result:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑g⁻¹ ⁻¹' s
y : α
hy : y ∈ ⇑g⁻¹ ⁻¹' s
⊢ (g * f * g⁻¹).SameCycle x y

Proof state:
α : Type u_2
f g : Perm α
s : Set α
h : f.IsCycleOn s
x : α
hx : x ∈ ⇑g⁻¹ ⁻¹' s
y : α
hy : y ∈ ⇑g⁻¹ ⁻¹' s
⊢ (g * f * g⁻¹).SameCycle x y

Tactic:
convert Equiv.Perm.SameCycle.conj (h.2 hx hy) (g := g) <;> rw [apply_inv_self]

Result:
no goals
-- Mathlib/Probability/Independence/Conditional.lean
lemma iCondIndepFun_iff {β : ι → Type*}
    (m : ∀ x : ι, MeasurableSpace (β x)) (f : ∀ x : ι, Ω → β x) (hf : ∀ i, Measurable (f i))
    (μ : Measure Ω) [IsFiniteMeasure μ] :
    iCondIndepFun m' hm' m f μ
      ↔ ∀ (s : Finset ι) {g : ι → Set Ω} (_H : ∀ i, i ∈ s → MeasurableSet[(m i).comap (f i)] (g i)),
      μ⟦⋂ i ∈ s, g i | m'⟧ =ᵐ[μ] ∏ i ∈ s, (μ⟦g i | m'⟧)

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndepFun m' hm' m f μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']

Tactic:
simp only [iCondIndepFun_iff_iCondIndep]

Result:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']

Proof state:
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ iCondIndep m' hm' (fun x => MeasurableSpace.comap (f x) (m x)) μ ↔
    ∀ (s : Finset ι) {g : ι → Set Ω},
      (∀ i ∈ s, MeasurableSet (g i)) →
        μ[(⋂ i ∈ s, g i).indicator fun ω => 1|m'] =ᶠ[ae μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1|m']

Tactic:
rw [iCondIndep_iff]

Result:
case hm
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ

Proof state:
case hm
Ω : Type u_1
ι : Type u_2
m' mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
hm' : m' ≤ mΩ
β : ι → Type u_3
m : (x : ι) → MeasurableSpace (β x)
f : (x : ι) → Ω → β x
hf : ∀ (i : ι), Measurable (f i)
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
⊢ ∀ (i : ι), MeasurableSpace.comap (f i) (m i) ≤ mΩ

Tactic:
exact fun i ↦ (hf i).comap_le

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
@[to_additive]
lemma exists_isComplement_right (H : Subgroup G) (g : G) :
    ∃ T, IsComplement H T ∧ g ∈ T

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
refine Function.update_of_ne ?_ g Quotient.out ▸ q.out_eq'

Result:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Proof state:
case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ q ≠ Quotient.mk'' g

Tactic:
exact hq

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
⊢ ∃ T, IsComplement (↑H) T ∧ g ∈ T

Tactic:
refine ⟨Set.range (Function.update Quotient.out _ g), isComplement_range_right fun q ↦ ?_,
  Quotient.mk'' g, Function.update_self (Quotient.mk'' g) g Quotient.out⟩

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Proof state:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
exact hq.symm ▸ congr_arg _ (Function.update_self (Quotient.mk'' g) g Quotient.out)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

Tactic:
by_cases hq : q = Quotient.mk'' g

Result:
case pos
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q

case neg
G : Type u_1
inst✝ : Group G
H : Subgroup G
g : G
q : Quotient (QuotientGroup.rightRel H)
hq : ¬q = Quotient.mk'' g
⊢ Quotient.mk'' (update Quotient.out (Quotient.mk'' g) g q) = q
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem mapsTo_sin_Ioo : MapsTo sin (Ioo (-(π / 2)) (π / 2)) (Ioo (-1) 1) := fun x h => by
  rwa [mem_Ioo, ← arcsin_lt_pi_div_two, ← neg_pi_div_two_lt_arcsin, arcsin_sin h.1.le h.2.le]

Proof state:
x : ℝ
h : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ sin x ∈ Ioo (-1) 1

Tactic:
rwa [mem_Ioo, ← arcsin_lt_pi_div_two, ← neg_pi_div_two_lt_arcsin, arcsin_sin h.1.le h.2.le]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem divRadical_isUnit {u : E} (hu : IsUnit u) : IsUnit (divRadical u)

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
u : E
hu : IsUnit u
⊢ IsUnit (divRadical u)

Tactic:
rwa [divRadical, radical_of_isUnit hu, EuclideanDomain.div_one]

Result:
no goals
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem mul_dvd_mul : ∀ {a b c d : α}, a ∣ b → c ∣ d → a * c ∣ b * d
  | a, _, c, _, ⟨e, rfl⟩, ⟨f, rfl⟩ => ⟨e * f, by simp⟩

Proof state:
α : Type u_1
inst✝ : CommSemigroup α
a c e f : α
⊢ a * e * (c * f) = a * c * (e * f)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma leftRightHomologyComparison'_eq_descH :
    leftRightHomologyComparison' h₁ h₂ =
      h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) (by simp))
        (by rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
          LeftHomologyData.f'_i_assoc, RightHomologyData.wp, zero_comp])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.descH (h₂.liftH (h₁.i ≫ h₂.p) ⋯) ⋯

Tactic:
simp only [← cancel_mono h₂.ι, ← cancel_epi h₁.π, π_leftRightHomologyComparison'_ι,
  LeftHomologyData.π_descH_assoc, RightHomologyData.liftH_ι]

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ (h₁.i ≫ h₂.p) ≫ h₂.g' = 0

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁✝ : S₁.HomologyData
h₂✝ : S₂.HomologyData
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
⊢ h₁.f' ≫ h₂.liftH (h₁.i ≫ h₂.p) ⋯ = 0

Tactic:
rw [← cancel_mono h₂.ι, assoc, RightHomologyData.liftH_ι,
LeftHomologyData.f'_i_assoc, RightHomologyData.wp, zero_comp]

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem binary_relation_sInf_iff {α β : Type*} (s : Set (α → β → Prop)) {a : α} {b : β} :
    sInf s a b ↔ ∀ r : α → β → Prop, r ∈ s → r a b

Proof state:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ (⨅ f, ↑f a) b ↔ ∀ r ∈ s, r a b

Tactic:
simp [← eq_iff_iff]

Result:
no goals

Proof state:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ sInf s a b ↔ ∀ r ∈ s, r a b

Tactic:
rw [sInf_apply]

Result:
α : Type u_8
β : Type u_9
s : Set (α → β → Prop)
a : α
b : β
⊢ (⨅ f, ↑f a) b ↔ ∀ r ∈ s, r a b
-- Mathlib/Analysis/InnerProductSpace/Projection.lean
theorem orthogonalProjection_mem_subspace_eq_self (v : K) : orthogonalProjection K v = v

Proof state:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : ↥K
⊢ ↑((orthogonalProjection K) ↑v) = ↑v

Tactic:
apply eq_orthogonalProjection_of_mem_of_inner_eq_zero <;> simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : ↥K
⊢ (orthogonalProjection K) ↑v = v

Tactic:
ext

Result:
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
inst✝ : HasOrthogonalProjection K
v : ↥K
⊢ ↑((orthogonalProjection K) ↑v) = ↑v
-- Mathlib/Data/Fin/VecNotation.lean
theorem tail_cons (x : α) (u : Fin m → α) : vecTail (vecCons x u) = u

Proof state:
case h
α : Type u
m : ℕ
x : α
u : Fin m → α
x✝ : Fin m
⊢ vecTail (vecCons x u) x✝ = u x✝

Tactic:
simp [vecTail]

Result:
no goals

Proof state:
α : Type u
m : ℕ
x : α
u : Fin m → α
⊢ vecTail (vecCons x u) = u

Tactic:
ext

Result:
case h
α : Type u
m : ℕ
x : α
u : Fin m → α
x✝ : Fin m
⊢ vecTail (vecCons x u) x✝ = u x✝
-- Mathlib/Data/Nat/ModEq.lean
theorem add_div_le_add_div (a b c : ℕ) : a / c + b / c ≤ (a + b) / c :=
  if hc0 : c = 0 then by simp [hc0]
  else by rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]; exact Nat.le_add_right _ _

Proof state:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ (a + b) / c

Tactic:
rw [Nat.add_div (Nat.pos_of_ne_zero hc0)]

Result:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Proof state:
a b c : ℕ
hc0 : ¬c = 0
⊢ a / c + b / c ≤ a / c + b / c + if c ≤ a % c + b % c then 1 else 0

Tactic:
exact Nat.le_add_right _ _

Result:
no goals

Proof state:
a b c : ℕ
hc0 : c = 0
⊢ a / c + b / c ≤ (a + b) / c

Tactic:
simp [hc0]

Result:
no goals
-- Mathlib/Data/Multiset/Filter.lean
theorem filter_singleton {a : α} (p : α → Prop) [DecidablePred p] :
    filter p {a} = if p a then {a} else ∅

Proof state:
α : Type u_1
a : α
p : α → Prop
inst✝ : DecidablePred p
⊢ filter p {a} = if p a then {a} else ∅

Tactic:
simp only [singleton, filter_cons, filter_zero, Multiset.add_zero, empty_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem hexagon_forward (X Y Z : Dial C) :
    (associator X Y Z).hom ≫ (braiding X (Y ⊗ Z)).hom ≫ (associator Y Z X).hom =
      tensorHom (braiding X Y).hom (𝟙 Z) ≫ (associator Y X Z).hom ≫
      tensorHom (𝟙 Y) (braiding X Z).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y Z : Dial C
⊢ (X.associator Y Z).hom ≫ (X.braiding (Y ⊗ Z)).hom ≫ (Y.associator Z X).hom =
    tensorHom (X.braiding Y).hom (𝟙 Z) ≫ (Y.associator X Z).hom ≫ tensorHom (𝟙 Y) (X.braiding Z).hom

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/Int/Log.lean
theorem log_of_right_le_one (b : ℕ) {r : R} (hr : r ≤ 1) : log b r = -Nat.clog b ⌈r⁻¹⌉₊

Proof state:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ log b 1 = -↑(Nat.clog b ⌈1⁻¹⌉₊)

Tactic:
rw [log, if_pos hr, inv_one, Nat.ceil_one, Nat.floor_one, Nat.log_one_right, Nat.clog_one_right,
  Int.ofNat_zero, neg_zero]

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)

Tactic:
exact if_neg hr.not_le

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr : r ≤ 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)

Tactic:
obtain rfl | hr := hr.eq_or_lt

Result:
case inl
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
hr : 1 ≤ 1
⊢ log b 1 = -↑(Nat.clog b ⌈1⁻¹⌉₊)

case inr
R : Type u_1
inst✝¹ : LinearOrderedSemifield R
inst✝ : FloorSemiring R
b : ℕ
r : R
hr✝ : r ≤ 1
hr : r < 1
⊢ log b r = -↑(Nat.clog b ⌈r⁻¹⌉₊)
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_smul_nonzero (p : R[X]) (ha : a ≠ 0) : (a • p).roots = p.roots

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R[X]
ha : a ≠ 0
⊢ (a • p).roots = p.roots

Tactic:
rw [smul_eq_C_mul, roots_C_mul _ ha]

Result:
no goals
-- Mathlib/Data/Matrix/Reflection.lean
theorem transposeᵣ_eq : ∀ {m n} (A : Matrix (Fin m) (Fin n) α), transposeᵣ A = transpose A
  | _, 0, _ => Subsingleton.elim _ _
  | m, n + 1, A =>
    Matrix.ext fun i j => by
      simp_rw [transposeᵣ, transposeᵣ_eq]
      refine i.cases ?_ fun i => ?_
      · dsimp
        rw [FinVec.map_eq, Function.comp_apply]
      · simp only [of_apply, Matrix.cons_val_succ]
        rfl

Proof state:
case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) i j = Aᵀ i j

Tactic:
refine i.cases ?_ fun i => ?_

Result:
case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j = Aᵀ 0 j

case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j

Proof state:
case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) 0 j = Aᵀ 0 j

Tactic:
dsimp

Result:
case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ FinVec.map (fun v => v 0) A j = A j 0

Proof state:
case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) i.succ j = Aᵀ i.succ j

Tactic:
simp only [of_apply, Matrix.cons_val_succ]

Result:
case refine_2
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i✝ : Fin (n + 1)
j : Fin m
i : Fin n
⊢ (A.submatrix id Fin.succ)ᵀ i j = Aᵀ i.succ j

Proof state:
case refine_1
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ FinVec.map (fun v => v 0) A j = A j 0

Tactic:
rw [FinVec.map_eq, Function.comp_apply]

Result:
no goals

Proof state:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ A.transposeᵣ i j = Aᵀ i j

Tactic:
simp_rw [transposeᵣ, transposeᵣ_eq]

Result:
α : Type u_1
m n : ℕ
A : Matrix (Fin m) (Fin (n + 1)) α
i : Fin (n + 1)
j : Fin m
⊢ of (vecCons (FinVec.map (fun v => v 0) A) (A.submatrix id Fin.succ)ᵀ) i j = Aᵀ i j
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/Rpow/Basic.lean
@[simp]
lemma rpow_algebraMap {x : ℝ≥0} {y : ℝ} :
    (algebraMap ℝ≥0 A x) ^ y = algebraMap ℝ≥0 A (x ^ y)

Proof state:
A : Type u_1
inst✝⁵ : PartialOrder A
inst✝⁴ : Ring A
inst✝³ : StarRing A
inst✝² : TopologicalSpace A
inst✝¹ : Algebra ℝ A
inst✝ : ContinuousFunctionalCalculus ℝ≥0 fun a => 0 ≤ a
x : ℝ≥0
y : ℝ
⊢ (algebraMap ℝ≥0 A) x ^ y = (algebraMap ℝ≥0 A) (x ^ y)

Tactic:
rw [rpow_def, cfc_algebraMap ..]

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem map_nhds_eq (hf : ApproximatesLinearOn f f' s c) (f'symm : f'.NonlinearRightInverse) {x : E}
    (hs : s ∈ 𝓝 x) (hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹) : map f (𝓝 x) = 𝓝 (f x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
⊢ map f (𝓝 x) = 𝓝 (f x)

Tactic:
refine
  le_antisymm ((hf.continuousOn x (mem_of_mem_nhds hs)).continuousAt hs) (le_map fun t ht => ?_)

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
⊢ f '' t ∈ 𝓝 (f x)

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
this : f '' (s ∩ t) ∈ 𝓝 (f x)
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
exact mem_of_superset this (image_subset _ inter_subset_right)

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
⊢ f '' t ∈ 𝓝 (f x)

Tactic:
have : f '' (s ∩ t) ∈ 𝓝 (f x) :=
  (hf.mono_set inter_subset_left).image_mem_nhds f'symm (inter_mem hs ht) hc

Result:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
x : E
hs : s ∈ 𝓝 x
hc : Subsingleton F ∨ c < f'symm.nnnorm⁻¹
t : Set E
ht : t ∈ 𝓝 x
this : f '' (s ∩ t) ∈ 𝓝 (f x)
⊢ f '' t ∈ 𝓝 (f x)
-- Mathlib/Algebra/Homology/HomotopyCategory/MappingCone.lean
@[simp]
lemma inr_fst :
    (Cochain.ofHom (inr φ)).comp (fst φ).1 (zero_add 1) = 0

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ p + 0 = p

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ p + 1 = q

Tactic:
omega

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
⊢ (Cochain.ofHom (inr φ)).comp ↑(fst φ) ⋯ = 0

Tactic:
ext p q hpq

Result:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ ((Cochain.ofHom (inr φ)).comp ↑(fst φ) ⋯).v p q hpq = Cochain.v 0 p q hpq

Proof state:
case h
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
F G : CochainComplex C ℤ
φ : F ⟶ G
inst✝ : HasHomotopyCofiber φ
p q : ℤ
hpq : p + 1 = q
⊢ ((Cochain.ofHom (inr φ)).comp ↑(fst φ) ⋯).v p q hpq = Cochain.v 0 p q hpq

Tactic:
simp [Cochain.comp_v _ _ (zero_add 1) p p q (by omega) (by omega)]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem coeIdeal_eq_one {I : Ideal R} : (I : FractionalIdeal R⁰ K) = 1 ↔ I = 1

Proof state:
R : Type u_1
inst✝³ : CommRing R
K : Type u_3
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
I : Ideal R
⊢ ↑I = 1 ↔ I = 1

Tactic:
simpa only [Ideal.one_eq_top] using coeIdeal_inj

Result:
no goals
-- Mathlib/MeasureTheory/SetSemiring.lean
theorem iInter_le_mem (hC : IsSetRing C) {s : ℕ → Set α} (hs : ∀ n, s n ∈ C) (n : ℕ) :
    (⋂ i ≤ n, s i) ∈ C

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
⊢ (⋂ k, ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C

Tactic:
exact hC.inter_mem hn (hs _)

Result:
no goals

Proof state:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
⊢ ⋂ i, ⋂ (_ : i ≤ n + 1), s i ∈ C

Tactic:
rw [biInter_le_succ]

Result:
case succ
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
hn : ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C
⊢ (⋂ k, ⋂ (_ : k ≤ n), s k) ∩ s (n + 1) ∈ C

Proof state:
case zero
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
⊢ ⋂ i, ⋂ (_ : i ≤ 0), s i ∈ C

Tactic:
simp [hs 0]

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
hC : IsSetRing C
s : ℕ → Set α
hs : ∀ (n : ℕ), s n ∈ C
n : ℕ
⊢ ⋂ i, ⋂ (_ : i ≤ n), s i ∈ C

Tactic:
induction n with
| zero => simp [hs 0]
| succ n hn => rw [biInter_le_succ]; exact hC.inter_mem hn (hs _)

Result:
no goals