harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Real/EReal.lean
lemma inv_neg (a : EReal) : (-a)⁻¹ = -a⁻¹

Proof state:
a : EReal
⊢ (-a)⁻¹ = -a⁻¹

Tactic:
induction a

Result:
case h_bot

⊢ (-⊥)⁻¹ = -⊥⁻¹

case h_real
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -(↑a✝)⁻¹

case h_top

⊢ (-⊤)⁻¹ = -⊤⁻¹

Proof state:
case h_real
a✝ : ℝ
⊢ ↑(-a✝)⁻¹ = ↑(-a✝⁻¹)

Tactic:
exact EReal.coe_eq_coe_iff.2 _root_.inv_neg

Result:
no goals

Proof state:
case h_top

⊢ (-⊤)⁻¹ = -⊤⁻¹

Tactic:
rw [neg_top, inv_bot, inv_top, neg_zero]

Result:
no goals

Proof state:
case h_real
a✝ : ℝ
⊢ (-↑a✝)⁻¹ = -(↑a✝)⁻¹

Tactic:
rw [← coe_inv _, ← coe_neg _⁻¹, ← coe_neg _, ← coe_inv (-_)]

Result:
case h_real
a✝ : ℝ
⊢ ↑(-a✝)⁻¹ = ↑(-a✝⁻¹)

Proof state:
case h_bot

⊢ (-⊥)⁻¹ = -⊥⁻¹

Tactic:
rw [neg_bot, inv_top, inv_bot, neg_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Opposites.lean
theorem pullbackIsoUnopPushout_hom_inr {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [HasPullback f g]
    [HasPushout f.op g.op] : pushout.inr _ _ ≫ (pullbackIsoUnopPushout f g).hom.op =
    (pullback.snd f g).op

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op = (pullback.snd f g).op

Tactic:
apply Quiver.Hom.unop_inj

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.snd f g).op.unop

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pushout.inr f.op g.op ≫ (pullbackIsoUnopPushout f g).hom.op).unop = (pullback.snd f g).op.unop

Tactic:
dsimp

Result:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ (pushout.inr f.op g.op).unop = pullback.snd f g

Proof state:
case a
C : Type u₁
inst✝² : Category.{v₁, u₁} C
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝¹ : HasPullback f g
inst✝ : HasPushout f.op g.op
⊢ (pullbackIsoUnopPushout f g).hom ≫ (pushout.inr f.op g.op).unop = pullback.snd f g

Tactic:
rw [← pullbackIsoUnopPushout_inv_snd, Iso.hom_inv_id_assoc]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_mul_X_pow : ∀ (n : ℕ), (p * X^n).smeval x = p.smeval x * x^n
  | 0 => by
    simp only [npow_zero, mul_one]
  | n + 1 => by
    rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
      ← smeval_assoc_X_pow, npow_one]

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
n : ℕ
⊢ (p * X ^ (n + 1)).smeval x = p.smeval x * x ^ (n + 1)

Tactic:
rw [npow_add, ← mul_assoc, npow_one, smeval_mul_X, smeval_mul_X_pow n, npow_add,
  ← smeval_assoc_X_pow, npow_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁵ : Semiring R
p : R[X]
S : Type u_2
inst✝⁴ : NonAssocSemiring S
inst✝³ : Module R S
inst✝² : Pow S ℕ
x : S
inst✝¹ : NatPowAssoc S
inst✝ : IsScalarTower R S S
⊢ (p * X ^ 0).smeval x = p.smeval x * x ^ 0

Tactic:
simp only [npow_zero, mul_one]

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem attach_image_val [DecidableEq α] {s : Finset α} : s.attach.image Subtype.val = s :=
  eq_of_veq <| by rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ (image Subtype.val s.attach).val = s.val

Tactic:
rw [image_val, attach_val, Multiset.attach_map_val, dedup_eq_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem revAt_add {N O n o : ℕ} (hn : n ≤ N) (ho : o ≤ O) :
    revAt (N + O) (n + o) = revAt N n + revAt O o

Proof state:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Tactic:
repeat' rw [add_tsub_cancel_left]

Result:
no goals

Proof state:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n' + o' = n' + (o + o' - o)

Tactic:
rw [add_tsub_cancel_left]

Result:
no goals

Proof state:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (revAt (o + o')) o

Tactic:
rw [revAt_le (le_add_right rfl.le)]

Result:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)

Proof state:
N O n o : ℕ
hn : n ≤ N
ho : o ≤ O
⊢ (revAt (N + O)) (n + o) = (revAt N) n + (revAt O) o

Tactic:
rcases Nat.le.dest hn with ⟨n', rfl⟩

Result:
case intro
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ (revAt (n + n' + O)) (n + o) = (revAt (n + n')) n + (revAt O) o

Proof state:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o

Tactic:
repeat' rw [revAt_le (le_add_right rfl.le)]

Result:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)

Proof state:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = n + n' - n + (o + o' - o)

