harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem lintegral_nnnorm_condExpIndSMul_le (hm : m ≤ m0) (hs : MeasurableSet s) (hμs : μ s ≠ ∞)
    (x : G) [SigmaFinite (μ.trim hm)] : ∫⁻ a, ‖condExpIndSMul hm hs hμs x a‖₊ ∂μ ≤ μ s * ‖x‖₊

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊

Tactic:
gcongr

Result:
case bc.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ s ∩ t ⊆ s

Proof state:
case bc.h
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ s ∩ t ⊆ s

Tactic:
apply Set.inter_subset_left

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
⊢ ∫⁻ (a : α), ↑‖↑↑(condExpIndSMul hm hs hμs x) a‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine lintegral_le_of_forall_fin_meas_trim_le hm (μ s * ‖x‖₊) fun t ht hμt => ?_

Result:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ↑‖↑↑(condExpIndSMul hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Proof state:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ ∫⁻ (x_1 : α) in t, ↑‖↑↑(condExpIndSMul hm hs hμs x) x_1‖₊ ∂μ ≤ μ s * ↑‖x‖₊

Tactic:
refine (setLIntegral_nnnorm_condExpIndSMul_le hm hs hμs x ht hμt).trans ?_

Result:
α : Type u_1
G : Type u_5
inst✝² : NormedAddCommGroup G
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
inst✝¹ : NormedSpace ℝ G
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
x : G
inst✝ : SigmaFinite (μ.trim hm)
t : Set α
ht : MeasurableSet t
hμt : μ t ≠ ⊤
⊢ μ (s ∩ t) * ↑‖x‖₊ ≤ μ s * ↑‖x‖₊
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_prod_left_eq_zip {l : Array α} (f : α → β) :
    (l.map fun x => (x, f x)) = l.zip (l.map f)

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => (x, f x)) l = l.zip (map f l)

Tactic:
rw [← zip_map']

Result:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ (map (fun x => x) l).zip (map f l) = l.zip (map f l)

Proof state:
case e_as
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => x) l = l

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ (map (fun x => x) l).zip (map f l) = l.zip (map f l)

Tactic:
congr

Result:
case e_as
α : Type u_1
β : Type u_2
l : Array α
f : α → β
⊢ map (fun x => x) l = l
-- Mathlib/Combinatorics/Additive/VerySmallDoubling.lean
private lemma big_intersection {x y : G} (hx : x ∈ A) (hy : y ∈ A) :
    2 * #A ≤ #((x • A) ∩ (y • A)) + #(A * A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A = #(x •> A ∩ y •> A) + #(x •> A ∪ y •> A)

Tactic:
rw [card_inter_add_card_union]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A = #(x •> A) + #(y •> A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ x •> A ⊆ A * A ∧ y •> A ⊆ A * A

Tactic:
exact ⟨smul_finset_subset_mul hx, smul_finset_subset_mul hy⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ 2 * #A ≤ #(x •> A ∩ y •> A) + #(A * A)

Tactic:
have : #((x • A) ∪ (y • A)) ≤ #(A * A) := by
  refine card_le_card ?_
  rw [union_subset_iff]
  exact ⟨smul_finset_subset_mul hx, smul_finset_subset_mul hy⟩

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A ≤ #(x •> A ∩ y •> A) + #(A * A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ x •> A ∪ y •> A ⊆ A * A

Tactic:
rw [union_subset_iff]

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ x •> A ⊆ A * A ∧ y •> A ⊆ A * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ #(x •> A ∪ y •> A) ≤ #(A * A)

Tactic:
refine card_le_card ?_

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
⊢ x •> A ∪ y •> A ⊆ A * A

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A ≤ #(x •> A ∩ y •> A) + #(A * A)

Tactic:
refine (add_le_add_left this _).trans_eq' ?_

Result:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A = #(x •> A ∩ y •> A) + #(x •> A ∪ y •> A)

Proof state:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
x y : G
hx : x ∈ A
hy : y ∈ A
this : #(x •> A ∪ y •> A) ≤ #(A * A)
⊢ 2 * #A = #(x •> A) + #(y •> A)

Tactic:
simp only [card_smul_finset, two_mul]

Result:
no goals
-- Mathlib/GroupTheory/Abelianization.lean
theorem map_commutator_eq {H : Type*} [Group H] (f : G →* H) :
    Subgroup.map f (_root_.commutator G) = ⁅f.range, f.range⁆

Proof state:
case hy
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker

Tactic:
rw [codisjoint_iff, top_sup_eq]

Result:
no goals

Proof state:
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Subgroup.map f (commutator G) = ⁅f.range, f.range⁆

Tactic:
rw [_root_.commutator_def, Subgroup.map_commutator]

Result:
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ ⁅Subgroup.map f ⊤, Subgroup.map f ⊤⁆ = ⁅f.range, f.range⁆

