harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Final.lean
theorem preservesLimit_of_comp {B : Type u₄} [Category.{v₄} B] {H : E ⥤ B}
    [PreservesLimit (F ⋙ G) H] : PreservesLimit G H where
  preserves {c} hc

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ ∀ (j : C),
    (H.mapCone (Cone.whisker F c)).π.app j =
      (Iso.refl (H.mapCone (Cone.whisker F c)).pt).hom ≫ (Cone.whisker F (H.mapCone c)).π.app j

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ Nonempty (IsLimit (H.mapCone c))

Tactic:
refine ⟨isLimitWhiskerEquiv F _ ?_⟩

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Tactic:
let hc' := isLimitOfPreserves H ((isLimitWhiskerEquiv F _).symm hc)

Result:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Proof state:
C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : F.Initial
E : Type u₃
inst✝² : Category.{v₃, u₃} E
G : D ⥤ E
B : Type u₄
inst✝¹ : Category.{v₄, u₄} B
H : E ⥤ B
inst✝ : PreservesLimit (F ⋙ G) H
c : Cone G
hc : IsLimit c
hc' : IsLimit (H.mapCone (Cone.whisker F c)) := isLimitOfPreserves H ((isLimitWhiskerEquiv F c).symm hc)
⊢ IsLimit (Cone.whisker F (H.mapCone c))

Tactic:
exact IsLimit.ofIsoLimit hc' (Cones.ext (Iso.refl _) (by simp))

Result:
no goals
-- Mathlib/CategoryTheory/Sites/CoverPreserving.lean
theorem CoverPreserving.comp {F} (hF : CoverPreserving J K F) {G} (hG : CoverPreserving K L G) :
    CoverPreserving J L (F ⋙ G) :=
  ⟨fun hS => by
    rw [Sieve.functorPushforward_comp]
    exact hG.cover_preserve (hF.cover_preserve hS)⟩

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ L ((F ⋙ G).obj U✝)

Tactic:
exact hG.cover_preserve (hF.cover_preserve hS)

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward (F ⋙ G) S✝ ∈ L ((F ⋙ G).obj U✝)