Tactic:
rw [add_assoc, add_left_comm n' o, ← add_assoc, revAt_le (le_add_right rfl.le)]

Result:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ n + o + (n' + o') - (n + o) = n + n' - n + (o + o' - o)

Proof state:
case intro
O n o : ℕ
ho : o ≤ O
n' : ℕ
hn : n ≤ n + n'
⊢ (revAt (n + n' + O)) (n + o) = (revAt (n + n')) n + (revAt O) o

Tactic:
rcases Nat.le.dest ho with ⟨o', rfl⟩

Result:
case intro.intro
n o n' : ℕ
hn : n ≤ n + n'
o' : ℕ
ho : o ≤ o + o'
⊢ (revAt (n + n' + (o + o'))) (n + o) = (revAt (n + n')) n + (revAt (o + o')) o
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sub_pow [CommRing R] (x y : R) (n : ℕ) :
    (x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * n.choose m

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
have : (-1 : R) ^ (n - m) = (-1) ^ (n + m) := by
  rw [mem_range] at hm
  simp [show n + m = n - m + 2 * m by omega, pow_add]

Result:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
rw [neg_pow, this]

Result:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * ((-1) ^ (n + m) * y ^ (n - m)) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-1) ^ (n - m) = (-1) ^ (n + m)

Tactic:
rw [mem_range] at hm

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ (-1) ^ (n - m) = (-1) ^ (n + m)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ (-1) ^ (n - m) = (-1) ^ (n + m)