Proof state:
case hy
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Subgroup.map f ⊤ = f.range

Tactic:
rw [Subgroup.map_eq_range_iff]

Result:
case hy
G : Type u
inst✝¹ : Group G
H : Type u_1
inst✝ : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
-- Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
theorem lift_comp_one_right {A : C} {B : Mon_ C} (f : A ⟶ B.X) (g : A ⟶ 𝟙_ C) :
    lift f (g ≫ B.one) ≫ B.mul = f

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ B.X
g : A ⟶ 𝟙_ C
this : lift f g ≫ B.X ◁ B.one ≫ B.mul = lift f g ≫ (ρ_ B.X).hom
⊢ lift f (g ≫ B.one) ≫ B.mul = f

Tactic:
rwa [lift_whiskerLeft_assoc, lift_rightUnitor_hom] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ B.X
g : A ⟶ 𝟙_ C
⊢ lift f (g ≫ B.one) ≫ B.mul = f

Tactic:
have := lift f g ≫= B.mul_one

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ B.X
g : A ⟶ 𝟙_ C
this : lift f g ≫ B.X ◁ B.one ≫ B.mul = lift f g ≫ (ρ_ B.X).hom
⊢ lift f (g ≫ B.one) ≫ B.mul = f
-- Mathlib/CategoryTheory/Limits/Shapes/Preorder/HasIterationOfShape.lean
lemma hasIterationOfShape_of_initialSeg {α : Type*} [LinearOrder α]
    (h : α ≤i J) [Nonempty α] :
    HasIterationOfShape α C where
  hasColimitsOfShape := hasColimitsOfShape_of_initialSeg C h
  hasColimitsOfShape_of_isSuccLimit j hj

Proof state:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ Nonempty ↑(Set.Iio j)

Tactic:
obtain ⟨a, ha⟩ := not_isMin_iff.1 hj.1

Result:
case intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
a : α
ha : a < j
⊢ Nonempty ↑(Set.Iio j)

Proof state:
case intro
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
a : α
ha : a < j
⊢ Nonempty ↑(Set.Iio j)

Tactic:
exact ⟨⟨a, ha⟩⟩

Result:
no goals

Proof state:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
have : Nonempty (Set.Iio j) := by
  obtain ⟨a, ha⟩ := not_isMin_iff.1 hj.1
  exact ⟨⟨a, ha⟩⟩

Result:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty ↑(Set.Iio j)
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Proof state:
J : Type w
inst✝⁶ : LinearOrder J
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasIterationOfShape J C
inst✝³ : SuccOrder J
inst✝² : WellFoundedLT J
α : Type u_1
inst✝¹ : LinearOrder α
h : (fun x1 x2 => x1 < x2) ≼i fun x1 x2 => x1 < x2
inst✝ : Nonempty α
j : α
hj : Order.IsSuccLimit j
this : Nonempty ↑(Set.Iio j)
⊢ HasColimitsOfShape (↑(Set.Iio j)) C

Tactic:
exact hasColimitsOfShape_of_initialSeg  _
  (InitialSeg.trans (Set.principalSegIio j) h)

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem disjoint_compl_left_iff : Disjoint xᶜ y ↔ y ≤ x

Proof state:
α : Type u
x y : α
inst✝ : BooleanAlgebra α
⊢ Disjoint xᶜ y ↔ y ≤ x

Tactic:
rw [← le_compl_iff_disjoint_left, compl_compl]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infDist_closure : infDist x (closure s) = infDist x s

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
x : α
⊢ infDist x (closure s) = infDist x s

Tactic:
simp [infDist, infEdist_closure]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem arccos_le_pi (x : ℝ) : arccos x ≤ π

Proof state:
x : ℝ
⊢ π / 2 - arcsin x ≤ π

Tactic:
linarith [neg_pi_div_two_le_arcsin x]

Result:
no goals

Proof state:
x : ℝ
⊢ arccos x ≤ π

Tactic:
unfold arccos

Result:
x : ℝ
⊢ π / 2 - arcsin x ≤ π
-- Mathlib/Probability/Kernel/Defs.lean
theorem sum_add [Countable ι] (κ η : ι → Kernel α β) :
    (Kernel.sum fun n => κ n + η n) = Kernel.sum κ + Kernel.sum η

Proof state:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ η : ι → Kernel α β
⊢ (Kernel.sum fun n => κ n + η n) = Kernel.sum κ + Kernel.sum η

Tactic:
ext a s hs

Result:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ η : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => κ n + η n) a) s = ((Kernel.sum κ + Kernel.sum η) a) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝ : Countable ι
κ η : ι → Kernel α β
a : α
s : Set β
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => κ n + η n) a) s = ((Kernel.sum κ + Kernel.sum η) a) s