Tactic:
rw [Sieve.functorPushforward_comp]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
A : Type u₃
inst✝ : Category.{v₃, u₃} A
J : GrothendieckTopology C
K : GrothendieckTopology D
L : GrothendieckTopology A
F : C ⥤ D
hF : CoverPreserving J K F
G : D ⥤ A
hG : CoverPreserving K L G
U✝ : C
S✝ : Sieve U✝
hS : S✝ ∈ J U✝
⊢ Sieve.functorPushforward G (Sieve.functorPushforward F S✝) ∈ L ((F ⋙ G).obj U✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem msb_cast (h : w = v) (x : BitVec w) : (x.cast h).msb = x.msb

Proof state:
w v : Nat
h : w = v
x : BitVec w
⊢ (BitVec.cast h x).msb = x.msb

Tactic:
simp [BitVec.msb]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/InfiniteSum.lean
theorem Summable.of_norm_bounded [CompleteSpace E] {f : ι → E} (g : ι → ℝ) (hg : Summable g)
    (h : ∀ i, ‖f i‖ ≤ g i) : Summable f

Proof state:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ Summable f

Tactic:
rw [summable_iff_cauchySeq_finset]

Result:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ b ∈ s, f b

Proof state:
ι : Type u_1
E : Type u_3
inst✝¹ : SeminormedAddCommGroup E
inst✝ : CompleteSpace E
f : ι → E
g : ι → ℝ
hg : Summable g
h : ∀ (i : ι), ‖f i‖ ≤ g i
⊢ CauchySeq fun s => ∑ b ∈ s, f b

Tactic:
exact cauchySeq_finset_of_norm_bounded g hg h

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma Injective2_disjSum {α β : Type*} : Function.Injective2 (@disjSum α β) :=
  fun _ _ _ _ => by simp [Finset.ext_iff]

Proof state:
α : Type u_3
β : Type u_4
x✝³ x✝² : Finset α
x✝¹ x✝ : Finset β
⊢ x✝³.disjSum x✝¹ = x✝².disjSum x✝ → x✝³ = x✝² ∧ x✝¹ = x✝

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem norm_values_discrete (a : PadicSeq p) (ha : ¬a ≈ 0) : ∃ z : ℤ, a.norm = (p : ℚ) ^ (-z)

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : a.norm = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, a.norm = ↑p ^ (-z)

Tactic:
simpa [hk] using padicNorm.values_discrete hk'

Result:
no goals

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
⊢ ∃ z, a.norm = ↑p ^ (-z)

Tactic:
let ⟨k, hk, hk'⟩ := norm_eq_norm_app_of_nonzero ha

Result:
p : ℕ
hp : Fact (Nat.Prime p)
a : PadicSeq p
ha : ¬a ≈ 0
k : ℚ
hk : a.norm = padicNorm p k
hk' : k ≠ 0
⊢ ∃ z, a.norm = ↑p ^ (-z)
-- Mathlib/Topology/Algebra/Support.lean
theorem comp₂_left (hf : HasCompactMulSupport f)
    (hf₂ : HasCompactMulSupport f₂) (hm : m 1 1 = 1) :
    HasCompactMulSupport fun x => m (f x) (f₂ x)

Proof state:
case h
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (f x) (f₂ x) = 1 x

Tactic:
simp_rw [hx, hx₂, Pi.one_apply, hm]

Result:
no goals

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : HasCompactMulSupport f
hf₂ : HasCompactMulSupport f₂
hm : m 1 1 = 1
⊢ HasCompactMulSupport fun x => m (f x) (f₂ x)

Tactic:
rw [hasCompactMulSupport_iff_eventuallyEq] at hf hf₂ ⊢

Result:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1

Proof state:
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
⊢ (fun x => m (f x) (f₂ x)) =ᶠ[coclosedCompact α] 1

Tactic:
filter_upwards [hf, hf₂] with x hx hx₂

Result:
case h
α : Type u_2
β : Type u_4
γ : Type u_5
δ : Type u_6
inst✝³ : TopologicalSpace α
inst✝² : One β
inst✝¹ : One γ
inst✝ : One δ
f : α → β
f₂ : α → γ
m : β → γ → δ
hf : f =ᶠ[coclosedCompact α] 1
hf₂ : f₂ =ᶠ[coclosedCompact α] 1
hm : m 1 1 = 1
x : α
hx : f x = 1 x
hx₂ : f₂ x = 1 x
⊢ m (f x) (f₂ x) = 1 x
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem sum_int_mod (s : Finset α) (n : ℤ) (f : α → ℤ) :
    (∑ i ∈ s, f i) % n = (∑ i ∈ s, f i % n) % n :=
  (Multiset.sum_int_mod _ _).trans <| by rw [Finset.sum, Multiset.map_map]; rfl

Proof state:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map (fun x => x % n) (Multiset.map (fun i => f i) s.val)).sum % n = (∑ i ∈ s, f i % n) % n

Tactic:
rw [Finset.sum, Multiset.map_map]

Result:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n

Proof state:
α : Type u_3
s : Finset α
n : ℤ
f : α → ℤ
⊢ (Multiset.map ((fun x => x % n) ∘ fun i => f i) s.val).sum % n = (Multiset.map (fun i => f i % n) s.val).sum % n

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mul_div_cancel (m : Nat) {n : Nat} (H : 0 < n) : m * n / n = m

Proof state:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m

Tactic:
rwa [Nat.zero_add, Nat.zero_div, Nat.zero_add] at t

Result:
no goals

Proof state:
m n : Nat
H : 0 < n
⊢ m * n / n = m

Tactic:
let t := add_mul_div_right 0 m H

Result:
m n : Nat
H : 0 < n
t : (0 + m * n) / n = 0 / n + m := add_mul_div_right 0 m H
⊢ m * n / n = m
-- Mathlib/Probability/Kernel/RadonNikodym.lean
@[fun_prop]
lemma measurable_rnDeriv_right (κ η : Kernel α γ) (a : α) :
    Measurable (fun x : γ ↦ rnDeriv κ η a x)

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
⊢ Measurable fun x => κ.rnDeriv η a x