Tactic:
simp [show n + m = n - m + 2 * m by omega, pow_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ (x - y) ^ n = ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
rw [sub_eq_add_neg, add_pow]

Result:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ ∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m < n + 1
⊢ n + m = n - m + 2 * m

Tactic:
omega

Result:
no goals

Proof state:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
this : (-1) ^ (n - m) = (-1) ^ (n + m)
⊢ x ^ m * ((-1) ^ (n + m) * y ^ (n - m)) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
ring

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ ∑ m ∈ range (n + 1), x ^ m * (-y) ^ (n - m) * ↑(n.choose m) =
    ∑ m ∈ range (n + 1), (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)

Tactic:
congr! 1 with m hm

Result:
case a
R : Type u_1
inst✝ : CommRing R
x y : R
n m : ℕ
hm : m ∈ range (n + 1)
⊢ x ^ m * (-y) ^ (n - m) * ↑(n.choose m) = (-1) ^ (m + n) * x ^ m * y ^ (n - m) * ↑(n.choose m)
-- Mathlib/Analysis/InnerProductSpace/Calculus.lean
theorem PartialHomeomorph.contDiff_univUnitBall : ContDiff ℝ n (univUnitBall : E → E)

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ ↑n ↑univUnitBall

Tactic:
suffices ContDiff ℝ n fun x : E => (√(1 + ‖x‖ ^ 2 : ℝ))⁻¹ from this.smul contDiff_id

Result:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ ↑n fun x => (√(1 + ‖x‖ ^ 2))⁻¹

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ ↑n fun x => (√(1 + ‖x‖ ^ 2))⁻¹

Tactic:
refine ContDiff.inv ?_ fun x => Real.sqrt_ne_zero'.mpr (h x)

Result:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ ↑n fun x => √(1 + ‖x‖ ^ 2)

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ ↑n fun x => √(1 + ‖x‖ ^ 2)

Tactic:
exact (contDiff_const.add <| contDiff_norm_sq ℝ).sqrt fun x => (h x).ne'

Result:
no goals

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
x : E
⊢ 0 < 1 + ‖x‖ ^ 2

Tactic:
positivity

Result:
no goals

Proof state:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
⊢ ContDiff ℝ ↑n fun x => (√(1 + ‖x‖ ^ 2))⁻¹

Tactic:
have h : ∀ x : E, (0 : ℝ) < (1 : ℝ) + ‖x‖ ^ 2 := fun x => by positivity

Result:
n : ℕ∞
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
h : ∀ (x : E), 0 < 1 + ‖x‖ ^ 2
⊢ ContDiff ℝ ↑n fun x => (√(1 + ‖x‖ ^ 2))⁻¹
-- Mathlib/GroupTheory/ArchimedeanDensely.lean
/-- The subgroup generated by an element of a group equals the set of
integer powers of the element, such that each power is a unique element.
This is the stronger version of `Subgroup.mem_closure_singleton`. -/
@[to_additive "The additive subgroup generated by an element of an additive group equals the set of
integer multiples of the element, such that each multiple is a unique element.
This is the stronger version of `AddSubgroup.mem_closure_singleton`."]
lemma Subgroup.mem_closure_singleton_iff_existsUnique_zpow {G : Type*}
    [LinearOrderedCommGroup G] {a b : G} (ha : a ≠ 1) :
    b ∈ closure {a} ↔ ∃! k : ℤ, a ^ k = b

Proof state:
case mpr
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ (∃! k, a ^ k = b) → ∃ n, a ^ n = b

Tactic:
exact fun h ↦ h.exists

Result:
no goals

Proof state:
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ b ∈ closure {a} ↔ ∃! k, a ^ k = b

Tactic:
rw [mem_closure_singleton]

Result:
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) ↔ ∃! k, a ^ k = b

Proof state:
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) ↔ ∃! k, a ^ k = b

Tactic:
constructor

Result:
case mp
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ (∃ n, a ^ n = b) → ∃! k, a ^ k = b

case mpr
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ (∃! k, a ^ k = b) → ∃ n, a ^ n = b

Proof state:
case mp.inr
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x => a ^ x

Tactic:
exact (zpow_right_strictMono ha).injective

Result:
no goals

Proof state:
case mp.inl
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha✝ : a ≠ 1
ha : a < 1
⊢ Function.Injective fun x => a ^ x

Tactic:
exact (zpow_right_strictAnti ha).injective

Result:
no goals

Proof state:
case intro
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a : G
ha : a ≠ 1
this : Function.Injective fun x => a ^ x
m : ℤ
⊢ ∃! k, a ^ k = a ^ m

Tactic:
exact ⟨m, rfl, fun k hk ↦ this hk⟩

Result:
no goals

Proof state:
case mp
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
⊢ Function.Injective fun x => a ^ x

Tactic:
rcases ha.lt_or_lt with ha | ha

Result:
case mp.inl
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha✝ : a ≠ 1
ha : a < 1
⊢ Function.Injective fun x => a ^ x

case mp.inr
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha✝ : a ≠ 1
ha : 1 < a
⊢ Function.Injective fun x => a ^ x

Proof state:
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a b : G
ha : a ≠ 1
this : Function.Injective fun x => a ^ x
⊢ (∃ n, a ^ n = b) → ∃! k, a ^ k = b

Tactic:
rintro ⟨m, rfl⟩

