harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma isIso_snd_of_isIso (h : IsPullback fst snd f g) [IsIso f] : IsIso snd

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso f
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.snd f g)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso f
⊢ IsIso snd

Tactic:
have := h.hasPullback

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso f
this : HasPullback f g
⊢ IsIso snd

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso f
this : HasPullback f g
⊢ IsIso snd

Tactic:
rw [← h.isoPullback_hom_snd]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : IsIso f
this : HasPullback f g
⊢ IsIso (h.isoPullback.hom ≫ pullback.snd f g)
-- Mathlib/Analysis/Convex/Between.lean
theorem wbtw_smul_vadd_smul_vadd_of_nonneg_of_le (x : P) (v : V) {r₁ r₂ : R} (hr₁ : 0 ≤ r₁)
    (hr₂ : r₁ ≤ r₂) : Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Proof state:
case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
simp [lineMap_apply, smul_smul, ((hr₁.lt_of_ne' h).trans_le hr₂).ne.symm]

Result:
no goals

Proof state:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
simp [h]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ Wbtw R x (r₁ • v +ᵥ x) (r₂ • v +ᵥ x)

Tactic:
refine ⟨r₁ / r₂, ⟨div_nonneg hr₁ (hr₁.trans hr₂), div_le_one_of_le₀ hr₂ (hr₁.trans hr₂)⟩, ?_⟩

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

Tactic:
by_cases h : r₁ = 0

Result:
case pos
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x

case neg
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
x : P
v : V
r₁ r₂ : R
hr₁ : 0 ≤ r₁
hr₂ : r₁ ≤ r₂
h : ¬r₁ = 0
⊢ (lineMap x (r₂ • v +ᵥ x)) (r₁ / r₂) = r₁ • v +ᵥ x
-- Mathlib/Analysis/Complex/LocallyUniformLimit.lean
theorem differentiableOn_tsum_of_summable_norm {u : ι → ℝ} (hu : Summable u)
    (hf : ∀ i : ι, DifferentiableOn ℂ (F i) U) (hU : IsOpen U)
    (hF_le : ∀ (i : ι) (w : ℂ), w ∈ U → ‖F i w‖ ≤ u i) :
    DifferentiableOn ℂ (fun w : ℂ => ∑' i : ι, F i w) U

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U

Tactic:
refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => ∑ n ∈ s, F n x) U

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U

Tactic:
classical
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn
refine hc.differentiableOn (Eventually.of_forall fun s => ?_) hU
exact DifferentiableOn.sum fun i _ => hf i

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U
s : Finset ι
⊢ DifferentiableOn ℂ (fun x => ∑ n ∈ s, F n x) U

Tactic:
exact DifferentiableOn.sum fun i _ => hf i

Result:
no goals

Proof state:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U

Tactic:
have hc := (tendstoUniformlyOn_tsum hu hF_le).tendstoLocallyUniformlyOn

Result:
E : Type u_1
ι : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
U : Set ℂ
F : ι → ℂ → E
inst✝ : CompleteSpace E
u : ι → ℝ
hu : Summable u
hf : ∀ (i : ι), DifferentiableOn ℂ (F i) U
hU : IsOpen U
hF_le : ∀ (i : ι), ∀ w ∈ U, ‖F i w‖ ≤ u i
hc : TendstoLocallyUniformlyOn (fun t x => ∑ n ∈ t, F n x) (fun x => ∑' (n : ι), F n x) atTop U
⊢ DifferentiableOn ℂ (fun w => ∑' (i : ι), F i w) U
-- Mathlib/Order/Filter/NAry.lean
theorem map_map₂_antidistrib {n : γ → δ} {m' : β' → α' → δ} {n₁ : β → β'} {n₂ : α → α'}
    (h_antidistrib : ∀ a b, n (m a b) = m' (n₁ b) (n₂ a)) :
    (map₂ m f g).map n = map₂ m' (g.map n₁) (f.map n₂)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ (fun a b => m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
exact map_map₂_distrib fun _ _ => h_antidistrib _ _

Result:
no goals

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ m f g) = map₂ m' (map n₁ g) (map n₂ f)

Tactic:
rw [map₂_swap m]

Result:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
m : α → β → γ
f : Filter α
g : Filter β
n : γ → δ
m' : β' → α' → δ
n₁ : β → β'
n₂ : α → α'
h_antidistrib : ∀ (a : α) (b : β), n (m a b) = m' (n₁ b) (n₂ a)
⊢ map n (map₂ (fun a b => m b a) g f) = map₂ m' (map n₁ g) (map n₂ f)
-- Mathlib/Data/Matroid/Loop.lean
@[simp]
lemma map_isLoop_iff {f : α → β} {hf : InjOn f M.E} (he : e ∈ M.E

Proof state:
α : Type u_1
β : Type u_2
M : Matroid α
e : α
f : α → β
hf : InjOn f M.E
he : autoParam (e ∈ M.E) _auto✝
⊢ (M.map f hf).IsLoop (f e) ↔ M.IsLoop e

Tactic:
rw [isLoop_iff, map_loops, hf.mem_image_iff M.loops_subset_ground he, isLoop_iff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Basis.lean
theorem coePiBasisFun.toMatrix_eq_transpose [Finite ι] :
    ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose

Proof state:
case h.a
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
M : ι → ι → R
i j : ι
⊢ (Pi.basisFun R ι).toMatrix M i j = Mᵀ i j

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
⊢ (Pi.basisFun R ι).toMatrix = transpose

Tactic:
ext M i j

Result:
case h.a
ι : Type u_1
R : Type u_5
inst✝¹ : CommSemiring R
inst✝ : Finite ι
M : ι → ι → R
i j : ι
⊢ (Pi.basisFun R ι).toMatrix M i j = Mᵀ i j
-- Mathlib/Logic/Unique.lean
theorem unique_subtype_iff_existsUnique {α} (p : α → Prop) :
    Nonempty (Unique (Subtype p)) ↔ ∃! a, p a :=
  ⟨fun ⟨u⟩ ↦ ⟨u.default.1, u.default.2, fun a h ↦ congr_arg Subtype.val (u.uniq ⟨a, h⟩)⟩,
   fun ⟨a, ha, he⟩ ↦ ⟨⟨⟨⟨a, ha⟩⟩, fun ⟨b, hb⟩ ↦ by
      congr
      exact he b hb⟩⟩⟩

Proof state:
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ ⟨b, hb⟩ = default

Tactic:
congr

Result:
case e_val
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a

Proof state:
case e_val
α : Sort u_1
p : α → Prop
x✝¹ : ∃! a, p a
a : α
ha : (fun a => p a) a
he : ∀ (y : α), (fun a => p a) y → y = a
x✝ : Subtype p
b : α
hb : p b
⊢ b = a

Tactic:
exact he b hb

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem zpow_sub {x : ℝ≥0∞} (x_ne_zero : x ≠ 0) (x_ne_top : x ≠ ⊤) (m n : ℤ) :
    x ^ (m - n) = (x ^ m) * (x ^ n)⁻¹

Proof state:
x : ℝ≥0∞
x_ne_zero : x ≠ 0
x_ne_top : x ≠ ⊤
m n : ℤ
⊢ x ^ (m - n) = x ^ m * (x ^ n)⁻¹

Tactic:
rw [sub_eq_add_neg, ENNReal.zpow_add x_ne_zero x_ne_top, ENNReal.zpow_neg x_ne_zero x_ne_top n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_zero_left (y : Nat) : gcd 0 y = y

Proof state:
y : Nat
⊢ gcd 0 y = y

Tactic:
rw [gcd]

Result:
y : Nat
⊢ (if 0 = 0 then y else (y % 0).gcd 0) = y

Proof state:
y : Nat
⊢ (if 0 = 0 then y else (y % 0).gcd 0) = y

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_le_size_insertIfNew [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    m.1.size ≤ (m.insertIfNew k v).1.size

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ m.val.size ≤ (m.insertIfNew k v).val.size

Tactic:
simp_to_model [insertIfNew] using List.length_le_length_insertEntryIfNew

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_const_iff {c : β} :
    HasFiniteIntegral (fun _ : α => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
c : β
⊢ HasFiniteIntegral (fun x => c) μ ↔ c = 0 ∨ IsFiniteMeasure μ

Tactic:
simp [hasFiniteIntegral_iff_enorm, lintegral_const, lt_top_iff_ne_top, ENNReal.mul_eq_top,
  or_iff_not_imp_left, isFiniteMeasure_iff]

Result:
no goals
-- Mathlib/Order/KrullDimension.lean
private lemma height_add_const (a : α) (n : ℕ∞) :
    height a + n = ⨆ (p : LTSeries α) (_ : p.last = a), p.length + n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
⊢ height a + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Tactic:
have hne : Nonempty { p : LTSeries α // p.last = a } := ⟨RelSeries.singleton _ a, rfl⟩

Result:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ height a + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Proof state:
α : Type u_1
inst✝ : Preorder α
a : α
n : ℕ∞
hne : Nonempty { p // RelSeries.last p = a }
⊢ height a + n = ⨆ p, ⨆ (_ : RelSeries.last p = a), ↑p.length + n

Tactic:
rw [height_eq_iSup_last_eq, iSup_subtype', iSup_subtype', ENat.iSup_add]

Result:
no goals
-- Mathlib/Data/Complex/Basic.lean
theorem inv_zero : (0⁻¹ : ℂ) = 0

Proof state:
⊢ 0⁻¹ = 0

Tactic:
rw [← ofReal_zero, ← ofReal_inv, inv_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Sum/Lemmas.lean
theorem liftRel_swap_iff : LiftRel s r x.swap y.swap ↔ LiftRel r s x y :=
  ⟨fun h => by rw [← swap_swap x, ← swap_swap y]; exact h.swap, LiftRel.swap⟩

Proof state:
β✝¹ : Type u_1
β✝ : Type u_2
s : β✝¹ → β✝ → Prop
α✝¹ : Type u_3
α✝ : Type u_4
r : α✝¹ → α✝ → Prop
x : α✝¹ ⊕ β✝¹
y : α✝ ⊕ β✝
h : LiftRel s r x.swap y.swap
⊢ LiftRel r s x.swap.swap y.swap.swap

Tactic:
exact h.swap

Result:
no goals

Proof state:
β✝¹ : Type u_1
β✝ : Type u_2
s : β✝¹ → β✝ → Prop
α✝¹ : Type u_3
α✝ : Type u_4
r : α✝¹ → α✝ → Prop
x : α✝¹ ⊕ β✝¹
y : α✝ ⊕ β✝
h : LiftRel s r x.swap y.swap
⊢ LiftRel r s x y

Tactic:
rw [← swap_swap x, ← swap_swap y]

Result:
β✝¹ : Type u_1
β✝ : Type u_2
s : β✝¹ → β✝ → Prop
α✝¹ : Type u_3
α✝ : Type u_4
r : α✝¹ → α✝ → Prop
x : α✝¹ ⊕ β✝¹
y : α✝ ⊕ β✝
h : LiftRel s r x.swap y.swap
⊢ LiftRel r s x.swap.swap y.swap.swap
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem det_adjustToOrientation :
    (e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨
      (e.adjustToOrientation x).toBasis.det = -e.toBasis.det

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ (e.adjustToOrientation x).toBasis.det = e.toBasis.det ∨ (e.adjustToOrientation x).toBasis.det = -e.toBasis.det

Tactic:
simpa using e.toBasis.det_adjustToOrientation x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem count_le_count_map [DecidableEq β] (l : Array α) (f : α → β) (x : α) :
    count x l ≤ count (f x) (map f l)

Proof state:
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
l : Array α
f : α → β
x : α
⊢ count x l ≤ count (f x) (map f l)

Tactic:
cases l

Result:
case mk
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
f : α → β
x : α
toList✝ : List α
⊢ count x { toList := toList✝ } ≤ count (f x) (map f { toList := toList✝ })

Proof state:
case mk
α : Type u_2
inst✝² : BEq α
inst✝¹ : LawfulBEq α
β : Type u_1
inst✝ : DecidableEq β
f : α → β
x : α
toList✝ : List α
⊢ count x { toList := toList✝ } ≤ count (f x) (map f { toList := toList✝ })

Tactic:
simp [List.count_le_count_map, countP_map]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem dvd_div_of_mul_dvd {a b c : R} (h : a * b ∣ c) : b ∣ c / a

Proof state:
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

Tactic:
simp only [div_zero, dvd_zero]

Result:
no goals

Proof state:
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d

Tactic:
rw [mul_assoc, mul_div_cancel_left₀ _ ha]

Result:
no goals

Proof state:
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
⊢ b ∣ c / a

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
R : Type u
inst✝ : EuclideanDomain R
b c : R
h : 0 * b ∣ c
⊢ b ∣ c / 0

case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a

Proof state:
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a

Tactic:
refine ⟨d, ?_⟩

Result:
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ a * b * d / a = b * d

Proof state:
case inr
R : Type u
inst✝ : EuclideanDomain R
a b c : R
h : a * b ∣ c
ha : a ≠ 0
⊢ b ∣ c / a

Tactic:
rcases h with ⟨d, rfl⟩

Result:
case inr.intro
R : Type u
inst✝ : EuclideanDomain R
a b : R
ha : a ≠ 0
d : R
⊢ b ∣ a * b * d / a
-- Mathlib/Algebra/Polynomial/Degree/Lemmas.lean
theorem natDegree_C_mul_of_mul_ne_zero (h : a * p.leadingCoeff ≠ 0) :
    (C a * p).natDegree = p.natDegree

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).natDegree = p.natDegree

Tactic:
refine eq_natDegree_of_le_mem_support (natDegree_C_mul_le a p) ?_

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ p.natDegree ∈ (C a * p).support

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).coeff p.natDegree ≠ 0

Tactic:
rwa [coeff_C_mul]

Result:
no goals

Proof state:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ p.natDegree ∈ (C a * p).support

Tactic:
refine mem_support_iff.mpr ?_

Result:
R : Type u
a : R
inst✝ : Semiring R
p : R[X]
h : a * p.leadingCoeff ≠ 0
⊢ (C a * p).coeff p.natDegree ≠ 0
-- Mathlib/FieldTheory/Finite/Basic.lean
theorem Nat.sq_add_sq_modEq (p : ℕ) [Fact p.Prime] (x : ℕ) :
    ∃ a b : ℕ, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]

Proof state:
p : ℕ
inst✝ : Fact (Prime p)
x : ℕ
⊢ ∃ a b, a ≤ p / 2 ∧ b ≤ p / 2 ∧ a ^ 2 + b ^ 2 ≡ x [MOD p]

Tactic:
simpa only [← Int.natCast_modEq_iff] using Nat.sq_add_sq_zmodEq p x

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_left_inj {x y : BitVec w} (z : BitVec w) : (x + z = y + z) ↔ x = y

Proof state:
w : Nat
x y z : BitVec w
⊢ x + z = y + z ↔ x = y

Tactic:
apply Iff.intro

Result:
case mp
w : Nat
x y z : BitVec w
⊢ x + z = y + z → x = y

case mpr
w : Nat
x y z : BitVec w
⊢ x = y → x + z = y + z

Proof state:
case mp
w : Nat
x y z : BitVec w
⊢ x + z = y + z → x = y

Tactic:
intro p

Result:
case mp
w : Nat
x y z : BitVec w
p : x + z = y + z
⊢ x = y

Proof state:
case mp
w : Nat
x y z : BitVec w
p : x + z = y + z
⊢ x = y

Tactic:
rw [← add_sub_cancel x z, ← add_sub_cancel y z, p]

Result:
no goals
-- Mathlib/Combinatorics/Additive/FreimanHom.lean
@[to_additive (attr := simp) isAddFreimanIso_one_iff]
lemma isMulFreimanIso_one_iff : IsMulFreimanIso 1 A B f ↔ BijOn f A B :=
  ⟨fun h => h.bijOn, fun h => ⟨h, by aesop (add simp [card_eq_one, BijOn])⟩⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CommMonoid α
inst✝ : CommMonoid β
A : Set α
B : Set β
f : α → β
h : BijOn f A B
⊢ ∀ ⦃s t : Multiset α⦄,
    (∀ ⦃x : α⦄, x ∈ s → x ∈ A) →
      (∀ ⦃x : α⦄, x ∈ t → x ∈ A) → s.card = 1 → t.card = 1 → ((map f s).prod = (map f t).prod ↔ s.prod = t.prod)

Tactic:
aesop (add simp [card_eq_one, BijOn])

Result:
no goals
-- Mathlib/Order/Interval/Set/Disjoint.lean
theorem eq_of_Ico_disjoint {x₁ x₂ y₁ y₂ : α} (h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)) (hx : x₁ < x₂)
    (h2 : x₂ ∈ Ico y₁ y₂) : y₁ = x₂

Proof state:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : Disjoint (Ico x₁ x₂) (Ico y₁ y₂)
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
rw [Ico_disjoint_Ico, min_eq_left (le_of_lt h2.2), le_max_iff] at h

Result:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Proof state:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ y₁ = x₂

Tactic:
apply le_antisymm h2.1

Result:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁

Proof state:
α : Type v
inst✝ : LinearOrder α
x₁ x₂ y₁ y₂ : α
h : x₂ ≤ x₁ ∨ x₂ ≤ y₁
hx : x₁ < x₂
h2 : x₂ ∈ Ico y₁ y₂
⊢ x₂ ≤ y₁

Tactic:
exact h.elim (fun h => absurd hx (not_lt_of_le h)) id

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem universalMulHom_unique (φ : R[S⁻¹] →* T) (huniv : ∀ r : R, φ (numeratorHom r) = f r) :
    φ = universalMulHom f fS hf

Proof state:
case h.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)

Tactic:
rw [universalMulHom_apply, ← huniv r, numeratorHom_apply, ← one_mul (φ (r /ₒ s)), ←
  Units.val_one, ← inv_mul_cancel (fS s), Units.val_mul, mul_assoc, ← hf, ← huniv, ← φ.map_mul,
  numeratorHom_apply, OreLocalization.mul_cancel]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x

Tactic:
induction' x with r s

Result:
case h.c
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
r : R
s : ↥S
⊢ φ (r /ₒ s) = (universalMulHom f fS hf) (r /ₒ s)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
⊢ φ = universalMulHom f fS hf

Tactic:
ext x

Result:
case h
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
T : Type u_2
inst✝ : Monoid T
f : R →* T
fS : ↥S →* Tˣ
hf : ∀ (s : ↥S), f ↑s = ↑(fS s)
φ : OreLocalization S R →* T
huniv : ∀ (r : R), φ (numeratorHom r) = f r
x : OreLocalization S R
⊢ φ x = (universalMulHom f fS hf) x
-- Mathlib/Algebra/MonoidAlgebra/Degree.lean
theorem le_inf_support_finset_prod (degt0 : 0 ≤ degt 0)
    (degtm : ∀ a b, degt a + degt b ≤ degt (a + b)) (s : Finset ι) (f : ι → R[A]) :
    (∑ i ∈ s, (f i).support.inf degt) ≤ (∏ i ∈ s, f i).support.inf degt :=
  le_of_eq_of_le (by rw [Multiset.map_map]; rfl) (le_inf_support_multiset_prod degt0 degtm _)

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).support.inf degt = (Multiset.map (fun f => f.support.inf degt) (Multiset.map (fun i => f i) s.val)).sum

Tactic:
rw [Multiset.map_map]

Result:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).support.inf degt = (Multiset.map ((fun f => f.support.inf degt) ∘ fun i => f i) s.val).sum

Proof state:
R : Type u_1
A : Type u_3
T : Type u_4
ι : Type u_6
inst✝⁶ : SemilatticeInf T
inst✝⁵ : OrderTop T
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid A
inst✝² : AddCommMonoid T
inst✝¹ : AddLeftMono T
inst✝ : AddRightMono T
degt : A → T
degt0 : 0 ≤ degt 0
degtm : ∀ (a b : A), degt a + degt b ≤ degt (a + b)
s : Finset ι
f : ι → R[A]
⊢ ∑ i ∈ s, (f i).support.inf degt = (Multiset.map ((fun f => f.support.inf degt) ∘ fun i => f i) s.val).sum

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_tanh_ofReal_re (x : ℝ) : ((tanh x).re : ℂ) = tanh x :=
  conj_eq_iff_re.1 <| by rw [← tanh_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (tanh ↑x) = tanh ↑x

Tactic:
rw [← tanh_conj, conj_ofReal]

Result:
no goals