Tactic:
fun_prop

Result:
no goals
-- Mathlib/Computability/TMConfig.lean
theorem succ_eval : succ.eval = fun v => pure [v.headI.succ]

Proof state:
⊢ succ.eval = fun v => pure [v.headI.succ]

Tactic:
simp [eval]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orthogonal.lean
theorem mem_orthogonal' (v : E) : v ∈ Kᗮ ↔ ∀ u ∈ K, ⟪v, u⟫ = 0

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
K : Submodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ u ∈ K, inner v u = 0

Tactic:
simp_rw [mem_orthogonal, inner_eq_zero_symm]

Result:
no goals
-- Mathlib/FieldTheory/Galois/Basic.lean
lemma IntermediateField.restrictNormalHom_ker (E : IntermediateField K L) [Normal K E] :
    (restrictNormalHom E).ker = E.fixingSubgroup

Proof state:
K : Type u_3
L : Type u_4
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
E : IntermediateField K L
inst✝ : Normal K ↥E
⊢ (restrictNormalHom ↥E).ker = E.fixingSubgroup

Tactic:
simp [fixingSubgroup, Subgroup.ext_iff, AlgEquiv.ext_iff, Subtype.ext_iff,
  restrictNormalHom_apply, mem_fixingSubgroup_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Prod.lean
theorem false_of_nontrivial_of_product_domain (R S : Type*) [Ring R] [Ring S] [IsDomain (R × S)]
    [Nontrivial R] [Nontrivial S] : False

Proof state:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False

Tactic:
rw [Prod.mk_eq_zero, Prod.mk_eq_zero] at this

Result:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False

Proof state:
case inl.intro
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ (0, 1) * (1, 0) = 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : 0 = 0 ∧ 1 = 0 ∨ 1 = 0 ∧ 0 = 0
⊢ False

Tactic:
rcases this with (⟨_, h⟩ | ⟨h, _⟩)

Result:
case inl.intro
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
left✝ : 0 = 0
h : 1 = 0
⊢ False

case inr.intro
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Proof state:
case inr.intro
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
h : 1 = 0
right✝ : 0 = 0
⊢ False

Tactic:
exact zero_ne_one h.symm

Result:
no goals

Proof state:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
⊢ False

Tactic:
have :=
  NoZeroDivisors.eq_zero_or_eq_zero_of_mul_eq_zero (show ((0 : R), (1 : S)) * (1, 0) = 0 by simp)

Result:
R : Type u_6
S : Type u_7
inst✝⁴ : Ring R
inst✝³ : Ring S
inst✝² : IsDomain (R × S)
inst✝¹ : Nontrivial R
inst✝ : Nontrivial S
this : (0, 1) = 0 ∨ (1, 0) = 0
⊢ False
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem balance1_toList {l : RBNode α} {v r} :
    (l.balance1 v r).toList = l.toList ++ v :: r.toList

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (l.balance1 v r).toList = l.toList ++ v :: r.toList

Tactic:
unfold balance1

Result:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b).toList =
    l.toList ++ v :: r.toList

Proof state:
α : Type u_1
l : RBNode α
v : α
r : RBNode α
⊢ (match l, v, r with
      | node red (node red a x b) y c, z, d => node red (node black a x b) y (node black c z d)
      | node red a x (node red b y c), z, d => node red (node black a x b) y (node black c z d)
      | a, x, b => node black a x b).toList =
    l.toList ++ v :: r.toList

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/AddChar.lean
lemma mulShift_mulShift (ψ : AddChar R M) (r s : R) :
    mulShift (mulShift ψ r) s = mulShift ψ (r * s)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ ((ψ.mulShift r).mulShift s) x✝ = (ψ.mulShift (r * s)) x✝

Tactic:
simp only [mulShift_apply, mul_assoc]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s : R
⊢ (ψ.mulShift r).mulShift s = ψ.mulShift (r * s)

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
r s x✝ : R
⊢ ((ψ.mulShift r).mulShift s) x✝ = (ψ.mulShift (r * s)) x✝
-- Mathlib/Data/Fin/Basic.lean
theorem castPred_one [NeZero n] (h := Fin.ext_iff.not.2 one_lt_last.ne) :
    castPred (1 : Fin (n + 2)) h = 1