Result:
case intro
G : Type u_1
inst✝ : LinearOrderedCommGroup G
a : G
ha : a ≠ 1
this : Function.Injective fun x => a ^ x
m : ℤ
⊢ ∃! k, a ^ k = a ^ m
-- Mathlib/Algebra/Algebra/Subalgebra/Directed.lean
theorem iSupLift_mk {dir : Directed (· ≤ ·) K} {f : ∀ i, K i →ₐ[R] B}
    {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)}
    {T : Subalgebra R A} {hT : T = iSup K} {i : ι} (x : K i) (hx : (x : A) ∈ T) :
    iSupLift K dir f hf T hT ⟨x, hx⟩ = f i x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ (iSupLift K dir f hf T hT) ⟨↑x, hx⟩ = (f i) x

Tactic:
dsimp [iSupLift, inclusion]

Result:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ ⟨↑x, hx⟩ = (f i) x

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
inst✝² : Semiring B
inst✝¹ : Algebra R B
ι : Type u_4
inst✝ : Nonempty ι
K : ι → Subalgebra R A
dir : Directed (fun x1 x2 => x1 ≤ x2) K
f : (i : ι) → ↥(K i) →ₐ[R] B
hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (inclusion h)
T : Subalgebra R A
hT : T = iSup K
i : ι
x : ↥(K i)
hx : ↑x ∈ T
⊢ Set.iUnionLift (fun i => ↑(K i)) (fun i x => (f i) x) ⋯ ↑T ⋯ ⟨↑x, hx⟩ = (f i) x

Tactic:
rw [Set.iUnionLift_mk]

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem mem_sInf {S : Set (NonUnitalSubalgebra R A)} {x : A} : x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
S : Set (NonUnitalSubalgebra R A)
x : A
⊢ x ∈ sInf S ↔ ∀ p ∈ S, x ∈ p