Tactic:
simp only [coe_add, Pi.add_apply, sum_apply, Measure.sum_apply _ hs, Pi.add_apply,
  Measure.coe_add, tsum_add ENNReal.summable ENNReal.summable]

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem erase_add_single (i : ι) (f : Π₀ i, β i) : f.erase i + single i (f i) = f :=
  ext fun i' =>
    if h : i = i' then by
      subst h; simp only [add_apply, single_apply, erase_apply, zero_add, dite_eq_ite, if_true]
    else by
      simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : ¬i = i'
⊢ (erase i f + single i (f i)) i' = f i'

Tactic:
simp only [add_apply, single_apply, erase_apply, dif_neg h, if_neg (Ne.symm h), add_zero]

Result:
no goals

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
i' : ι
h : i = i'
⊢ (erase i f + single i (f i)) i' = f i'

Tactic:
subst h

Result:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase i f + single i (f i)) i = f i

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
i : ι
f : Π₀ (i : ι), β i
⊢ (erase i f + single i (f i)) i = f i

Tactic:
simp only [add_apply, single_apply, erase_apply, zero_add, dite_eq_ite, if_true]

Result:
no goals
-- Mathlib/Geometry/RingedSpace/LocallyRingedSpace.lean
@[reassoc]
lemma stalkMap_congr (f g : X ⟶ Y) (hfg : f = g) (x x' : X) (hxx' : x = x') :
    f.stalkMap x ≫ X.presheaf.stalkSpecializes (specializes_of_eq hxx'.symm) =
      Y.presheaf.stalkSpecializes (specializes_of_eq <| hfg ▸ hxx' ▸ rfl) ≫ g.stalkMap x'

Proof state:
X Y : LocallyRingedSpace
f g : X ⟶ Y
hfg : f = g
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap g x'

Tactic:
subst hfg

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x

Tactic:
simp

Result:
no goals

Proof state:
X Y : LocallyRingedSpace
f : X ⟶ Y
x x' : ↑X.toTopCat
hxx' : x = x'
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x'

Tactic:
subst hxx'

Result:
X Y : LocallyRingedSpace
f : X ⟶ Y
x : ↑X.toTopCat
⊢ Hom.stalkMap f x ≫ X.presheaf.stalkSpecializes ⋯ = Y.presheaf.stalkSpecializes ⋯ ≫ Hom.stalkMap f x
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂'_comp (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (n' → R) →ₗ[R] n → R) :
    toMatrix₂' R (B.comp f) = (toMatrix' f)ᵀ * toMatrix₂' R B

Proof state:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B ∘ₗ f) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
rw [← LinearMap.compl₂_id (B.comp f), ← LinearMap.compl₁₂]