Proof state:
case zero
inst✝ : NeZero 0
h : optParam (¬1 = last (0 + 1)) ⋯
⊢ castPred 1 h = 1

Tactic:
exact subsingleton_one.elim _ 1

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
h : optParam (¬1 = last (n + 1)) ⋯
⊢ castPred 1 h = 1

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
h : optParam (¬1 = last (0 + 1)) ⋯
⊢ castPred 1 h = 1

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
h : optParam (¬1 = last (n✝ + 1 + 1)) ⋯
⊢ castPred 1 h = 1

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
h : optParam (¬1 = last (n✝ + 1 + 1)) ⋯
⊢ castPred 1 h = 1

Tactic:
rfl

Result:
no goals
-- Mathlib/AlgebraicGeometry/Morphisms/AffineAnd.lean
lemma targetAffineLocally_affineAnd_le
    (hQW : ∀ {R S : Type u} [CommRing R] [CommRing S] {f : R →+* S}, Q f → W f) :
    targetAffineLocally (affineAnd Q) ≤ targetAffineLocally (affineAnd W)

Proof state:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f
U : ↑Y.affineOpens
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => W) (f ∣_ ↑U)

Tactic:
exact ⟨(h U).1, hQW (h U).2⟩

Result:
no goals

Proof state:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
⊢ targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) ≤
    targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => W)

Tactic:
intro X Y f h U

Result:
Q W : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop
hQW : ∀ {R S : Type u} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S}, Q f → W f
X Y : Scheme
f : X ⟶ Y
h : targetAffineLocally (affineAnd fun {R S} [CommRing R] [CommRing S] => Q) f
U : ↑Y.affineOpens
⊢ affineAnd (fun {R S} [CommRing R] [CommRing S] => W) (f ∣_ ↑U)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem prefix_iff_eq_append : l₁ <+: l₂ ↔ l₁ ++ drop (length l₁) l₂ = l₂ :=
  ⟨by rintro ⟨r, rfl⟩; rw [drop_left], fun e => ⟨_, e⟩⟩

Proof state:
α✝ : Type u_1
l₁ l₂ : List α✝
⊢ l₁ <+: l₂ → l₁ ++ drop l₁.length l₂ = l₂

Tactic:
rintro ⟨r, rfl⟩

Result:
case intro
α✝ : Type u_1
l₁ r : List α✝
⊢ l₁ ++ drop l₁.length (l₁ ++ r) = l₁ ++ r

Proof state:
case intro
α✝ : Type u_1
l₁ r : List α✝
⊢ l₁ ++ drop l₁.length (l₁ ++ r) = l₁ ++ r

Tactic:
rw [drop_left]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem angle_rev_eq_pi_div_two_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∠ p₃ p₂ p₁ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₃ p₂ p₁ = π / 2

Tactic:
rw [angle_comm]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
exact angle_eq_pi_div_two_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/Data/Finset/Prod.lean
theorem filter_product_right (q : β → Prop) [DecidablePred q] :
    ((s ×ˢ t).filter fun x : α × β => q x.2) = s ×ˢ t.filter q

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
q : β → Prop
inst✝ : DecidablePred q
⊢ filter (fun x => q x.2) (s ×ˢ t) = s ×ˢ filter q t