Tactic:
simp only [← SetLike.mem_coe, coe_sInf, Set.mem_iInter₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_lt_self {n k : Nat} (hLtN : 0 < n) (hLtK : 1 < k) : n / k < n

Proof state:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 < n

Tactic:
have ⟨_, hKN⟩ := h

Result:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 < n

Proof state:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 < n

Tactic:
have := Nat.add_le_of_le_sub hKN this

Result:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this✝ : (n - k) / k ≤ n - k
this : (n - k) / k + k ≤ n
⊢ (n - k) / k + 1 < n

Proof state:
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n

Tactic:
cases (inferInstance : Decidable (0 < k ∧ k ≤ n)) with
| isFalse h => simp [hLtN, h]
| isTrue h =>
  suffices (n - k) / k + 1 < n by simp [h, this]
  have ⟨_, hKN⟩ := h
  have : (n - k) / k ≤ n - k := div_le_self (n - k) k
  have := Nat.add_le_of_le_sub hKN this
  exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this

Result:
no goals

Proof state:
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
this : (n - k) / k + 1 < n
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n

Tactic:
simp [h, this]

Result:
no goals

Proof state:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n

Tactic:
suffices (n - k) / k + 1 < n by simp [h, this]

Result:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
⊢ (n - k) / k + 1 < n

Proof state:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
⊢ (n - k) / k + 1 < n

Tactic:
have : (n - k) / k ≤ n - k := div_le_self (n - k) k

Result:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this : (n - k) / k ≤ n - k
⊢ (n - k) / k + 1 < n

Proof state:
case isFalse
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : ¬(0 < k ∧ k ≤ n)
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n

Tactic:
simp [hLtN, h]

Result:
no goals

Proof state:
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ n / k < n

Tactic:
rw [div_eq]

Result:
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
⊢ ite (0 < k ∧ k ≤ n) ((n - k) / k + 1) 0 < n

Proof state:
case isTrue
n k : Nat
hLtN : 0 < n
hLtK : 1 < k
h : 0 < k ∧ k ≤ n
left✝ : 0 < k
hKN : k ≤ n
this✝ : (n - k) / k ≤ n - k
this : (n - k) / k + k ≤ n
⊢ (n - k) / k + 1 < n

Tactic:
exact Nat.lt_of_lt_of_le (Nat.add_lt_add_left hLtK _) this

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
lemma coheight_add_one_le {a b : α} (hab : b < a) : coheight a + 1 ≤ coheight b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
⊢ coheight a + 1 ≤ coheight b

Tactic:
cases hfin : coheight a with
| top =>
  have : ⊤ ≤ coheight b := by
    rw [← hfin]
    gcongr
  simp [this]
| coe n =>
  apply Order.add_one_le_of_lt
  rw [← hfin]
  gcongr
  simp [hfin]

Result:
no goals

Proof state:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ ↑n < coheight b

Tactic:
rw [← hfin]

Result:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < coheight b

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
this : ⊤ ≤ coheight b
⊢ ⊤ + 1 ≤ coheight b

Tactic:
simp [this]

Result:
no goals

Proof state:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < coheight b

Tactic:
gcongr

Result:
case coe.h.hfin
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < ⊤

Proof state:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ ⊤ + 1 ≤ coheight b

Tactic:
have : ⊤ ≤ coheight b := by
  rw [← hfin]
  gcongr

Result:
case top
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
this : ⊤ ≤ coheight b
⊢ ⊤ + 1 ≤ coheight b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ ⊤ ≤ coheight b

Tactic:
rw [← hfin]

Result:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ coheight a ≤ coheight b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
hfin : coheight a = ⊤
⊢ coheight a ≤ coheight b

Tactic:
gcongr

Result:
no goals

Proof state:
case coe
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ ↑n + 1 ≤ coheight b

Tactic:
apply Order.add_one_le_of_lt

Result:
case coe.h
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ ↑n < coheight b

Proof state:
case coe.h.hfin
α : Type u_1
inst✝ : Preorder α
a b : α
hab : b < a
n : ℕ
hfin : coheight a = ↑n
⊢ coheight a < ⊤

Tactic:
simp [hfin]

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
/-- In a category which admits strongly cartesian pullbacks, any cartesian morphism is
strongly cartesian. This is a helper-lemma for the fact that admitting strongly cartesian pullbacks
implies being fibered. -/
lemma isStronglyCartesian_of_exists_isCartesian (p : 𝒳 ⥤ 𝒮) (h : ∀ (a : 𝒳) (R : 𝒮)
    (f : R ⟶ p.obj a), ∃ (b : 𝒳) (φ : b ⟶ a), IsStronglyCartesian p f φ) {R S : 𝒮} (f : R ⟶ S)
      {a b : 𝒳} (φ : a ⟶ b) [p.IsCartesian f φ] : p.IsStronglyCartesian f φ

Proof state:
case h
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ (fun χ => p.IsHomLift g χ ∧ χ ≫ φ = φ') (τ' ≫ Φ.hom) ∧
    ∀ (y : c ⟶ a), (fun χ => p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom

Tactic:
refine ⟨⟨by simp only [Φ]; infer_instance, ?_⟩, ?_⟩

Result:
case h.refine_1
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ (τ' ≫ Φ.hom) ≫ φ = φ'

case h.refine_2
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ ∀ (y : c ⟶ a), (fun χ => p.IsHomLift g χ ∧ χ ≫ φ = φ') y → y = τ' ≫ Φ.hom

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
h : ∀ (a : 𝒳) (R : 𝒮) (f : R ⟶ p.obj a), ∃ b φ, p.IsStronglyCartesian f φ
a b : 𝒳
φ : a ⟶ b
c : 𝒳
φ' : c ⟶ b
g : p.obj c ⟶ p.obj a
inst✝ : p.IsCartesian (p.map φ) φ
hφ' : p.IsHomLift (g ≫ p.map φ) φ'
a' : 𝒳
ψ : a' ⟶ b
hψ : p.IsStronglyCartesian (p.map φ) ψ
τ' : c ⟶ a' := IsStronglyCartesian.map p (p.map φ) ψ ⋯ φ'
Φ : a' ≅ a := domainUniqueUpToIso p (p.map φ) φ ψ
⊢ p.IsHomLift g (τ' ≫ (domainUniqueUpToIso p (p.map φ) φ ψ).hom)

Tactic:
infer_instance

Result:
no goals