Result:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Proof state:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (n' → R) →ₗ[R] n → R
⊢ (toMatrix₂' R) (B.compl₁₂ f id) = (toMatrix' f)ᵀ * (toMatrix₂' R) B

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Shift/SingleFunctors.lean
@[reassoc (attr := simp)]
lemma hom_inv_id_hom_app (e : F ≅ G) (n : A) (X : C) :
    (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 _

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_7, u_1} C
inst✝² : Category.{u_6, u_2} D
A : Type u_5
inst✝¹ : AddMonoid A
inst✝ : HasShift D A
F G : SingleFunctors C D A
e : F ≅ G
n : A
X : C
⊢ (e.hom.hom n).app X ≫ (e.inv.hom n).app X = 𝟙 ((F.functor n).obj X)

Tactic:
rw [← NatTrans.comp_app, hom_inv_id_hom, NatTrans.id_app]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem strictMono_rpow_of_pos {z : ℝ} (h : 0 < z) : StrictMono fun x : ℝ≥0∞ => x ^ z

Proof state:
case intro.inr.intro
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : ↑x < ↑y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ↑y

Tactic:
simp only [← coe_rpow_of_nonneg _ h.le, NNReal.rpow_lt_rpow (coe_lt_coe.1 hxy) h, coe_lt_coe]

Result:
no goals

Proof state:
z : ℝ
h : 0 < z
⊢ StrictMono fun x => x ^ z

Tactic:
intro x y hxy

Result:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y

Proof state:
case intro
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y

Tactic:
rcases eq_or_ne y ∞ with (rfl | hy)

Result:
case intro.inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ⊤

case intro.inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y

Proof state:
case intro.inl
z : ℝ
h : 0 < z
x : ℝ≥0
hxy : ↑x < ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ⊤

Tactic:
simp only [top_rpow_of_pos h, ← coe_rpow_of_nonneg _ h.le, coe_lt_top]

Result:
no goals

Proof state:
case intro.inr
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
hy : y ≠ ⊤
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y

Tactic:
lift y to ℝ≥0 using hy

Result:
case intro.inr.intro
z : ℝ
h : 0 < z
x y : ℝ≥0
hxy : ↑x < ↑y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) ↑y

Proof state:
z : ℝ
h : 0 < z
x y : ℝ≥0∞
hxy : x < y
⊢ (fun x => x ^ z) x < (fun x => x ^ z) y

Tactic:
lift x to ℝ≥0 using ne_top_of_lt hxy

Result:
case intro
z : ℝ
h : 0 < z
y : ℝ≥0∞
x : ℝ≥0
hxy : ↑x < y
⊢ (fun x => x ^ z) ↑x < (fun x => x ^ z) y
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem dist_self_div_right (a b : E) : dist a (a / b) = ‖b‖

Proof state:
E : Type u_2
inst✝ : SeminormedCommGroup E
a b : E
⊢ dist a (a / b) = ‖b‖

Tactic:
rw [div_eq_mul_inv, dist_self_mul_right, norm_inv']

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_zero_of_column_eq (i_ne_j : i ≠ j) (hij : ∀ k, M k i = M k j) : M.det = 0

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ i = Mᵀ j

Tactic:
exact funext hij

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ M.det = 0

Tactic:
rw [← det_transpose, det_zero_of_row_eq i_ne_j]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
i_ne_j : i ≠ j
hij : ∀ (k : n), M k i = M k j
⊢ Mᵀ i = Mᵀ j
-- Mathlib/Data/Set/Lattice.lean
theorem iSup_iUnion (s : ι → Set α) (f : α → β) : ⨆ a ∈ ⋃ i, s i, f a = ⨆ (i) (a ∈ s i), f a

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j

Tactic:
simp_rw [mem_iUnion, iSup_exists]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ i, ⨆ a ∈ s i, f a

Tactic:
rw [iSup_comm]

Result:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : CompleteLattice β
s : ι → Set α
f : α → β
⊢ ⨆ a ∈ ⋃ i, s i, f a = ⨆ j, ⨆ i, ⨆ (_ : j ∈ s i), f j
-- Mathlib/Data/ZMod/Basic.lean
theorem _root_.Prod.snd_zmod_cast (a : ZMod n) : (cast a : R × S).snd = cast a

Proof state:
n : ℕ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod n
⊢ a.cast.2 = a.cast

Tactic:
cases n

Result:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Proof state:
case succ
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
n✝ : ℕ
a : ZMod (n✝ + 1)
⊢ a.cast.2 = a.cast

Tactic:
simp [ZMod.cast]

Result:
no goals

Proof state:
case zero
R : Type u_1
inst✝¹ : AddGroupWithOne R
S : Type u_2
inst✝ : AddGroupWithOne S
a : ZMod 0
⊢ a.cast.2 = a.cast

Tactic:
rfl

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem zero_right (a : ℤ) : J(a | 0) = 1

Proof state:
a : ℤ
⊢ J(a | 0) = 1

Tactic:
simp only [jacobiSym, primeFactorsList_zero, List.prod_nil, List.pmap]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Range.lean
theorem zipIdx_append (xs : Vector α n) (ys : Vector α m) (k : Nat) :
    zipIdx (xs ++ ys) k = zipIdx xs k ++ zipIdx ys (k + n)

Proof state:
case mk
α : Type u_1
m : Nat
ys : Vector α m
k : Nat
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ ys).zipIdx k =
    { toArray := xs, size_toArray := ⋯ }.zipIdx k ++ ys.zipIdx (k + xs.size)

Tactic:
rcases ys with ⟨ys, rfl⟩

Result:
case mk.mk
α : Type u_1
k : Nat
xs ys : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }).zipIdx k =
    { toArray := xs, size_toArray := ⋯ }.zipIdx k ++ { toArray := ys, size_toArray := ⋯ }.zipIdx (k + xs.size)

Proof state:
α : Type u_1
n m : Nat
xs : Vector α n
ys : Vector α m
k : Nat
⊢ (xs ++ ys).zipIdx k = xs.zipIdx k ++ ys.zipIdx (k + n)

Tactic:
rcases xs with ⟨xs, rfl⟩

Result:
case mk
α : Type u_1
m : Nat
ys : Vector α m
k : Nat
xs : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ ys).zipIdx k =
    { toArray := xs, size_toArray := ⋯ }.zipIdx k ++ ys.zipIdx (k + xs.size)

Proof state:
case mk.mk
α : Type u_1
k : Nat
xs ys : Array α
⊢ ({ toArray := xs, size_toArray := ⋯ } ++ { toArray := ys, size_toArray := ⋯ }).zipIdx k =
    { toArray := xs, size_toArray := ⋯ }.zipIdx k ++ { toArray := ys, size_toArray := ⋯ }.zipIdx (k + xs.size)

Tactic:
simp [Array.zipIdx_append]

Result:
no goals