Tactic:
simpa using filter_product (fun _ : α => true) q

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem to_int_eq_succ_pred (n : PosNum) : (n : ℤ) = (n.pred' : ℕ) + 1

Proof state:
n : PosNum
⊢ ↑(↑n.pred' + 1) = ↑↑n.pred' + 1

Tactic:
rfl

Result:
no goals

Proof state:
n : PosNum
⊢ ↑n = ↑↑n.pred' + 1

Tactic:
rw [← n.to_nat_to_int, to_nat_eq_succ_pred]

Result:
n : PosNum
⊢ ↑(↑n.pred' + 1) = ↑↑n.pred' + 1
-- Mathlib/CategoryTheory/EqToHom.lean
theorem comp_eqToHom_iff {X Y Y' : C} (p : Y = Y') (f : X ⟶ Y) (g : X ⟶ Y') :
    f ≫ eqToHom p = g ↔ f = g ≫ eqToHom p.symm :=
  { mp := fun h => h ▸ by simp
    mpr := fun h => by simp [eq_whisker h (eqToHom p)] }

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f ≫ eqToHom p = g
⊢ f = (f ≫ eqToHom p) ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Y' : C
p : Y = Y'
f : X ⟶ Y
g : X ⟶ Y'
h : f = g ≫ eqToHom ⋯
⊢ f ≫ eqToHom p = g

Tactic:
simp [eq_whisker h (eqToHom p)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_self_add (n m : Nat) : n - (n + m) = 0

Proof state:
n m : Nat
⊢ n + 0 - (n + m) = 0

Tactic:
rw [Nat.add_sub_add_left, Nat.zero_sub]

Result:
no goals

Proof state:
n m : Nat
⊢ n - (n + m) = 0

Tactic:
show (n + 0) - (n + m) = 0

Result:
n m : Nat
⊢ n + 0 - (n + m) = 0
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_sub_intCast (hx : x ≠ 0) (y : ℝ) (n : ℕ) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)

Tactic:
exact Real.rpow_sub_intCast (mod_cast hx) _ _

Result:
no goals

Proof state:
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
ext

Result:
case a
x : ℝ≥0
hx : x ≠ 0
y : ℝ
n : ℕ
⊢ ↑(x ^ (y - ↑n)) = ↑(x ^ y / x ^ n)
-- Mathlib/RingTheory/Flat/Basic.lean
/-- A module `M` over a ring `R` is flat iff for all finitely generated ideals `I` of `R`, the
tensor product of the inclusion `I → R` and the identity `M → M` is injective. See
`iff_rTensor_injective'` to extend to all ideals `I`. -/
lemma iff_rTensor_injective :
    Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective (I.subtype.rTensor M)

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
x : ↥I ⊗[R] M
hx : (rTensor M (Submodule.subtype I)) x = 0
⊢ x = 0

Tactic:
obtain ⟨J, hfg, hle, y, rfl⟩ := Submodule.exists_fg_le_eq_rTensor_inclusion x

Result:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : ↥J ⊗[R] M
hx : (rTensor M (Submodule.subtype I)) ((rTensor M (inclusion hle)) y) = 0
⊢ (rTensor M (inclusion hle)) y = 0

Proof state:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ Flat R M ↔ ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))

Tactic:
refine iff_rTensor_injective'.trans ⟨fun h I _ ↦ h I,
  fun h I ↦ (injective_iff_map_eq_zero _).mpr fun x hx ↦ ?_⟩

Result:
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
x : ↥I ⊗[R] M
hx : (rTensor M (Submodule.subtype I)) x = 0
⊢ x = 0

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : ↥J ⊗[R] M
hx : (rTensor M (Submodule.subtype I ∘ₗ inclusion hle)) y = 0
⊢ (rTensor M (inclusion hle)) y = 0

Tactic:
rw [(injective_iff_map_eq_zero _).mp (h hfg) y hx, map_zero]

Result:
no goals

Proof state:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : ↥J ⊗[R] M
hx : (rTensor M (Submodule.subtype I)) ((rTensor M (inclusion hle)) y) = 0
⊢ (rTensor M (inclusion hle)) y = 0

Tactic:
rw [← rTensor_comp_apply] at hx

Result:
case intro.intro.intro.intro
R : Type u
M : Type v
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
h : ∀ ⦃I : Ideal R⦄, I.FG → Function.Injective ⇑(rTensor M (Submodule.subtype I))
I : Ideal R
J : Submodule R R
hfg : J.FG
hle : J ≤ I
y : ↥J ⊗[R] M
hx : (rTensor M (Submodule.subtype I ∘ₗ inclusion hle)) y = 0
⊢ (rTensor M (inclusion hle)) y = 0